[STATEMENT]
lemma ex_bij_betw_strict_mono_card:
  assumes "finite M" "M \<subseteq> ON"
  obtains h where "bij_betw h {..<card M} M" and "strict_mono_on {..<card M} h"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>h. \<lbrakk>bij_betw h {..<card M} M; strict_mono_on {..<card M} h\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<And>h. \<lbrakk>bij_betw h {..<card M} M; strict_mono_on {..<card M} h\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
have bij: "bij_betw (ordermap M VWF) M (elts (card M))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bij_betw (ordermap M VWF) M (elts (ord_of_nat (card M)))
[PROOF STEP]
using Finite_V \<open>finite M\<close> ordermap_bij ordertype_VWF_finite_nat
[PROOF STATE]
proof (prove)
using this:
finite ?X \<Longrightarrow> small ?X
finite M
\<lbrakk>wf ?r; total_on ?A ?r; small ?A\<rbrakk> \<Longrightarrow> bij_betw (ordermap ?A ?r) ?A (elts (ordertype ?A ?r))
finite ?A \<Longrightarrow> ordertype ?A VWF = ord_of_nat (card ?A)

goal (1 subgoal):
 1. bij_betw (ordermap M VWF) M (elts (ord_of_nat (card M)))
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
bij_betw (ordermap M VWF) M (elts (ord_of_nat (card M)))

goal (1 subgoal):
 1. (\<And>h. \<lbrakk>bij_betw h {..<card M} M; strict_mono_on {..<card M} h\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
let ?h = "(inv_into M (ordermap M VWF)) \<circ> ord_of_nat"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<And>h. \<lbrakk>bij_betw h {..<card M} M; strict_mono_on {..<card M} h\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
show thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. thesis
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. bij_betw ?h {..<card M} M
 2. strict_mono_on {..<card M} ?h
[PROOF STEP]
show bijh: "bij_betw ?h {..<card M} M"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bij_betw (inv_into M (ordermap M VWF) \<circ> ord_of_nat) {..<card M} M
[PROOF STEP]
proof (rule bij_betw_trans)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. bij_betw ord_of_nat {..<card M} ?B
 2. bij_betw (inv_into M (ordermap M VWF)) ?B M
[PROOF STEP]
show "bij_betw ord_of_nat {..<card M} (elts (card M))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bij_betw ord_of_nat {..<card M} (elts (ord_of_nat (card M)))
[PROOF STEP]
by (simp add: bij_betw_def elts_ord_of_nat inj_on_def)
[PROOF STATE]
proof (state)
this:
bij_betw ord_of_nat {..<card M} (elts (ord_of_nat (card M)))

goal (1 subgoal):
 1. bij_betw (inv_into M (ordermap M VWF)) (elts (ord_of_nat (card M))) M
[PROOF STEP]
show "bij_betw (inv_into M (ordermap M VWF)) (elts (card M)) M"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bij_betw (inv_into M (ordermap M VWF)) (elts (ord_of_nat (card M))) M
[PROOF STEP]
using Finite_V assms bij_betw_inv_into ordermap_bij ordertype_VWF_finite_nat
[PROOF STATE]
proof (prove)
using this:
finite ?X \<Longrightarrow> small ?X
finite M
M \<subseteq> ON
bij_betw ?f ?A ?B \<Longrightarrow> bij_betw (inv_into ?A ?f) ?B ?A
\<lbrakk>wf ?r; total_on ?A ?r; small ?A\<rbrakk> \<Longrightarrow> bij_betw (ordermap ?A ?r) ?A (elts (ordertype ?A ?r))
finite ?A \<Longrightarrow> ordertype ?A VWF = ord_of_nat (card ?A)

goal (1 subgoal):
 1. bij_betw (inv_into M (ordermap M VWF)) (elts (ord_of_nat (card M))) M
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
bij_betw (inv_into M (ordermap M VWF)) (elts (ord_of_nat (card M))) M

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
bij_betw (inv_into M (ordermap M VWF) \<circ> ord_of_nat) {..<card M} M

goal (1 subgoal):
 1. strict_mono_on {..<card M} (inv_into M (ordermap M VWF) \<circ> ord_of_nat)
[PROOF STEP]
show "strict_mono_on {..<card M} ?h"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. strict_mono_on {..<card M} (inv_into M (ordermap M VWF) \<circ> ord_of_nat)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. strict_mono_on {..<card M} (inv_into M (ordermap M VWF) \<circ> ord_of_nat)
[PROOF STEP]
have "?h m < ?h n"
        if "m < n" "n < card M" for m n
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (inv_into M (ordermap M VWF) \<circ> ord_of_nat) m < (inv_into M (ordermap M VWF) \<circ> ord_of_nat) n
[PROOF STEP]
proof (rule ccontr)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> (inv_into M (ordermap M VWF) \<circ> ord_of_nat) m < (inv_into M (ordermap M VWF) \<circ> ord_of_nat) n \<Longrightarrow> False
[PROOF STEP]
obtain mn: "m \<in> elts (ordertype M VWF)" "n \<in> elts (ordertype M VWF)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lbrakk>ord_of_nat m \<in> elts (ordertype M VWF); ord_of_nat n \<in> elts (ordertype M VWF)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using \<open>m < n\<close> \<open>n < card M\<close> \<open>finite M\<close> ordertype_VWF_finite_nat
[PROOF STATE]
proof (prove)
using this:
m < n
n < card M
finite M
finite ?A \<Longrightarrow> ordertype ?A VWF = ord_of_nat (card ?A)

goal (1 subgoal):
 1. (\<lbrakk>ord_of_nat m \<in> elts (ordertype M VWF); ord_of_nat n \<in> elts (ordertype M VWF)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
ord_of_nat m \<in> elts (ordertype M VWF)
ord_of_nat n \<in> elts (ordertype M VWF)

goal (1 subgoal):
 1. \<not> (inv_into M (ordermap M VWF) \<circ> ord_of_nat) m < (inv_into M (ordermap M VWF) \<circ> ord_of_nat) n \<Longrightarrow> False
[PROOF STEP]
have ord: "Ord (?h m)" "Ord (?h n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Ord ((inv_into M (ordermap M VWF) \<circ> ord_of_nat) m) &&& Ord ((inv_into M (ordermap M VWF) \<circ> ord_of_nat) n)
[PROOF STEP]
using bijh assms(2) bij_betwE that
[PROOF STATE]
proof (prove)
using this:
bij_betw (inv_into M (ordermap M VWF) \<circ> ord_of_nat) {..<card M} M
M \<subseteq> ON
bij_betw ?f ?A ?B \<Longrightarrow> \<forall>a\<in>?A. ?f a \<in> ?B
m < n
n < card M

goal (1 subgoal):
 1. Ord ((inv_into M (ordermap M VWF) \<circ> ord_of_nat) m) &&& Ord ((inv_into M (ordermap M VWF) \<circ> ord_of_nat) n)
[PROOF STEP]
by fastforce+
[PROOF STATE]
proof (state)
this:
Ord ((inv_into M (ordermap M VWF) \<circ> ord_of_nat) m)
Ord ((inv_into M (ordermap M VWF) \<circ> ord_of_nat) n)

goal (1 subgoal):
 1. \<not> (inv_into M (ordermap M VWF) \<circ> ord_of_nat) m < (inv_into M (ordermap M VWF) \<circ> ord_of_nat) n \<Longrightarrow> False
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
Ord ((inv_into M (ordermap M VWF) \<circ> ord_of_nat) m)
Ord ((inv_into M (ordermap M VWF) \<circ> ord_of_nat) n)

goal (1 subgoal):
 1. \<not> (inv_into M (ordermap M VWF) \<circ> ord_of_nat) m < (inv_into M (ordermap M VWF) \<circ> ord_of_nat) n \<Longrightarrow> False
[PROOF STEP]
assume "\<not> ?h m < ?h n"
[PROOF STATE]
proof (state)
this:
\<not> (inv_into M (ordermap M VWF) \<circ> ord_of_nat) m < (inv_into M (ordermap M VWF) \<circ> ord_of_nat) n

goal (1 subgoal):
 1. \<not> (inv_into M (ordermap M VWF) \<circ> ord_of_nat) m < (inv_into M (ordermap M VWF) \<circ> ord_of_nat) n \<Longrightarrow> False
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
Ord ((inv_into M (ordermap M VWF) \<circ> ord_of_nat) m)
Ord ((inv_into M (ordermap M VWF) \<circ> ord_of_nat) n)
\<not> (inv_into M (ordermap M VWF) \<circ> ord_of_nat) m < (inv_into M (ordermap M VWF) \<circ> ord_of_nat) n
[PROOF STEP]
consider "?h m = ?h n" | "?h m > ?h n"
[PROOF STATE]
proof (prove)
using this:
Ord ((inv_into M (ordermap M VWF) \<circ> ord_of_nat) m)
Ord ((inv_into M (ordermap M VWF) \<circ> ord_of_nat) n)
\<not> (inv_into M (ordermap M VWF) \<circ> ord_of_nat) m < (inv_into M (ordermap M VWF) \<circ> ord_of_nat) n

goal (1 subgoal):
 1. \<lbrakk>(inv_into M (ordermap M VWF) \<circ> ord_of_nat) m = (inv_into M (ordermap M VWF) \<circ> ord_of_nat) n \<Longrightarrow> thesis; (inv_into M (ordermap M VWF) \<circ> ord_of_nat) n < (inv_into M (ordermap M VWF) \<circ> ord_of_nat) m \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
using Ord_linear_lt
[PROOF STATE]
proof (prove)
using this:
Ord ((inv_into M (ordermap M VWF) \<circ> ord_of_nat) m)
Ord ((inv_into M (ordermap M VWF) \<circ> ord_of_nat) n)
\<not> (inv_into M (ordermap M VWF) \<circ> ord_of_nat) m < (inv_into M (ordermap M VWF) \<circ> ord_of_nat) n
\<lbrakk>Ord ?k; Ord ?l; ?k < ?l \<Longrightarrow> ?thesis; ?k = ?l \<Longrightarrow> ?thesis; ?l < ?k \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. \<lbrakk>(inv_into M (ordermap M VWF) \<circ> ord_of_nat) m = (inv_into M (ordermap M VWF) \<circ> ord_of_nat) n \<Longrightarrow> thesis; (inv_into M (ordermap M VWF) \<circ> ord_of_nat) n < (inv_into M (ordermap M VWF) \<circ> ord_of_nat) m \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<lbrakk>(inv_into M (ordermap M VWF) \<circ> ord_of_nat) m = (inv_into M (ordermap M VWF) \<circ> ord_of_nat) n \<Longrightarrow> ?thesis; (inv_into M (ordermap M VWF) \<circ> ord_of_nat) n < (inv_into M (ordermap M VWF) \<circ> ord_of_nat) m \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. \<not> (inv_into M (ordermap M VWF) \<circ> ord_of_nat) m < (inv_into M (ordermap M VWF) \<circ> ord_of_nat) n \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>(inv_into M (ordermap M VWF) \<circ> ord_of_nat) m = (inv_into M (ordermap M VWF) \<circ> ord_of_nat) n \<Longrightarrow> ?thesis; (inv_into M (ordermap M VWF) \<circ> ord_of_nat) n < (inv_into M (ordermap M VWF) \<circ> ord_of_nat) m \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>(inv_into M (ordermap M VWF) \<circ> ord_of_nat) m = (inv_into M (ordermap M VWF) \<circ> ord_of_nat) n \<Longrightarrow> ?thesis; (inv_into M (ordermap M VWF) \<circ> ord_of_nat) n < (inv_into M (ordermap M VWF) \<circ> ord_of_nat) m \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. False
[PROOF STEP]
proof cases
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. (inv_into M (ordermap M VWF) \<circ> ord_of_nat) m = (inv_into M (ordermap M VWF) \<circ> ord_of_nat) n \<Longrightarrow> False
 2. (inv_into M (ordermap M VWF) \<circ> ord_of_nat) n < (inv_into M (ordermap M VWF) \<circ> ord_of_nat) m \<Longrightarrow> False
[PROOF STEP]
case 1
[PROOF STATE]
proof (state)
this:
(inv_into M (ordermap M VWF) \<circ> ord_of_nat) m = (inv_into M (ordermap M VWF) \<circ> ord_of_nat) n

goal (2 subgoals):
 1. (inv_into M (ordermap M VWF) \<circ> ord_of_nat) m = (inv_into M (ordermap M VWF) \<circ> ord_of_nat) n \<Longrightarrow> False
 2. (inv_into M (ordermap M VWF) \<circ> ord_of_nat) n < (inv_into M (ordermap M VWF) \<circ> ord_of_nat) m \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(inv_into M (ordermap M VWF) \<circ> ord_of_nat) m = (inv_into M (ordermap M VWF) \<circ> ord_of_nat) n
[PROOF STEP]
have "m = n"
[PROOF STATE]
proof (prove)
using this:
(inv_into M (ordermap M VWF) \<circ> ord_of_nat) m = (inv_into M (ordermap M VWF) \<circ> ord_of_nat) n

goal (1 subgoal):
 1. m = n
[PROOF STEP]
by (metis inv_ordermap_mono_eq mn comp_apply ord_of_nat_inject)
[PROOF STATE]
proof (state)
this:
m = n

goal (2 subgoals):
 1. (inv_into M (ordermap M VWF) \<circ> ord_of_nat) m = (inv_into M (ordermap M VWF) \<circ> ord_of_nat) n \<Longrightarrow> False
 2. (inv_into M (ordermap M VWF) \<circ> ord_of_nat) n < (inv_into M (ordermap M VWF) \<circ> ord_of_nat) m \<Longrightarrow> False
[PROOF STEP]
with \<open>m < n\<close>
[PROOF STATE]
proof (chain)
picking this:
m < n
m = n
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
m < n
m = n

goal (1 subgoal):
 1. False
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
False

goal (1 subgoal):
 1. (inv_into M (ordermap M VWF) \<circ> ord_of_nat) n < (inv_into M (ordermap M VWF) \<circ> ord_of_nat) m \<Longrightarrow> False
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (inv_into M (ordermap M VWF) \<circ> ord_of_nat) n < (inv_into M (ordermap M VWF) \<circ> ord_of_nat) m \<Longrightarrow> False
[PROOF STEP]
case 2
[PROOF STATE]
proof (state)
this:
(inv_into M (ordermap M VWF) \<circ> ord_of_nat) n < (inv_into M (ordermap M VWF) \<circ> ord_of_nat) m

goal (1 subgoal):
 1. (inv_into M (ordermap M VWF) \<circ> ord_of_nat) n < (inv_into M (ordermap M VWF) \<circ> ord_of_nat) m \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(inv_into M (ordermap M VWF) \<circ> ord_of_nat) n < (inv_into M (ordermap M VWF) \<circ> ord_of_nat) m
[PROOF STEP]
have "ord_of_nat n \<le> ord_of_nat m"
[PROOF STATE]
proof (prove)
using this:
(inv_into M (ordermap M VWF) \<circ> ord_of_nat) n < (inv_into M (ordermap M VWF) \<circ> ord_of_nat) m

goal (1 subgoal):
 1. ord_of_nat n \<le> ord_of_nat m
[PROOF STEP]
by (metis Finite_V mn assms comp_def inv_ordermap_VWF_mono_le less_imp_le)
[PROOF STATE]
proof (state)
this:
ord_of_nat n \<le> ord_of_nat m

goal (1 subgoal):
 1. (inv_into M (ordermap M VWF) \<circ> ord_of_nat) n < (inv_into M (ordermap M VWF) \<circ> ord_of_nat) m \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
ord_of_nat n \<le> ord_of_nat m
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
ord_of_nat n \<le> ord_of_nat m

goal (1 subgoal):
 1. False
[PROOF STEP]
using leD \<open>m < n\<close>
[PROOF STATE]
proof (prove)
using this:
ord_of_nat n \<le> ord_of_nat m
?y \<le> ?x \<Longrightarrow> \<not> ?x < ?y
m < n

goal (1 subgoal):
 1. False
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
False

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
False

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<lbrakk>?m < ?n; ?n < card M\<rbrakk> \<Longrightarrow> (inv_into M (ordermap M VWF) \<circ> ord_of_nat) ?m < (inv_into M (ordermap M VWF) \<circ> ord_of_nat) ?n

goal (1 subgoal):
 1. strict_mono_on {..<card M} (inv_into M (ordermap M VWF) \<circ> ord_of_nat)
[PROOF STEP]
with assms
[PROOF STATE]
proof (chain)
picking this:
finite M
M \<subseteq> ON
\<lbrakk>?m < ?n; ?n < card M\<rbrakk> \<Longrightarrow> (inv_into M (ordermap M VWF) \<circ> ord_of_nat) ?m < (inv_into M (ordermap M VWF) \<circ> ord_of_nat) ?n
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
finite M
M \<subseteq> ON
\<lbrakk>?m < ?n; ?n < card M\<rbrakk> \<Longrightarrow> (inv_into M (ordermap M VWF) \<circ> ord_of_nat) ?m < (inv_into M (ordermap M VWF) \<circ> ord_of_nat) ?n

goal (1 subgoal):
 1. strict_mono_on {..<card M} (inv_into M (ordermap M VWF) \<circ> ord_of_nat)
[PROOF STEP]
by (auto simp: strict_mono_on_def)
[PROOF STATE]
proof (state)
this:
strict_mono_on {..<card M} (inv_into M (ordermap M VWF) \<circ> ord_of_nat)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
strict_mono_on {..<card M} (inv_into M (ordermap M VWF) \<circ> ord_of_nat)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
thesis

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma ordertype_finite_less_than [simp]:
  assumes "finite A" shows "ordertype A less_than = card A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ordertype A less_than = ord_of_nat (card A)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ordertype A less_than = ord_of_nat (card A)
[PROOF STEP]
let ?M = "ord_of_nat ` A"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ordertype A less_than = ord_of_nat (card A)
[PROOF STEP]
obtain M: "finite ?M" "?M \<subseteq> ON"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lbrakk>finite (ord_of_nat ` A); ord_of_nat ` A \<subseteq> ON\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using Ord_ord_of_nat assms
[PROOF STATE]
proof (prove)
using this:
Ord (ord_of_nat ?k)
finite A

goal (1 subgoal):
 1. (\<lbrakk>finite (ord_of_nat ` A); ord_of_nat ` A \<subseteq> ON\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
finite (ord_of_nat ` A)
ord_of_nat ` A \<subseteq> ON

goal (1 subgoal):
 1. ordertype A less_than = ord_of_nat (card A)
[PROOF STEP]
have "ordertype A less_than = ordertype ?M VWF"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ordertype A less_than = ordertype (ord_of_nat ` A) VWF
[PROOF STEP]
by (rule ordertype_inc_eq [symmetric]) (use assms finite_imp_small total_on_def in \<open>force+\<close>)
[PROOF STATE]
proof (state)
this:
ordertype A less_than = ordertype (ord_of_nat ` A) VWF

goal (1 subgoal):
 1. ordertype A less_than = ord_of_nat (card A)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
ordertype A less_than = ordertype (ord_of_nat ` A) VWF

goal (1 subgoal):
 1. ordertype A less_than = ord_of_nat (card A)
[PROOF STEP]
have "\<dots> = card A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ordertype (ord_of_nat ` A) VWF = ord_of_nat (card A)
[PROOF STEP]
proof (subst ordertype_eq_iff)
[PROOF STATE]
proof (state)
goal (6 subgoals):
 1. Ord (ord_of_nat (card A))
 2. wf VWF
 3. small (ord_of_nat ` A)
 4. total_on (ord_of_nat ` A) VWF
 5. trans VWF
 6. \<exists>f. bij_betw f (ord_of_nat ` A) (elts (ord_of_nat (card A))) \<and> (\<forall>x\<in>ord_of_nat ` A. \<forall>y\<in>ord_of_nat ` A. (f x < f y) = ((x, y) \<in> VWF))
[PROOF STEP]
let ?M = "ord_of_nat ` A"
[PROOF STATE]
proof (state)
goal (6 subgoals):
 1. Ord (ord_of_nat (card A))
 2. wf VWF
 3. small (ord_of_nat ` A)
 4. total_on (ord_of_nat ` A) VWF
 5. trans VWF
 6. \<exists>f. bij_betw f (ord_of_nat ` A) (elts (ord_of_nat (card A))) \<and> (\<forall>x\<in>ord_of_nat ` A. \<forall>y\<in>ord_of_nat ` A. (f x < f y) = ((x, y) \<in> VWF))
[PROOF STEP]
obtain h where bijh: "bij_betw h {..<card A} ?M" and smh: "strict_mono_on {..<card A} h"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>h. \<lbrakk>bij_betw h {..<card A} (ord_of_nat ` A); strict_mono_on {..<card A} h\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis M card_image ex_bij_betw_strict_mono_card inj_on_def ord_of_nat_inject)
[PROOF STATE]
proof (state)
this:
bij_betw h {..<card A} (ord_of_nat ` A)
strict_mono_on {..<card A} h

goal (6 subgoals):
 1. Ord (ord_of_nat (card A))
 2. wf VWF
 3. small (ord_of_nat ` A)
 4. total_on (ord_of_nat ` A) VWF
 5. trans VWF
 6. \<exists>f. bij_betw f (ord_of_nat ` A) (elts (ord_of_nat (card A))) \<and> (\<forall>x\<in>ord_of_nat ` A. \<forall>y\<in>ord_of_nat ` A. (f x < f y) = ((x, y) \<in> VWF))
[PROOF STEP]
define f where "f \<equiv> ord_of_nat \<circ> inv_into {..<card A} h"
[PROOF STATE]
proof (state)
this:
f \<equiv> ord_of_nat \<circ> inv_into {..<card A} h

goal (6 subgoals):
 1. Ord (ord_of_nat (card A))
 2. wf VWF
 3. small (ord_of_nat ` A)
 4. total_on (ord_of_nat ` A) VWF
 5. trans VWF
 6. \<exists>f. bij_betw f (ord_of_nat ` A) (elts (ord_of_nat (card A))) \<and> (\<forall>x\<in>ord_of_nat ` A. \<forall>y\<in>ord_of_nat ` A. (f x < f y) = ((x, y) \<in> VWF))
[PROOF STEP]
show "\<exists>f. bij_betw f ?M (elts (card A)) \<and> (\<forall>x\<in>?M. \<forall>y\<in>?M. f x < f y \<longleftrightarrow> ((x, y) \<in> VWF))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>f. bij_betw f (ord_of_nat ` A) (elts (ord_of_nat (card A))) \<and> (\<forall>x\<in>ord_of_nat ` A. \<forall>y\<in>ord_of_nat ` A. (f x < f y) = ((x, y) \<in> VWF))
[PROOF STEP]
proof (intro exI conjI ballI)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. bij_betw ?f (ord_of_nat ` A) (elts (ord_of_nat (card A)))
 2. \<And>x y. \<lbrakk>x \<in> ord_of_nat ` A; y \<in> ord_of_nat ` A\<rbrakk> \<Longrightarrow> (?f x < ?f y) = ((x, y) \<in> VWF)
[PROOF STEP]
have "bij_betw (ord_of_nat \<circ> inv_into {..<card A} h) (ord_of_nat ` A) (ord_of_nat ` {..<card A})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bij_betw (ord_of_nat \<circ> inv_into {..<card A} h) (ord_of_nat ` A) (ord_of_nat ` {..<card A})
[PROOF STEP]
by (meson UNIV_I bijh bij_betw_def bij_betw_inv_into bij_betw_subset bij_betw_trans inj_ord_of_nat subsetI)
[PROOF STATE]
proof (state)
this:
bij_betw (ord_of_nat \<circ> inv_into {..<card A} h) (ord_of_nat ` A) (ord_of_nat ` {..<card A})

goal (2 subgoals):
 1. bij_betw ?f (ord_of_nat ` A) (elts (ord_of_nat (card A)))
 2. \<And>x y. \<lbrakk>x \<in> ord_of_nat ` A; y \<in> ord_of_nat ` A\<rbrakk> \<Longrightarrow> (?f x < ?f y) = ((x, y) \<in> VWF)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
bij_betw (ord_of_nat \<circ> inv_into {..<card A} h) (ord_of_nat ` A) (ord_of_nat ` {..<card A})
[PROOF STEP]
show "bij_betw f ?M (elts (card A))"
[PROOF STATE]
proof (prove)
using this:
bij_betw (ord_of_nat \<circ> inv_into {..<card A} h) (ord_of_nat ` A) (ord_of_nat ` {..<card A})

goal (1 subgoal):
 1. bij_betw f (ord_of_nat ` A) (elts (ord_of_nat (card A)))
[PROOF STEP]
by (metis elts_ord_of_nat f_def)
[PROOF STATE]
proof (state)
this:
bij_betw f (ord_of_nat ` A) (elts (ord_of_nat (card A)))

goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<in> ord_of_nat ` A; y \<in> ord_of_nat ` A\<rbrakk> \<Longrightarrow> (f x < f y) = ((x, y) \<in> VWF)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<in> ord_of_nat ` A; y \<in> ord_of_nat ` A\<rbrakk> \<Longrightarrow> (f x < f y) = ((x, y) \<in> VWF)
[PROOF STEP]
fix x y
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<in> ord_of_nat ` A; y \<in> ord_of_nat ` A\<rbrakk> \<Longrightarrow> (f x < f y) = ((x, y) \<in> VWF)
[PROOF STEP]
assume xy: "x \<in> ?M" "y \<in> ?M"
[PROOF STATE]
proof (state)
this:
x \<in> ord_of_nat ` A
y \<in> ord_of_nat ` A

goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<in> ord_of_nat ` A; y \<in> ord_of_nat ` A\<rbrakk> \<Longrightarrow> (f x < f y) = ((x, y) \<in> VWF)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x \<in> ord_of_nat ` A
y \<in> ord_of_nat ` A
[PROOF STEP]
obtain m n where "x = ord_of_nat m" "y = ord_of_nat n"
[PROOF STATE]
proof (prove)
using this:
x \<in> ord_of_nat ` A
y \<in> ord_of_nat ` A

goal (1 subgoal):
 1. (\<And>m n. \<lbrakk>x = ord_of_nat m; y = ord_of_nat n\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x = ord_of_nat m
y = ord_of_nat n

goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<in> ord_of_nat ` A; y \<in> ord_of_nat ` A\<rbrakk> \<Longrightarrow> (f x < f y) = ((x, y) \<in> VWF)
[PROOF STEP]
have "(f x < f y) \<longleftrightarrow> ((h \<circ> inv_into {..<card A} h) x < (h \<circ> inv_into {..<card A} h) y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (f x < f y) = ((h \<circ> inv_into {..<card A} h) x < (h \<circ> inv_into {..<card A} h) y)
[PROOF STEP]
unfolding f_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((ord_of_nat \<circ> inv_into {..<card A} h) x < (ord_of_nat \<circ> inv_into {..<card A} h) y) = ((h \<circ> inv_into {..<card A} h) x < (h \<circ> inv_into {..<card A} h) y)
[PROOF STEP]
using smh bij_betw_imp_surj_on [OF bijh]
[PROOF STATE]
proof (prove)
using this:
strict_mono_on {..<card A} h
h ` {..<card A} = ord_of_nat ` A

goal (1 subgoal):
 1. ((ord_of_nat \<circ> inv_into {..<card A} h) x < (ord_of_nat \<circ> inv_into {..<card A} h) y) = ((h \<circ> inv_into {..<card A} h) x < (h \<circ> inv_into {..<card A} h) y)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>strict_mono_on {..<card A} h; h ` {..<card A} = ord_of_nat ` A\<rbrakk> \<Longrightarrow> (inv_into {..<card A} h x < inv_into {..<card A} h y) = (h (inv_into {..<card A} h x) < h (inv_into {..<card A} h y))
[PROOF STEP]
by (metis (mono_tags, lifting) inv_into_into not_less_iff_gr_or_eq order.asym strict_mono_onD xy)
[PROOF STATE]
proof (state)
this:
(f x < f y) = ((h \<circ> inv_into {..<card A} h) x < (h \<circ> inv_into {..<card A} h) y)

goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<in> ord_of_nat ` A; y \<in> ord_of_nat ` A\<rbrakk> \<Longrightarrow> (f x < f y) = ((x, y) \<in> VWF)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(f x < f y) = ((h \<circ> inv_into {..<card A} h) x < (h \<circ> inv_into {..<card A} h) y)

goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<in> ord_of_nat ` A; y \<in> ord_of_nat ` A\<rbrakk> \<Longrightarrow> (f x < f y) = ((x, y) \<in> VWF)
[PROOF STEP]
have "\<dots> = (x < y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((h \<circ> inv_into {..<card A} h) x < (h \<circ> inv_into {..<card A} h) y) = (x < y)
[PROOF STEP]
using bijh
[PROOF STATE]
proof (prove)
using this:
bij_betw h {..<card A} (ord_of_nat ` A)

goal (1 subgoal):
 1. ((h \<circ> inv_into {..<card A} h) x < (h \<circ> inv_into {..<card A} h) y) = (x < y)
[PROOF STEP]
by (simp add: bij_betw_inv_into_right xy)
[PROOF STATE]
proof (state)
this:
((h \<circ> inv_into {..<card A} h) x < (h \<circ> inv_into {..<card A} h) y) = (x < y)

goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<in> ord_of_nat ` A; y \<in> ord_of_nat ` A\<rbrakk> \<Longrightarrow> (f x < f y) = ((x, y) \<in> VWF)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
((h \<circ> inv_into {..<card A} h) x < (h \<circ> inv_into {..<card A} h) y) = (x < y)

goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<in> ord_of_nat ` A; y \<in> ord_of_nat ` A\<rbrakk> \<Longrightarrow> (f x < f y) = ((x, y) \<in> VWF)
[PROOF STEP]
have "\<dots> \<longleftrightarrow> ((x, y) \<in> VWF)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x < y) = ((x, y) \<in> VWF)
[PROOF STEP]
using M(2) ON_imp_Ord xy
[PROOF STATE]
proof (prove)
using this:
ord_of_nat ` A \<subseteq> ON
\<lbrakk>?H \<subseteq> ON; ?x \<in> ?H\<rbrakk> \<Longrightarrow> Ord ?x
x \<in> ord_of_nat ` A
y \<in> ord_of_nat ` A

goal (1 subgoal):
 1. (x < y) = ((x, y) \<in> VWF)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(x < y) = ((x, y) \<in> VWF)

goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<in> ord_of_nat ` A; y \<in> ord_of_nat ` A\<rbrakk> \<Longrightarrow> (f x < f y) = ((x, y) \<in> VWF)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(f x < f y) = ((x, y) \<in> VWF)
[PROOF STEP]
show "(f x < f y) \<longleftrightarrow> ((x, y) \<in> VWF)"
[PROOF STATE]
proof (prove)
using this:
(f x < f y) = ((x, y) \<in> VWF)

goal (1 subgoal):
 1. (f x < f y) = ((x, y) \<in> VWF)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
(f x < f y) = ((x, y) \<in> VWF)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>f. bij_betw f (ord_of_nat ` A) (elts (ord_of_nat (card A))) \<and> (\<forall>x\<in>ord_of_nat ` A. \<forall>y\<in>ord_of_nat ` A. (f x < f y) = ((x, y) \<in> VWF))

goal (5 subgoals):
 1. Ord (ord_of_nat (card A))
 2. wf VWF
 3. small (ord_of_nat ` A)
 4. total_on (ord_of_nat ` A) VWF
 5. trans VWF
[PROOF STEP]
qed auto
[PROOF STATE]
proof (state)
this:
ordertype (ord_of_nat ` A) VWF = ord_of_nat (card A)

goal (1 subgoal):
 1. ordertype A less_than = ord_of_nat (card A)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
ordertype A less_than = ord_of_nat (card A)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
ordertype A less_than = ord_of_nat (card A)

goal (1 subgoal):
 1. ordertype A less_than = ord_of_nat (card A)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
ordertype A less_than = ord_of_nat (card A)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma gcard_eq_vcard [simp]: "gcard (elts x) = vcard x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. gcard (elts x) = vcard x
[PROOF STEP]
by (simp add: vcard_def gcard_def)


[STATEMENT]
lemma cardinal_cong: "elts x \<approx> elts y \<Longrightarrow> vcard x = vcard y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. elts x \<approx> elts y \<Longrightarrow> vcard x = vcard y
[PROOF STEP]
unfolding vcard_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. elts x \<approx> elts y \<Longrightarrow> (LEAST i. Ord i \<and> elts i \<approx> elts x) = (LEAST i. Ord i \<and> elts i \<approx> elts y)
[PROOF STEP]
by (meson eqpoll_sym eqpoll_trans)


[STATEMENT]
lemma gcardinal_cong:
  assumes "X \<approx> Y" shows "gcard X = gcard Y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. gcard X = gcard Y
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. gcard X = gcard Y
[PROOF STEP]
have "(LEAST i. Ord i \<and> elts i \<approx> X) = (LEAST i. Ord i \<and> elts i \<approx> Y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (LEAST i. Ord i \<and> elts i \<approx> X) = (LEAST i. Ord i \<and> elts i \<approx> Y)
[PROOF STEP]
by (meson eqpoll_sym eqpoll_trans assms)
[PROOF STATE]
proof (state)
this:
(LEAST i. Ord i \<and> elts i \<approx> X) = (LEAST i. Ord i \<and> elts i \<approx> Y)

goal (1 subgoal):
 1. gcard X = gcard Y
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(LEAST i. Ord i \<and> elts i \<approx> X) = (LEAST i. Ord i \<and> elts i \<approx> Y)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(LEAST i. Ord i \<and> elts i \<approx> X) = (LEAST i. Ord i \<and> elts i \<approx> Y)

goal (1 subgoal):
 1. gcard X = gcard Y
[PROOF STEP]
unfolding gcard_def
[PROOF STATE]
proof (prove)
using this:
(LEAST i. Ord i \<and> elts i \<approx> X) = (LEAST i. Ord i \<and> elts i \<approx> Y)

goal (1 subgoal):
 1. (if small X then LEAST i. Ord i \<and> elts i \<approx> X else 0) = (if small Y then LEAST i. Ord i \<and> elts i \<approx> Y else 0)
[PROOF STEP]
by (meson eqpoll_sym small_eqcong assms)
[PROOF STATE]
proof (state)
this:
gcard X = gcard Y

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma vcard_set_image: "inj_on f (elts x) \<Longrightarrow> vcard (set (f ` elts x)) = vcard x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inj_on f (elts x) \<Longrightarrow> vcard (set (f ` elts x)) = vcard x
[PROOF STEP]
by (simp add: cardinal_cong)


[STATEMENT]
lemma gcard_image: "inj_on f X \<Longrightarrow> gcard (f ` X) = gcard X"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inj_on f X \<Longrightarrow> gcard (f ` X) = gcard X
[PROOF STEP]
by (simp add: gcardinal_cong)


[STATEMENT]
lemma Card_cardinal_eq: "Card \<kappa> \<Longrightarrow> vcard \<kappa> = \<kappa>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Card \<kappa> \<Longrightarrow> vcard \<kappa> = \<kappa>
[PROOF STEP]
by (simp add: Card_def)


[STATEMENT]
lemma Card_is_Ord:
  assumes "Card \<kappa>" shows "Ord \<kappa>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Ord \<kappa>
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Ord \<kappa>
[PROOF STEP]
obtain \<alpha> where "Ord \<alpha>" "elts \<alpha> \<approx> elts \<kappa>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>\<alpha>. \<lbrakk>Ord \<alpha>; elts \<alpha> \<approx> elts \<kappa>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using Ord_ordertype ordertype_eqpoll
[PROOF STATE]
proof (prove)
using this:
Ord (ordertype ?A VWF)
small ?A \<Longrightarrow> elts (ordertype ?A VWF) \<approx> ?A

goal (1 subgoal):
 1. (\<And>\<alpha>. \<lbrakk>Ord \<alpha>; elts \<alpha> \<approx> elts \<kappa>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
Ord \<alpha>
elts \<alpha> \<approx> elts \<kappa>

goal (1 subgoal):
 1. Ord \<kappa>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Ord \<alpha>
elts \<alpha> \<approx> elts \<kappa>
[PROOF STEP]
have "Ord (LEAST i. Ord i \<and> elts i \<approx> elts \<kappa>)"
[PROOF STATE]
proof (prove)
using this:
Ord \<alpha>
elts \<alpha> \<approx> elts \<kappa>

goal (1 subgoal):
 1. Ord (LEAST i. Ord i \<and> elts i \<approx> elts \<kappa>)
[PROOF STEP]
by (metis Ord_Least)
[PROOF STATE]
proof (state)
this:
Ord (LEAST i. Ord i \<and> elts i \<approx> elts \<kappa>)

goal (1 subgoal):
 1. Ord \<kappa>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Ord (LEAST i. Ord i \<and> elts i \<approx> elts \<kappa>)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
Ord (LEAST i. Ord i \<and> elts i \<approx> elts \<kappa>)

goal (1 subgoal):
 1. Ord \<kappa>
[PROOF STEP]
using Card_def vcard_def assms
[PROOF STATE]
proof (prove)
using this:
Ord (LEAST i. Ord i \<and> elts i \<approx> elts \<kappa>)
Card ?i \<equiv> ?i = vcard ?i
vcard ?a \<equiv> LEAST i. Ord i \<and> elts i \<approx> elts ?a
Card \<kappa>

goal (1 subgoal):
 1. Ord \<kappa>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Ord \<kappa>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma cardinal_eqpoll: "elts (vcard a) \<approx> elts a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. elts (vcard a) \<approx> elts a
[PROOF STEP]
unfolding vcard_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. elts (LEAST i. Ord i \<and> elts i \<approx> elts a) \<approx> elts a
[PROOF STEP]
using ordertype_eqpoll [of "elts a"] Ord_LeastI
[PROOF STATE]
proof (prove)
using this:
small (elts a) \<Longrightarrow> elts (ordertype (elts a) VWF) \<approx> elts a
\<lbrakk>Ord ?k; ?P ?k\<rbrakk> \<Longrightarrow> ?P (LEAST i. Ord i \<and> ?P i)

goal (1 subgoal):
 1. elts (LEAST i. Ord i \<and> elts i \<approx> elts a) \<approx> elts a
[PROOF STEP]
by (meson Ord_ordertype small_elts)


[STATEMENT]
lemma inj_into_vcard:
  obtains f where "f \<in> elts A \<rightarrow> elts (vcard A)" "inj_on f (elts A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>f. \<lbrakk>f \<in> elts A \<rightarrow> elts (vcard A); inj_on f (elts A)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using cardinal_eqpoll [of A] inj_on_the_inv_into the_inv_into_onto
[PROOF STATE]
proof (prove)
using this:
elts (vcard A) \<approx> elts A
inj_on ?f ?A \<Longrightarrow> inj_on (the_inv_into ?A ?f) (?f ` ?A)
inj_on ?f ?A \<Longrightarrow> the_inv_into ?A ?f ` ?f ` ?A = ?A

goal (1 subgoal):
 1. (\<And>f. \<lbrakk>f \<in> elts A \<rightarrow> elts (vcard A); inj_on f (elts A)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (fastforce simp: Pi_iff bij_betw_def eqpoll_def)


[STATEMENT]
lemma cardinal_idem [simp]: "vcard (vcard a) = vcard a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vcard (vcard a) = vcard a
[PROOF STEP]
using cardinal_cong cardinal_eqpoll
[PROOF STATE]
proof (prove)
using this:
elts ?x \<approx> elts ?y \<Longrightarrow> vcard ?x = vcard ?y
elts (vcard ?a) \<approx> elts ?a

goal (1 subgoal):
 1. vcard (vcard a) = vcard a
[PROOF STEP]
by blast


[STATEMENT]
lemma subset_smaller_vcard:
  assumes "\<kappa> \<le> vcard x" "Card \<kappa>"
  obtains y where "y \<le> x" "vcard y = \<kappa>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>y. \<lbrakk>y \<le> x; vcard y = \<kappa>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<And>y. \<lbrakk>y \<le> x; vcard y = \<kappa>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
obtain \<phi> where \<phi>: "bij_betw \<phi> (elts (vcard x)) (elts x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>\<phi>. bij_betw \<phi> (elts (vcard x)) (elts x) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using cardinal_eqpoll eqpoll_def
[PROOF STATE]
proof (prove)
using this:
elts (vcard ?a) \<approx> elts ?a
?A \<approx> ?B \<equiv> \<exists>f. bij_betw f ?A ?B

goal (1 subgoal):
 1. (\<And>\<phi>. bij_betw \<phi> (elts (vcard x)) (elts x) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
bij_betw \<phi> (elts (vcard x)) (elts x)

goal (1 subgoal):
 1. (\<And>y. \<lbrakk>y \<le> x; vcard y = \<kappa>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
show thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. thesis
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ?y \<le> x
 2. vcard ?y = \<kappa>
[PROOF STEP]
let ?y = "ZFC_in_HOL.set (\<phi> ` elts \<kappa>)"
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ?y \<le> x
 2. vcard ?y = \<kappa>
[PROOF STEP]
show "?y \<le> x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set (\<phi> ` elts \<kappa>) \<le> x
[PROOF STEP]
by (meson \<phi> assms bij_betwE set_image_le_iff small_elts vsubsetD)
[PROOF STATE]
proof (state)
this:
set (\<phi> ` elts \<kappa>) \<le> x

goal (1 subgoal):
 1. vcard (set (\<phi> ` elts \<kappa>)) = \<kappa>
[PROOF STEP]
show "vcard ?y = \<kappa>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vcard (set (\<phi> ` elts \<kappa>)) = \<kappa>
[PROOF STEP]
by (metis vcard_set_image Card_def assms bij_betw_def bij_betw_subset \<phi> less_eq_V_def)
[PROOF STATE]
proof (state)
this:
vcard (set (\<phi> ` elts \<kappa>)) = \<kappa>

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
thesis

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma nat_into_Card:
  assumes "\<alpha> \<in> elts \<omega>" shows "Card(\<alpha>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Card \<alpha>
[PROOF STEP]
proof (unfold Card_def vcard_def, rule sym)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (LEAST i. Ord i \<and> elts i \<approx> elts \<alpha>) = \<alpha>
[PROOF STEP]
obtain n where n: "\<alpha> = ord_of_nat n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>n. \<alpha> = ord_of_nat n \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis \<omega>_def assms elts_of_set imageE inf)
[PROOF STATE]
proof (state)
this:
\<alpha> = ord_of_nat n

goal (1 subgoal):
 1. (LEAST i. Ord i \<and> elts i \<approx> elts \<alpha>) = \<alpha>
[PROOF STEP]
have "Ord(\<alpha>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Ord \<alpha>
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<alpha> \<in> elts \<omega>

goal (1 subgoal):
 1. Ord \<alpha>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Ord \<alpha>

goal (1 subgoal):
 1. (LEAST i. Ord i \<and> elts i \<approx> elts \<alpha>) = \<alpha>
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
Ord \<alpha>

goal (1 subgoal):
 1. (LEAST i. Ord i \<and> elts i \<approx> elts \<alpha>) = \<alpha>
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
Ord \<alpha>

goal (1 subgoal):
 1. (LEAST i. Ord i \<and> elts i \<approx> elts \<alpha>) = \<alpha>
[PROOF STEP]
fix \<beta>
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (LEAST i. Ord i \<and> elts i \<approx> elts \<alpha>) = \<alpha>
[PROOF STEP]
assume "\<beta> < \<alpha>" "Ord \<beta>" "elts \<beta> \<approx> elts \<alpha>"
[PROOF STATE]
proof (state)
this:
\<beta> < \<alpha>
Ord \<beta>
elts \<beta> \<approx> elts \<alpha>

goal (1 subgoal):
 1. (LEAST i. Ord i \<and> elts i \<approx> elts \<alpha>) = \<alpha>
[PROOF STEP]
with n
[PROOF STATE]
proof (chain)
picking this:
\<alpha> = ord_of_nat n
\<beta> < \<alpha>
Ord \<beta>
elts \<beta> \<approx> elts \<alpha>
[PROOF STEP]
have "elts \<beta> \<approx> {..<n}"
[PROOF STATE]
proof (prove)
using this:
\<alpha> = ord_of_nat n
\<beta> < \<alpha>
Ord \<beta>
elts \<beta> \<approx> elts \<alpha>

goal (1 subgoal):
 1. elts \<beta> \<approx> {..<n}
[PROOF STEP]
by (simp add: ord_of_nat_eq_initial [of n] eqpoll_trans inj_on_def inj_on_image_eqpoll_self)
[PROOF STATE]
proof (state)
this:
elts \<beta> \<approx> {..<n}

goal (1 subgoal):
 1. (LEAST i. Ord i \<and> elts i \<approx> elts \<alpha>) = \<alpha>
[PROOF STEP]
hence False
[PROOF STATE]
proof (prove)
using this:
elts \<beta> \<approx> {..<n}

goal (1 subgoal):
 1. False
[PROOF STEP]
using assms n  \<open>Ord \<beta>\<close> \<open>\<beta> < \<alpha>\<close> \<open>Ord(\<alpha>)\<close>
[PROOF STATE]
proof (prove)
using this:
elts \<beta> \<approx> {..<n}
\<alpha> \<in> elts \<omega>
\<alpha> = ord_of_nat n
Ord \<beta>
\<beta> < \<alpha>
Ord \<alpha>

goal (1 subgoal):
 1. False
[PROOF STEP]
by (metis \<open>elts \<beta> \<approx> elts \<alpha>\<close> card_seteq eqpoll_finite_iff eqpoll_iff_card finite_lessThan less_eq_V_def less_le_not_le order_refl)
[PROOF STATE]
proof (state)
this:
False

goal (1 subgoal):
 1. (LEAST i. Ord i \<and> elts i \<approx> elts \<alpha>) = \<alpha>
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<lbrakk>?\<beta>2 < \<alpha>; Ord ?\<beta>2; elts ?\<beta>2 \<approx> elts \<alpha>\<rbrakk> \<Longrightarrow> False

goal (1 subgoal):
 1. (LEAST i. Ord i \<and> elts i \<approx> elts \<alpha>) = \<alpha>
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
Ord \<alpha>
\<lbrakk>?\<beta>2 < \<alpha>; Ord ?\<beta>2; elts ?\<beta>2 \<approx> elts \<alpha>\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
show "(LEAST i. Ord i \<and> elts i \<approx> elts \<alpha>) = \<alpha>"
[PROOF STATE]
proof (prove)
using this:
Ord \<alpha>
\<lbrakk>?\<beta>2 < \<alpha>; Ord ?\<beta>2; elts ?\<beta>2 \<approx> elts \<alpha>\<rbrakk> \<Longrightarrow> False

goal (1 subgoal):
 1. (LEAST i. Ord i \<and> elts i \<approx> elts \<alpha>) = \<alpha>
[PROOF STEP]
by (metis (no_types, lifting) Least_equality Ord_linear_le eqpoll_refl less_le_not_le)
[PROOF STATE]
proof (state)
this:
(LEAST i. Ord i \<and> elts i \<approx> elts \<alpha>) = \<alpha>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma Card_0 [iff]: "Card 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Card 0
[PROOF STEP]
by (simp add: nat_into_Card)


[STATEMENT]
lemma CardI: "\<lbrakk>Ord i; \<And>j. \<lbrakk>j < i; Ord j\<rbrakk> \<Longrightarrow> \<not> elts j \<approx> elts i\<rbrakk> \<Longrightarrow> Card i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Ord i; \<And>j. \<lbrakk>j < i; Ord j\<rbrakk> \<Longrightarrow> \<not> elts j \<approx> elts i\<rbrakk> \<Longrightarrow> Card i
[PROOF STEP]
unfolding Card_def vcard_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Ord i; \<And>j. \<lbrakk>j < i; Ord j\<rbrakk> \<Longrightarrow> \<not> elts j \<approx> elts i\<rbrakk> \<Longrightarrow> i = (LEAST ia. Ord ia \<and> elts ia \<approx> elts i)
[PROOF STEP]
by (metis Ord_Least Ord_linear_lt cardinal_eqpoll eqpoll_refl not_less_Ord_Least vcard_def)


[STATEMENT]
lemma vcard_0 [simp]: "vcard 0 = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vcard 0 = 0
[PROOF STEP]
using Card_0 Card_def
[PROOF STATE]
proof (prove)
using this:
Card 0
Card ?i \<equiv> ?i = vcard ?i

goal (1 subgoal):
 1. vcard 0 = 0
[PROOF STEP]
by auto


[STATEMENT]
lemma Ord_cardinal [simp,intro!]: "Ord(vcard a)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Ord (vcard a)
[PROOF STEP]
unfolding vcard_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Ord (LEAST i. Ord i \<and> elts i \<approx> elts a)
[PROOF STEP]
by (metis Card_def Card_is_Ord cardinal_cong cardinal_eqpoll vcard_def)


[STATEMENT]
lemma gcard_big_0: "\<not> small X \<Longrightarrow> gcard X = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> small X \<Longrightarrow> gcard X = 0
[PROOF STEP]
by (simp add: gcard_def)


[STATEMENT]
lemma gcard_eq_card:
  assumes "finite X" shows "gcard X = ord_of_nat (card X)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. gcard X = ord_of_nat (card X)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. gcard X = ord_of_nat (card X)
[PROOF STEP]
have "\<And>y. Ord y \<and> elts y \<approx> X \<Longrightarrow> ord_of_nat (card X) \<le> y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>y. Ord y \<and> elts y \<approx> X \<Longrightarrow> ord_of_nat (card X) \<le> y
[PROOF STEP]
by (metis assms eqpoll_finite_iff eqpoll_iff_card order_le_less ordertype_VWF_finite_nat ordertype_eq_Ord)
[PROOF STATE]
proof (state)
this:
Ord ?y \<and> elts ?y \<approx> X \<Longrightarrow> ord_of_nat (card X) \<le> ?y

goal (1 subgoal):
 1. gcard X = ord_of_nat (card X)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Ord ?y \<and> elts ?y \<approx> X \<Longrightarrow> ord_of_nat (card X) \<le> ?y
[PROOF STEP]
have "(LEAST i. Ord i \<and> elts i \<approx> X) = ord_of_nat (card X)"
[PROOF STATE]
proof (prove)
using this:
Ord ?y \<and> elts ?y \<approx> X \<Longrightarrow> ord_of_nat (card X) \<le> ?y

goal (1 subgoal):
 1. (LEAST i. Ord i \<and> elts i \<approx> X) = ord_of_nat (card X)
[PROOF STEP]
by (simp add: assms eqpoll_iff_card finite_Ord_omega Least_equality)
[PROOF STATE]
proof (state)
this:
(LEAST i. Ord i \<and> elts i \<approx> X) = ord_of_nat (card X)

goal (1 subgoal):
 1. gcard X = ord_of_nat (card X)
[PROOF STEP]
with assms
[PROOF STATE]
proof (chain)
picking this:
finite X
(LEAST i. Ord i \<and> elts i \<approx> X) = ord_of_nat (card X)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
finite X
(LEAST i. Ord i \<and> elts i \<approx> X) = ord_of_nat (card X)

goal (1 subgoal):
 1. gcard X = ord_of_nat (card X)
[PROOF STEP]
by (simp add: finite_imp_small gcard_def)
[PROOF STATE]
proof (state)
this:
gcard X = ord_of_nat (card X)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma gcard_empty_0 [simp]: "gcard {} = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. gcard {} = 0
[PROOF STEP]
by (simp add: gcard_eq_card)


[STATEMENT]
lemma gcard_single_1 [simp]: "gcard {x} = 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. gcard {x} = 1
[PROOF STEP]
by (simp add: gcard_eq_card one_V_def)


[STATEMENT]
lemma Card_gcard [iff]: "Card (gcard X)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Card (gcard X)
[PROOF STEP]
by (metis Card_0 Card_def cardinal_idem gcard_big_0 gcardinal_cong small_eqpoll gcard_eq_vcard)


[STATEMENT]
lemma gcard_eqpoll: "small X \<Longrightarrow> elts (gcard X) \<approx> X"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. small X \<Longrightarrow> elts (gcard X) \<approx> X
[PROOF STEP]
by (metis cardinal_eqpoll eqpoll_trans gcard_eq_vcard gcardinal_cong small_eqpoll)


[STATEMENT]
lemma lepoll_imp_gcard_le:
  assumes "A \<lesssim> B" "small B"
  shows "gcard A \<le> gcard B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. gcard A \<le> gcard B
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. gcard A \<le> gcard B
[PROOF STEP]
have "elts (gcard A) \<approx> A" "elts (gcard B) \<approx> B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. elts (gcard A) \<approx> A &&& elts (gcard B) \<approx> B
[PROOF STEP]
by (meson assms gcard_eqpoll lepoll_small)+
[PROOF STATE]
proof (state)
this:
elts (gcard A) \<approx> A
elts (gcard B) \<approx> B

goal (1 subgoal):
 1. gcard A \<le> gcard B
[PROOF STEP]
with \<open>A \<lesssim> B\<close>
[PROOF STATE]
proof (chain)
picking this:
A \<lesssim> B
elts (gcard A) \<approx> A
elts (gcard B) \<approx> B
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
A \<lesssim> B
elts (gcard A) \<approx> A
elts (gcard B) \<approx> B

goal (1 subgoal):
 1. gcard A \<le> gcard B
[PROOF STEP]
by (metis Ord_cardinal Ord_linear2 eqpoll_sym gcard_eq_vcard gcardinal_cong lepoll_antisym
              lepoll_trans2 less_V_def less_eq_V_def subset_imp_lepoll)
[PROOF STATE]
proof (state)
this:
gcard A \<le> gcard B

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma gcard_image_le:
  assumes "small A" shows "gcard (f ` A) \<le> gcard A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. gcard (f ` A) \<le> gcard A
[PROOF STEP]
using assms image_lepoll lepoll_imp_gcard_le
[PROOF STATE]
proof (prove)
using this:
small A
?f ` ?A \<lesssim> ?A
\<lbrakk>?A \<lesssim> ?B; small ?B\<rbrakk> \<Longrightarrow> gcard ?A \<le> gcard ?B

goal (1 subgoal):
 1. gcard (f ` A) \<le> gcard A
[PROOF STEP]
by blast


[STATEMENT]
lemma subset_imp_gcard_le:
  assumes "A \<subseteq> B" "small B"
  shows "gcard A \<le> gcard B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. gcard A \<le> gcard B
[PROOF STEP]
by (simp add: assms lepoll_imp_gcard_le subset_imp_lepoll)


[STATEMENT]
lemma gcard_le_lepoll: "\<lbrakk>gcard A \<le> \<alpha>; small A\<rbrakk> \<Longrightarrow> A \<lesssim> elts \<alpha>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>gcard A \<le> \<alpha>; small A\<rbrakk> \<Longrightarrow> A \<lesssim> elts \<alpha>
[PROOF STEP]
by (meson eqpoll_sym gcard_eqpoll lepoll_trans1 less_eq_V_def subset_imp_lepoll)


[STATEMENT]
lemma Card_iff_initial: "Card \<kappa> \<longleftrightarrow> Ord \<kappa> \<and> (\<forall>\<alpha>. Ord \<alpha> \<and> \<alpha> < \<kappa> \<longrightarrow> ~ elts \<alpha> \<approx> elts \<kappa>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Card \<kappa> = (Ord \<kappa> \<and> (\<forall>\<alpha>. Ord \<alpha> \<and> \<alpha> < \<kappa> \<longrightarrow> \<not> elts \<alpha> \<approx> elts \<kappa>))
[PROOF STEP]
by (metis CardI Card_def Card_is_Ord not_less_Ord_Least vcard_def)


[STATEMENT]
lemma Card_\<omega> [iff]: "Card \<omega>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Card \<omega>
[PROOF STEP]
by (meson CardI Ord_\<omega> eqpoll_finite_iff infinite_Ord_omega infinite_\<omega> leD)


[STATEMENT]
lemma lt_Card_imp_lesspoll: "\<lbrakk>i < a; Card a; Ord i\<rbrakk> \<Longrightarrow> elts i \<prec> elts a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>i < a; Card a; Ord i\<rbrakk> \<Longrightarrow> elts i \<prec> elts a
[PROOF STEP]
by (meson Card_iff_initial less_eq_V_def less_imp_le lesspoll_def subset_imp_lepoll)


[STATEMENT]
lemma lepoll_imp_Card_le:
  assumes "elts a \<lesssim> elts b" shows "vcard a \<le> vcard b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vcard a \<le> vcard b
[PROOF STEP]
using assms lepoll_imp_gcard_le
[PROOF STATE]
proof (prove)
using this:
elts a \<lesssim> elts b
\<lbrakk>?A \<lesssim> ?B; small ?B\<rbrakk> \<Longrightarrow> gcard ?A \<le> gcard ?B

goal (1 subgoal):
 1. vcard a \<le> vcard b
[PROOF STEP]
by fastforce


[STATEMENT]
lemma lepoll_cardinal_le: "\<lbrakk>elts A \<lesssim> elts i; Ord i\<rbrakk> \<Longrightarrow> vcard A \<le> i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>elts A \<lesssim> elts i; Ord i\<rbrakk> \<Longrightarrow> vcard A \<le> i
[PROOF STEP]
by (metis Ord_Least Ord_linear2 dual_order.trans eqpoll_refl lepoll_imp_Card_le not_less_Ord_Least vcard_def)


[STATEMENT]
lemma cardinal_le_lepoll: "vcard A \<le> \<alpha> \<Longrightarrow> elts A \<lesssim> elts \<alpha>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vcard A \<le> \<alpha> \<Longrightarrow> elts A \<lesssim> elts \<alpha>
[PROOF STEP]
by (meson cardinal_eqpoll eqpoll_sym lepoll_trans1 less_eq_V_def subset_imp_lepoll)


[STATEMENT]
lemma lesspoll_imp_Card_less:
  assumes "elts a \<prec> elts b" shows "vcard a < vcard b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vcard a < vcard b
[PROOF STEP]
by (metis assms cardinal_eqpoll eqpoll_sym eqpoll_trans lepoll_imp_Card_le less_V_def lesspoll_def)


[STATEMENT]
lemma Card_Union [simp,intro]:
  assumes A: "\<And>x. x \<in> A \<Longrightarrow> Card(x)" shows "Card(\<Squnion>A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Card (\<Squnion> A)
[PROOF STEP]
proof (rule CardI)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. Ord (\<Squnion> A)
 2. \<And>j. \<lbrakk>j < \<Squnion> A; Ord j\<rbrakk> \<Longrightarrow> \<not> elts j \<approx> elts (\<Squnion> A)
[PROOF STEP]
show "Ord(\<Squnion>A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Ord (\<Squnion> A)
[PROOF STEP]
using A
[PROOF STATE]
proof (prove)
using this:
?x \<in> A \<Longrightarrow> Card ?x

goal (1 subgoal):
 1. Ord (\<Squnion> A)
[PROOF STEP]
by (simp add: Card_is_Ord Ord_Sup)
[PROOF STATE]
proof (state)
this:
Ord (\<Squnion> A)

goal (1 subgoal):
 1. \<And>j. \<lbrakk>j < \<Squnion> A; Ord j\<rbrakk> \<Longrightarrow> \<not> elts j \<approx> elts (\<Squnion> A)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>j. \<lbrakk>j < \<Squnion> A; Ord j\<rbrakk> \<Longrightarrow> \<not> elts j \<approx> elts (\<Squnion> A)
[PROOF STEP]
fix j
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>j. \<lbrakk>j < \<Squnion> A; Ord j\<rbrakk> \<Longrightarrow> \<not> elts j \<approx> elts (\<Squnion> A)
[PROOF STEP]
assume j: "j < \<Squnion>A" "Ord j"
[PROOF STATE]
proof (state)
this:
j < \<Squnion> A
Ord j

goal (1 subgoal):
 1. \<And>j. \<lbrakk>j < \<Squnion> A; Ord j\<rbrakk> \<Longrightarrow> \<not> elts j \<approx> elts (\<Squnion> A)
[PROOF STEP]
hence "\<exists>c\<in>A. j < c \<and> Card(c)"
[PROOF STATE]
proof (prove)
using this:
j < \<Squnion> A
Ord j

goal (1 subgoal):
 1. \<exists>c\<in>A. j < c \<and> Card c
[PROOF STEP]
using A
[PROOF STATE]
proof (prove)
using this:
j < \<Squnion> A
Ord j
?x \<in> A \<Longrightarrow> Card ?x

goal (1 subgoal):
 1. \<exists>c\<in>A. j < c \<and> Card c
[PROOF STEP]
by (meson Card_is_Ord Ord_linear2 ZFC_in_HOL.Sup_least leD)
[PROOF STATE]
proof (state)
this:
\<exists>c\<in>A. j < c \<and> Card c

goal (1 subgoal):
 1. \<And>j. \<lbrakk>j < \<Squnion> A; Ord j\<rbrakk> \<Longrightarrow> \<not> elts j \<approx> elts (\<Squnion> A)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>c\<in>A. j < c \<and> Card c
[PROOF STEP]
obtain c where c: "c\<in>A" "j < c" "Card(c)"
[PROOF STATE]
proof (prove)
using this:
\<exists>c\<in>A. j < c \<and> Card c

goal (1 subgoal):
 1. (\<And>c. \<lbrakk>c \<in> A; j < c; Card c\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
c \<in> A
j < c
Card c

goal (1 subgoal):
 1. \<And>j. \<lbrakk>j < \<Squnion> A; Ord j\<rbrakk> \<Longrightarrow> \<not> elts j \<approx> elts (\<Squnion> A)
[PROOF STEP]
hence jls: "elts j \<prec> elts c"
[PROOF STATE]
proof (prove)
using this:
c \<in> A
j < c
Card c

goal (1 subgoal):
 1. elts j \<prec> elts c
[PROOF STEP]
using j(2) lt_Card_imp_lesspoll
[PROOF STATE]
proof (prove)
using this:
c \<in> A
j < c
Card c
Ord j
\<lbrakk>?i < ?a; Card ?a; Ord ?i\<rbrakk> \<Longrightarrow> elts ?i \<prec> elts ?a

goal (1 subgoal):
 1. elts j \<prec> elts c
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
elts j \<prec> elts c

goal (1 subgoal):
 1. \<And>j. \<lbrakk>j < \<Squnion> A; Ord j\<rbrakk> \<Longrightarrow> \<not> elts j \<approx> elts (\<Squnion> A)
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
elts j \<prec> elts c

goal (1 subgoal):
 1. \<And>j. \<lbrakk>j < \<Squnion> A; Ord j\<rbrakk> \<Longrightarrow> \<not> elts j \<approx> elts (\<Squnion> A)
[PROOF STEP]
assume eqp: "elts j \<approx> elts (\<Squnion>A)"
[PROOF STATE]
proof (state)
this:
elts j \<approx> elts (\<Squnion> A)

goal (1 subgoal):
 1. \<And>j. \<lbrakk>j < \<Squnion> A; Ord j\<rbrakk> \<Longrightarrow> \<not> elts j \<approx> elts (\<Squnion> A)
[PROOF STEP]
have  "elts c \<lesssim> elts (\<Squnion>A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. elts c \<lesssim> elts (\<Squnion> A)
[PROOF STEP]
using c
[PROOF STATE]
proof (prove)
using this:
c \<in> A
j < c
Card c

goal (1 subgoal):
 1. elts c \<lesssim> elts (\<Squnion> A)
[PROOF STEP]
by (metis Card_def Sup_V_def ZFC_in_HOL.Sup_upper cardinal_le_lepoll j(1) not_less_0)
[PROOF STATE]
proof (state)
this:
elts c \<lesssim> elts (\<Squnion> A)

goal (1 subgoal):
 1. \<And>j. \<lbrakk>j < \<Squnion> A; Ord j\<rbrakk> \<Longrightarrow> \<not> elts j \<approx> elts (\<Squnion> A)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
elts c \<lesssim> elts (\<Squnion> A)

goal (1 subgoal):
 1. \<And>j. \<lbrakk>j < \<Squnion> A; Ord j\<rbrakk> \<Longrightarrow> \<not> elts j \<approx> elts (\<Squnion> A)
[PROOF STEP]
have "... \<approx> elts j"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. elts (\<Squnion> A) \<approx> elts j
[PROOF STEP]
by (rule eqpoll_sym [OF eqp])
[PROOF STATE]
proof (state)
this:
elts (\<Squnion> A) \<approx> elts j

goal (1 subgoal):
 1. \<And>j. \<lbrakk>j < \<Squnion> A; Ord j\<rbrakk> \<Longrightarrow> \<not> elts j \<approx> elts (\<Squnion> A)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
elts (\<Squnion> A) \<approx> elts j

goal (1 subgoal):
 1. \<And>j. \<lbrakk>j < \<Squnion> A; Ord j\<rbrakk> \<Longrightarrow> \<not> elts j \<approx> elts (\<Squnion> A)
[PROOF STEP]
have "... \<prec> elts c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. elts j \<prec> elts c
[PROOF STEP]
by (rule jls)
[PROOF STATE]
proof (state)
this:
elts j \<prec> elts c

goal (1 subgoal):
 1. \<And>j. \<lbrakk>j < \<Squnion> A; Ord j\<rbrakk> \<Longrightarrow> \<not> elts j \<approx> elts (\<Squnion> A)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
elts c \<prec> elts c
[PROOF STEP]
have "elts c \<prec> elts c"
[PROOF STATE]
proof (prove)
using this:
elts c \<prec> elts c

goal (1 subgoal):
 1. elts c \<prec> elts c
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
elts c \<prec> elts c

goal (1 subgoal):
 1. \<And>j. \<lbrakk>j < \<Squnion> A; Ord j\<rbrakk> \<Longrightarrow> \<not> elts j \<approx> elts (\<Squnion> A)
[PROOF STEP]
hence False
[PROOF STATE]
proof (prove)
using this:
elts c \<prec> elts c

goal (1 subgoal):
 1. False
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
False

goal (1 subgoal):
 1. \<And>j. \<lbrakk>j < \<Squnion> A; Ord j\<rbrakk> \<Longrightarrow> \<not> elts j \<approx> elts (\<Squnion> A)
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
elts j \<approx> elts (\<Squnion> A) \<Longrightarrow> False

goal (1 subgoal):
 1. \<And>j. \<lbrakk>j < \<Squnion> A; Ord j\<rbrakk> \<Longrightarrow> \<not> elts j \<approx> elts (\<Squnion> A)
[PROOF STEP]
thus "\<not> elts j \<approx> elts (\<Squnion>A)"
[PROOF STATE]
proof (prove)
using this:
elts j \<approx> elts (\<Squnion> A) \<Longrightarrow> False

goal (1 subgoal):
 1. \<not> elts j \<approx> elts (\<Squnion> A)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<not> elts j \<approx> elts (\<Squnion> A)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma Card_UN: "(\<And>x. x \<in> A \<Longrightarrow> Card(K x)) ==> Card(Sup (K ` A))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>x. x \<in> A \<Longrightarrow> Card (K x)) \<Longrightarrow> Card (\<Squnion> (K ` A))
[PROOF STEP]
by blast


[STATEMENT]
lemma transrec3_0 [simp]: "transrec3 a b c 0 = a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. transrec3 a b c 0 = a
[PROOF STEP]
by (simp add: transrec transrec3_def)


[STATEMENT]
lemma transrec3_succ [simp]:
     "transrec3 a b c (succ i) = b i (transrec3 a b c i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. transrec3 a b c (ZFC_in_HOL.succ i) = b i (transrec3 a b c i)
[PROOF STEP]
by (simp add: transrec transrec3_def)


[STATEMENT]
lemma transrec3_Limit [simp]:
     "Limit i \<Longrightarrow>  transrec3 a b c i = c i (\<lambda>j \<in> elts i. transrec3 a b c j)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Limit i \<Longrightarrow> transrec3 a b c i = c i (restrict (transrec3 a b c) (elts i))
[PROOF STEP]
unfolding transrec3_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Limit i \<Longrightarrow> transrec (\<lambda>r x. if x = 0 then a else if Limit x then c x (restrict r (elts x)) else b (ZFC_in_HOL.pred x) (r (ZFC_in_HOL.pred x))) i = c i (restrict (transrec (\<lambda>r x. if x = 0 then a else if Limit x then c x (restrict r (elts x)) else b (ZFC_in_HOL.pred x) (r (ZFC_in_HOL.pred x)))) (elts i))
[PROOF STEP]
by (subst transrec) auto


[STATEMENT]
lemma vsum_commute_eqpoll: "elts (a\<Uplus>b) \<approx> elts (b\<Uplus>a)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. elts (a \<Uplus> b) \<approx> elts (b \<Uplus> a)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. elts (a \<Uplus> b) \<approx> elts (b \<Uplus> a)
[PROOF STEP]
have "bij_betw (\<lambda>z \<in> elts (a\<Uplus>b). sum_case Inr Inl z) (elts (a\<Uplus>b)) (elts (b\<Uplus>a))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bij_betw (restrict (sum_case ZFC_Cardinals.Inr ZFC_Cardinals.Inl) (elts (a \<Uplus> b))) (elts (a \<Uplus> b)) (elts (b \<Uplus> a))
[PROOF STEP]
unfolding bij_betw_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inj_on (restrict (sum_case ZFC_Cardinals.Inr ZFC_Cardinals.Inl) (elts (a \<Uplus> b))) (elts (a \<Uplus> b)) \<and> restrict (sum_case ZFC_Cardinals.Inr ZFC_Cardinals.Inl) (elts (a \<Uplus> b)) ` elts (a \<Uplus> b) = elts (b \<Uplus> a)
[PROOF STEP]
proof (intro conjI inj_onI)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x y. \<lbrakk>x \<in> elts (a \<Uplus> b); y \<in> elts (a \<Uplus> b); restrict (sum_case ZFC_Cardinals.Inr ZFC_Cardinals.Inl) (elts (a \<Uplus> b)) x = restrict (sum_case ZFC_Cardinals.Inr ZFC_Cardinals.Inl) (elts (a \<Uplus> b)) y\<rbrakk> \<Longrightarrow> x = y
 2. restrict (sum_case ZFC_Cardinals.Inr ZFC_Cardinals.Inl) (elts (a \<Uplus> b)) ` elts (a \<Uplus> b) = elts (b \<Uplus> a)
[PROOF STEP]
show "restrict (sum_case Inr Inl) (elts (a \<Uplus> b)) ` elts (a \<Uplus> b) = elts (b \<Uplus> a)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. restrict (sum_case ZFC_Cardinals.Inr ZFC_Cardinals.Inl) (elts (a \<Uplus> b)) ` elts (a \<Uplus> b) = elts (b \<Uplus> a)
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>xa. xa \<in> elts b \<Longrightarrow> ZFC_Cardinals.Inl xa \<in> sum_case ZFC_Cardinals.Inr ZFC_Cardinals.Inl ` elts (a \<Uplus> b)
 2. \<And>y. y \<in> elts a \<Longrightarrow> ZFC_Cardinals.Inr y \<in> sum_case ZFC_Cardinals.Inr ZFC_Cardinals.Inl ` elts (a \<Uplus> b)
[PROOF STEP]
apply (metis (no_types) imageI sum_case_Inr sum_iff)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>y. y \<in> elts a \<Longrightarrow> ZFC_Cardinals.Inr y \<in> sum_case ZFC_Cardinals.Inr ZFC_Cardinals.Inl ` elts (a \<Uplus> b)
[PROOF STEP]
by (metis Inl_in_sum_iff imageI sum_case_Inl)
[PROOF STATE]
proof (state)
this:
restrict (sum_case ZFC_Cardinals.Inr ZFC_Cardinals.Inl) (elts (a \<Uplus> b)) ` elts (a \<Uplus> b) = elts (b \<Uplus> a)

goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<in> elts (a \<Uplus> b); y \<in> elts (a \<Uplus> b); restrict (sum_case ZFC_Cardinals.Inr ZFC_Cardinals.Inl) (elts (a \<Uplus> b)) x = restrict (sum_case ZFC_Cardinals.Inr ZFC_Cardinals.Inl) (elts (a \<Uplus> b)) y\<rbrakk> \<Longrightarrow> x = y
[PROOF STEP]
qed auto
[PROOF STATE]
proof (state)
this:
bij_betw (restrict (sum_case ZFC_Cardinals.Inr ZFC_Cardinals.Inl) (elts (a \<Uplus> b))) (elts (a \<Uplus> b)) (elts (b \<Uplus> a))

goal (1 subgoal):
 1. elts (a \<Uplus> b) \<approx> elts (b \<Uplus> a)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
bij_betw (restrict (sum_case ZFC_Cardinals.Inr ZFC_Cardinals.Inl) (elts (a \<Uplus> b))) (elts (a \<Uplus> b)) (elts (b \<Uplus> a))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
bij_betw (restrict (sum_case ZFC_Cardinals.Inr ZFC_Cardinals.Inl) (elts (a \<Uplus> b))) (elts (a \<Uplus> b)) (elts (b \<Uplus> a))

goal (1 subgoal):
 1. elts (a \<Uplus> b) \<approx> elts (b \<Uplus> a)
[PROOF STEP]
using eqpoll_def
[PROOF STATE]
proof (prove)
using this:
bij_betw (restrict (sum_case ZFC_Cardinals.Inr ZFC_Cardinals.Inl) (elts (a \<Uplus> b))) (elts (a \<Uplus> b)) (elts (b \<Uplus> a))
?A \<approx> ?B \<equiv> \<exists>f. bij_betw f ?A ?B

goal (1 subgoal):
 1. elts (a \<Uplus> b) \<approx> elts (b \<Uplus> a)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
elts (a \<Uplus> b) \<approx> elts (b \<Uplus> a)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma cadd_commute: "i \<oplus> j = j \<oplus> i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i \<oplus> j = j \<oplus> i
[PROOF STEP]
by (simp add: cadd_def cardinal_cong vsum_commute_eqpoll)


[STATEMENT]
lemma sum_assoc_bij:
  "bij_betw (\<lambda>z \<in> elts ((a\<Uplus>b)\<Uplus>c). sum_case(sum_case Inl (\<lambda>y. Inr(Inl y))) (\<lambda>y. Inr(Inr y)) z)
      (elts ((a\<Uplus>b)\<Uplus>c)) (elts (a\<Uplus>(b\<Uplus>c)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bij_betw (restrict (sum_case (sum_case ZFC_Cardinals.Inl (\<lambda>y. ZFC_Cardinals.Inr (ZFC_Cardinals.Inl y))) (\<lambda>y. ZFC_Cardinals.Inr (ZFC_Cardinals.Inr y))) (elts (a \<Uplus> b \<Uplus> c))) (elts (a \<Uplus> b \<Uplus> c)) (elts (a \<Uplus> (b \<Uplus> c)))
[PROOF STEP]
by (rule_tac f' = "sum_case (\<lambda>x. Inl (Inl x)) (sum_case (\<lambda>x. Inl (Inr x)) Inr)"
      in bij_betw_byWitness) auto


[STATEMENT]
lemma sum_assoc_eqpoll: "elts ((a\<Uplus>b)\<Uplus>c) \<approx> elts (a\<Uplus>(b\<Uplus>c))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. elts (a \<Uplus> b \<Uplus> c) \<approx> elts (a \<Uplus> (b \<Uplus> c))
[PROOF STEP]
unfolding eqpoll_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>f. bij_betw f (elts (a \<Uplus> b \<Uplus> c)) (elts (a \<Uplus> (b \<Uplus> c)))
[PROOF STEP]
by (metis sum_assoc_bij)


[STATEMENT]
lemma elts_vcard_vsum_eqpoll: "elts (vcard (i \<Uplus> j)) \<approx> Inl ` elts i \<union> Inr ` elts j"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. elts (vcard (i \<Uplus> j)) \<approx> ZFC_Cardinals.Inl ` elts i \<union> ZFC_Cardinals.Inr ` elts j
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. elts (vcard (i \<Uplus> j)) \<approx> ZFC_Cardinals.Inl ` elts i \<union> ZFC_Cardinals.Inr ` elts j
[PROOF STEP]
have "elts (i \<Uplus> j) \<approx> Inl ` elts i \<union> Inr ` elts j"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. elts (i \<Uplus> j) \<approx> ZFC_Cardinals.Inl ` elts i \<union> ZFC_Cardinals.Inr ` elts j
[PROOF STEP]
by (simp add: elts_vsum)
[PROOF STATE]
proof (state)
this:
elts (i \<Uplus> j) \<approx> ZFC_Cardinals.Inl ` elts i \<union> ZFC_Cardinals.Inr ` elts j

goal (1 subgoal):
 1. elts (vcard (i \<Uplus> j)) \<approx> ZFC_Cardinals.Inl ` elts i \<union> ZFC_Cardinals.Inr ` elts j
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
elts (i \<Uplus> j) \<approx> ZFC_Cardinals.Inl ` elts i \<union> ZFC_Cardinals.Inr ` elts j
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
elts (i \<Uplus> j) \<approx> ZFC_Cardinals.Inl ` elts i \<union> ZFC_Cardinals.Inr ` elts j

goal (1 subgoal):
 1. elts (vcard (i \<Uplus> j)) \<approx> ZFC_Cardinals.Inl ` elts i \<union> ZFC_Cardinals.Inr ` elts j
[PROOF STEP]
using cardinal_eqpoll eqpoll_trans
[PROOF STATE]
proof (prove)
using this:
elts (i \<Uplus> j) \<approx> ZFC_Cardinals.Inl ` elts i \<union> ZFC_Cardinals.Inr ` elts j
elts (vcard ?a) \<approx> elts ?a
\<lbrakk>?A \<approx> ?B; ?B \<approx> ?C\<rbrakk> \<Longrightarrow> ?A \<approx> ?C

goal (1 subgoal):
 1. elts (vcard (i \<Uplus> j)) \<approx> ZFC_Cardinals.Inl ` elts i \<union> ZFC_Cardinals.Inr ` elts j
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
elts (vcard (i \<Uplus> j)) \<approx> ZFC_Cardinals.Inl ` elts i \<union> ZFC_Cardinals.Inr ` elts j

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma cadd_assoc: "(i \<oplus> j) \<oplus> k = i \<oplus> (j \<oplus> k)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i \<oplus> j \<oplus> k = i \<oplus> (j \<oplus> k)
[PROOF STEP]
proof (unfold cadd_def, rule cardinal_cong)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. elts (vcard (i \<Uplus> j) \<Uplus> k) \<approx> elts (i \<Uplus> vcard (j \<Uplus> k))
[PROOF STEP]
have "elts (vcard(i \<Uplus> j) \<Uplus> k) \<approx> elts ((i \<Uplus> j) \<Uplus> k)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. elts (vcard (i \<Uplus> j) \<Uplus> k) \<approx> elts (i \<Uplus> j \<Uplus> k)
[PROOF STEP]
by (auto simp: disjnt_def elts_vsum elts_vcard_vsum_eqpoll intro: Un_eqpoll_cong)
[PROOF STATE]
proof (state)
this:
elts (vcard (i \<Uplus> j) \<Uplus> k) \<approx> elts (i \<Uplus> j \<Uplus> k)

goal (1 subgoal):
 1. elts (vcard (i \<Uplus> j) \<Uplus> k) \<approx> elts (i \<Uplus> vcard (j \<Uplus> k))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
elts (vcard (i \<Uplus> j) \<Uplus> k) \<approx> elts (i \<Uplus> j \<Uplus> k)

goal (1 subgoal):
 1. elts (vcard (i \<Uplus> j) \<Uplus> k) \<approx> elts (i \<Uplus> vcard (j \<Uplus> k))
[PROOF STEP]
have "\<dots>  \<approx> elts (i \<Uplus> (j \<Uplus> k))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. elts (i \<Uplus> j \<Uplus> k) \<approx> elts (i \<Uplus> (j \<Uplus> k))
[PROOF STEP]
by (rule sum_assoc_eqpoll)
[PROOF STATE]
proof (state)
this:
elts (i \<Uplus> j \<Uplus> k) \<approx> elts (i \<Uplus> (j \<Uplus> k))

goal (1 subgoal):
 1. elts (vcard (i \<Uplus> j) \<Uplus> k) \<approx> elts (i \<Uplus> vcard (j \<Uplus> k))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
elts (i \<Uplus> j \<Uplus> k) \<approx> elts (i \<Uplus> (j \<Uplus> k))

goal (1 subgoal):
 1. elts (vcard (i \<Uplus> j) \<Uplus> k) \<approx> elts (i \<Uplus> vcard (j \<Uplus> k))
[PROOF STEP]
have "\<dots>  \<approx> elts (i \<Uplus> vcard(j \<Uplus> k))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. elts (i \<Uplus> (j \<Uplus> k)) \<approx> elts (i \<Uplus> vcard (j \<Uplus> k))
[PROOF STEP]
by (auto simp: disjnt_def elts_vsum elts_vcard_vsum_eqpoll [THEN eqpoll_sym] intro: Un_eqpoll_cong)
[PROOF STATE]
proof (state)
this:
elts (i \<Uplus> (j \<Uplus> k)) \<approx> elts (i \<Uplus> vcard (j \<Uplus> k))

goal (1 subgoal):
 1. elts (vcard (i \<Uplus> j) \<Uplus> k) \<approx> elts (i \<Uplus> vcard (j \<Uplus> k))
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
elts (vcard (i \<Uplus> j) \<Uplus> k) \<approx> elts (i \<Uplus> vcard (j \<Uplus> k))
[PROOF STEP]
show "elts (vcard (i \<Uplus> j) \<Uplus> k) \<approx> elts (i \<Uplus> vcard (j \<Uplus> k))"
[PROOF STATE]
proof (prove)
using this:
elts (vcard (i \<Uplus> j) \<Uplus> k) \<approx> elts (i \<Uplus> vcard (j \<Uplus> k))

goal (1 subgoal):
 1. elts (vcard (i \<Uplus> j) \<Uplus> k) \<approx> elts (i \<Uplus> vcard (j \<Uplus> k))
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
elts (vcard (i \<Uplus> j) \<Uplus> k) \<approx> elts (i \<Uplus> vcard (j \<Uplus> k))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma cadd_left_commute: "j \<oplus> (i \<oplus> k) = i \<oplus> (j \<oplus> k)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. j \<oplus> (i \<oplus> k) = i \<oplus> (j \<oplus> k)
[PROOF STEP]
using cadd_assoc cadd_commute
[PROOF STATE]
proof (prove)
using this:
?i \<oplus> ?j \<oplus> ?k = ?i \<oplus> (?j \<oplus> ?k)
?i \<oplus> ?j = ?j \<oplus> ?i

goal (1 subgoal):
 1. j \<oplus> (i \<oplus> k) = i \<oplus> (j \<oplus> k)
[PROOF STEP]
by force


[STATEMENT]
lemma vsum_0_eqpoll: "elts (0\<Uplus>a) \<approx> elts a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. elts (0 \<Uplus> a) \<approx> elts a
[PROOF STEP]
by (simp add: elts_vsum)


[STATEMENT]
lemma cadd_0 [simp]: "Card \<kappa> \<Longrightarrow> 0 \<oplus> \<kappa> = \<kappa>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Card \<kappa> \<Longrightarrow> 0 \<oplus> \<kappa> = \<kappa>
[PROOF STEP]
by (metis Card_def cadd_def cardinal_cong vsum_0_eqpoll)


[STATEMENT]
lemma cadd_0_right [simp]: "Card \<kappa> \<Longrightarrow> \<kappa> \<oplus> 0 = \<kappa>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Card \<kappa> \<Longrightarrow> \<kappa> \<oplus> 0 = \<kappa>
[PROOF STEP]
by (simp add: cadd_commute)


[STATEMENT]
lemma vsum_lepoll_self: "elts a \<lesssim> elts (a\<Uplus>b)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. elts a \<lesssim> elts (a \<Uplus> b)
[PROOF STEP]
unfolding elts_vsum
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. elts a \<lesssim> ZFC_Cardinals.Inl ` elts a \<union> ZFC_Cardinals.Inr ` elts b
[PROOF STEP]
by (meson Inl_iff Un_upper1 inj_onI lepoll_def)


[STATEMENT]
lemma cadd_le_self:
  assumes \<kappa>: "Card \<kappa>" shows "\<kappa> \<le> \<kappa> \<oplus> a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<kappa> \<le> \<kappa> \<oplus> a
[PROOF STEP]
proof (unfold cadd_def)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<kappa> \<le> vcard (\<kappa> \<Uplus> a)
[PROOF STEP]
have "\<kappa> \<le> vcard \<kappa>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<kappa> \<le> vcard \<kappa>
[PROOF STEP]
using Card_def \<kappa>
[PROOF STATE]
proof (prove)
using this:
Card ?i \<equiv> ?i = vcard ?i
Card \<kappa>

goal (1 subgoal):
 1. \<kappa> \<le> vcard \<kappa>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<kappa> \<le> vcard \<kappa>

goal (1 subgoal):
 1. \<kappa> \<le> vcard (\<kappa> \<Uplus> a)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<kappa> \<le> vcard \<kappa>

goal (1 subgoal):
 1. \<kappa> \<le> vcard (\<kappa> \<Uplus> a)
[PROOF STEP]
have "\<dots> \<le> vcard (\<kappa> \<Uplus> a)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vcard \<kappa> \<le> vcard (\<kappa> \<Uplus> a)
[PROOF STEP]
by (simp add: lepoll_imp_Card_le vsum_lepoll_self)
[PROOF STATE]
proof (state)
this:
vcard \<kappa> \<le> vcard (\<kappa> \<Uplus> a)

goal (1 subgoal):
 1. \<kappa> \<le> vcard (\<kappa> \<Uplus> a)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
\<kappa> \<le> vcard (\<kappa> \<Uplus> a)
[PROOF STEP]
show "\<kappa> \<le> vcard (\<kappa> \<Uplus> a)"
[PROOF STATE]
proof (prove)
using this:
\<kappa> \<le> vcard (\<kappa> \<Uplus> a)

goal (1 subgoal):
 1. \<kappa> \<le> vcard (\<kappa> \<Uplus> a)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
\<kappa> \<le> vcard (\<kappa> \<Uplus> a)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma cadd_le_mono: "\<lbrakk>\<kappa>' \<le> \<kappa>; \<mu>' \<le> \<mu>\<rbrakk> \<Longrightarrow> \<kappa>' \<oplus> \<mu>' \<le> \<kappa> \<oplus> \<mu>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<kappa>' \<le> \<kappa>; \<mu>' \<le> \<mu>\<rbrakk> \<Longrightarrow> \<kappa>' \<oplus> \<mu>' \<le> \<kappa> \<oplus> \<mu>
[PROOF STEP]
unfolding cadd_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<kappa>' \<le> \<kappa>; \<mu>' \<le> \<mu>\<rbrakk> \<Longrightarrow> vcard (\<kappa>' \<Uplus> \<mu>') \<le> vcard (\<kappa> \<Uplus> \<mu>)
[PROOF STEP]
by (metis (no_types) lepoll_imp_Card_le less_eq_V_def subset_imp_lepoll sum_subset_iff)


[STATEMENT]
lemma prod_bij: "\<lbrakk>bij_betw f A C; bij_betw g B D\<rbrakk>
             \<Longrightarrow> bij_betw (\<lambda>(x, y). (f x, g y)) (A \<times> B) (C \<times> D)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>bij_betw f A C; bij_betw g B D\<rbrakk> \<Longrightarrow> bij_betw (\<lambda>(x, y). (f x, g y)) (A \<times> B) (C \<times> D)
[PROOF STEP]
apply (rule bij_betw_byWitness [where f' = "\<lambda>(x,y). (inv_into A f x, inv_into B g y)"])
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<lbrakk>bij_betw f A C; bij_betw g B D\<rbrakk> \<Longrightarrow> \<forall>a\<in>A \<times> B. (case case a of (x, y) \<Rightarrow> (f x, g y) of (x, y) \<Rightarrow> (inv_into A f x, inv_into B g y)) = a
 2. \<lbrakk>bij_betw f A C; bij_betw g B D\<rbrakk> \<Longrightarrow> \<forall>a'\<in>C \<times> D. (case case a' of (x, y) \<Rightarrow> (inv_into A f x, inv_into B g y) of (x, y) \<Rightarrow> (f x, g y)) = a'
 3. \<lbrakk>bij_betw f A C; bij_betw g B D\<rbrakk> \<Longrightarrow> (\<lambda>(x, y). (f x, g y)) ` (A \<times> B) \<subseteq> C \<times> D
 4. \<lbrakk>bij_betw f A C; bij_betw g B D\<rbrakk> \<Longrightarrow> (\<lambda>(x, y). (inv_into A f x, inv_into B g y)) ` (C \<times> D) \<subseteq> A \<times> B
[PROOF STEP]
apply (auto simp: bij_betw_inv_into_left bij_betw_inv_into_right bij_betwE)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>aa ba. \<lbrakk>bij_betw f A C; bij_betw g B D; aa \<in> C; ba \<in> D\<rbrakk> \<Longrightarrow> inv_into A f aa \<in> A
 2. \<And>aa ba. \<lbrakk>bij_betw f A C; bij_betw g B D; aa \<in> C; ba \<in> D\<rbrakk> \<Longrightarrow> inv_into B g ba \<in> B
[PROOF STEP]
using bij_betwE bij_betw_inv_into
[PROOF STATE]
proof (prove)
using this:
bij_betw ?f ?A ?B \<Longrightarrow> \<forall>a\<in>?A. ?f a \<in> ?B
bij_betw ?f ?A ?B \<Longrightarrow> bij_betw (inv_into ?A ?f) ?B ?A

goal (2 subgoals):
 1. \<And>aa ba. \<lbrakk>bij_betw f A C; bij_betw g B D; aa \<in> C; ba \<in> D\<rbrakk> \<Longrightarrow> inv_into A f aa \<in> A
 2. \<And>aa ba. \<lbrakk>bij_betw f A C; bij_betw g B D; aa \<in> C; ba \<in> D\<rbrakk> \<Longrightarrow> inv_into B g ba \<in> B
[PROOF STEP]
apply blast+
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma cmult_commute: "i \<otimes> j = j \<otimes> i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i \<otimes> j = j \<otimes> i
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. i \<otimes> j = j \<otimes> i
[PROOF STEP]
have "(\<lambda>(x, y). \<langle>x, y\<rangle>) ` (elts i \<times> elts j) \<approx> (\<lambda>(x, y). \<langle>x, y\<rangle>) ` (elts j \<times> elts i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>(x, y). \<langle>x, y\<rangle>) ` (elts i \<times> elts j) \<approx> (\<lambda>(x, y). \<langle>x, y\<rangle>) ` (elts j \<times> elts i)
[PROOF STEP]
by (simp add: times_commute_eqpoll)
[PROOF STATE]
proof (state)
this:
(\<lambda>(x, y). \<langle>x, y\<rangle>) ` (elts i \<times> elts j) \<approx> (\<lambda>(x, y). \<langle>x, y\<rangle>) ` (elts j \<times> elts i)

goal (1 subgoal):
 1. i \<otimes> j = j \<otimes> i
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(\<lambda>(x, y). \<langle>x, y\<rangle>) ` (elts i \<times> elts j) \<approx> (\<lambda>(x, y). \<langle>x, y\<rangle>) ` (elts j \<times> elts i)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(\<lambda>(x, y). \<langle>x, y\<rangle>) ` (elts i \<times> elts j) \<approx> (\<lambda>(x, y). \<langle>x, y\<rangle>) ` (elts j \<times> elts i)

goal (1 subgoal):
 1. i \<otimes> j = j \<otimes> i
[PROOF STEP]
unfolding cmult_def
[PROOF STATE]
proof (prove)
using this:
(\<lambda>(x, y). \<langle>x, y\<rangle>) ` (elts i \<times> elts j) \<approx> (\<lambda>(x, y). \<langle>x, y\<rangle>) ` (elts j \<times> elts i)

goal (1 subgoal):
 1. vcard (vtimes i j) = vcard (vtimes j i)
[PROOF STEP]
using cardinal_cong elts_VSigma
[PROOF STATE]
proof (prove)
using this:
(\<lambda>(x, y). \<langle>x, y\<rangle>) ` (elts i \<times> elts j) \<approx> (\<lambda>(x, y). \<langle>x, y\<rangle>) ` (elts j \<times> elts i)
elts ?x \<approx> elts ?y \<Longrightarrow> vcard ?x = vcard ?y
elts (VSigma ?A ?B) = (\<lambda>(x, y). \<langle>x, y\<rangle>) ` (SIGMA x:elts ?A. elts (?B x))

goal (1 subgoal):
 1. vcard (vtimes i j) = vcard (vtimes j i)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
i \<otimes> j = j \<otimes> i

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma elts_vcard_VSigma_eqpoll: "elts (vcard (vtimes i j)) \<approx> elts i \<times> elts j"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. elts (vcard (vtimes i j)) \<approx> elts i \<times> elts j
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. elts (vcard (vtimes i j)) \<approx> elts i \<times> elts j
[PROOF STEP]
have "elts (vtimes i j) \<approx> elts i \<times> elts j"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. elts (vtimes i j) \<approx> elts i \<times> elts j
[PROOF STEP]
by (simp add: elts_VSigma)
[PROOF STATE]
proof (state)
this:
elts (vtimes i j) \<approx> elts i \<times> elts j

goal (1 subgoal):
 1. elts (vcard (vtimes i j)) \<approx> elts i \<times> elts j
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
elts (vtimes i j) \<approx> elts i \<times> elts j
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
elts (vtimes i j) \<approx> elts i \<times> elts j

goal (1 subgoal):
 1. elts (vcard (vtimes i j)) \<approx> elts i \<times> elts j
[PROOF STEP]
using cardinal_eqpoll eqpoll_trans
[PROOF STATE]
proof (prove)
using this:
elts (vtimes i j) \<approx> elts i \<times> elts j
elts (vcard ?a) \<approx> elts ?a
\<lbrakk>?A \<approx> ?B; ?B \<approx> ?C\<rbrakk> \<Longrightarrow> ?A \<approx> ?C

goal (1 subgoal):
 1. elts (vcard (vtimes i j)) \<approx> elts i \<times> elts j
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
elts (vcard (vtimes i j)) \<approx> elts i \<times> elts j

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma elts_cmult: "elts (\<kappa>' \<otimes> \<kappa>) \<approx> elts \<kappa>' \<times> elts \<kappa>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. elts (\<kappa>' \<otimes> \<kappa>) \<approx> elts \<kappa>' \<times> elts \<kappa>
[PROOF STEP]
by (simp add: cmult_def elts_vcard_VSigma_eqpoll)


[STATEMENT]
lemma cmult_assoc: "(i \<otimes> j) \<otimes> k = i \<otimes> (j \<otimes> k)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i \<otimes> j \<otimes> k = i \<otimes> (j \<otimes> k)
[PROOF STEP]
unfolding cmult_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vcard (vtimes (vcard (vtimes i j)) k) = vcard (vtimes i (vcard (vtimes j k)))
[PROOF STEP]
proof (rule cardinal_cong)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. elts (vtimes (vcard (vtimes i j)) k) \<approx> elts (vtimes i (vcard (vtimes j k)))
[PROOF STEP]
have "elts (vcard (vtimes i j)) \<times> elts k \<approx> (elts i \<times> elts j) \<times> elts k"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. elts (vcard (vtimes i j)) \<times> elts k \<approx> (elts i \<times> elts j) \<times> elts k
[PROOF STEP]
by (blast intro: times_eqpoll_cong elts_vcard_VSigma_eqpoll cardinal_eqpoll)
[PROOF STATE]
proof (state)
this:
elts (vcard (vtimes i j)) \<times> elts k \<approx> (elts i \<times> elts j) \<times> elts k

goal (1 subgoal):
 1. elts (vtimes (vcard (vtimes i j)) k) \<approx> elts (vtimes i (vcard (vtimes j k)))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
elts (vcard (vtimes i j)) \<times> elts k \<approx> (elts i \<times> elts j) \<times> elts k

goal (1 subgoal):
 1. elts (vtimes (vcard (vtimes i j)) k) \<approx> elts (vtimes i (vcard (vtimes j k)))
[PROOF STEP]
have "\<dots>  \<approx> elts i \<times> (elts j \<times> elts k)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (elts i \<times> elts j) \<times> elts k \<approx> elts i \<times> elts j \<times> elts k
[PROOF STEP]
by (rule times_assoc_eqpoll)
[PROOF STATE]
proof (state)
this:
(elts i \<times> elts j) \<times> elts k \<approx> elts i \<times> elts j \<times> elts k

goal (1 subgoal):
 1. elts (vtimes (vcard (vtimes i j)) k) \<approx> elts (vtimes i (vcard (vtimes j k)))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(elts i \<times> elts j) \<times> elts k \<approx> elts i \<times> elts j \<times> elts k

goal (1 subgoal):
 1. elts (vtimes (vcard (vtimes i j)) k) \<approx> elts (vtimes i (vcard (vtimes j k)))
[PROOF STEP]
have "\<dots>  \<approx> elts i \<times> elts (vcard (vtimes j k))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. elts i \<times> elts j \<times> elts k \<approx> elts i \<times> elts (vcard (vtimes j k))
[PROOF STEP]
by (blast intro: times_eqpoll_cong elts_vcard_VSigma_eqpoll cardinal_eqpoll eqpoll_sym)
[PROOF STATE]
proof (state)
this:
elts i \<times> elts j \<times> elts k \<approx> elts i \<times> elts (vcard (vtimes j k))

goal (1 subgoal):
 1. elts (vtimes (vcard (vtimes i j)) k) \<approx> elts (vtimes i (vcard (vtimes j k)))
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
elts (vcard (vtimes i j)) \<times> elts k \<approx> elts i \<times> elts (vcard (vtimes j k))
[PROOF STEP]
show "elts (VSigma (vcard (vtimes i j)) (\<lambda>z. k)) \<approx> elts (VSigma i (\<lambda>z. vcard (vtimes j k)))"
[PROOF STATE]
proof (prove)
using this:
elts (vcard (vtimes i j)) \<times> elts k \<approx> elts i \<times> elts (vcard (vtimes j k))

goal (1 subgoal):
 1. elts (vtimes (vcard (vtimes i j)) k) \<approx> elts (vtimes i (vcard (vtimes j k)))
[PROOF STEP]
by (simp add: elts_VSigma)
[PROOF STATE]
proof (state)
this:
elts (vtimes (vcard (vtimes i j)) k) \<approx> elts (vtimes i (vcard (vtimes j k)))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma cadd_cmult_distrib: "(i \<oplus> j) \<otimes> k = (i \<otimes> k) \<oplus> (j \<otimes> k)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (i \<oplus> j) \<otimes> k = i \<otimes> k \<oplus> j \<otimes> k
[PROOF STEP]
unfolding cadd_def cmult_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vcard (vtimes (vcard (i \<Uplus> j)) k) = vcard (vcard (vtimes i k) \<Uplus> vcard (vtimes j k))
[PROOF STEP]
proof (rule cardinal_cong)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. elts (vtimes (vcard (i \<Uplus> j)) k) \<approx> elts (vcard (vtimes i k) \<Uplus> vcard (vtimes j k))
[PROOF STEP]
have "elts (vtimes (vcard (i \<Uplus> j)) k) \<approx> elts (vcard (vsum i j)) \<times> elts k"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. elts (vtimes (vcard (i \<Uplus> j)) k) \<approx> elts (vcard (i \<Uplus> j)) \<times> elts k
[PROOF STEP]
using cardinal_eqpoll elts_vcard_VSigma_eqpoll eqpoll_sym eqpoll_trans
[PROOF STATE]
proof (prove)
using this:
elts (vcard ?a) \<approx> elts ?a
elts (vcard (vtimes ?i ?j)) \<approx> elts ?i \<times> elts ?j
?A \<approx> ?B \<Longrightarrow> ?B \<approx> ?A
\<lbrakk>?A \<approx> ?B; ?B \<approx> ?C\<rbrakk> \<Longrightarrow> ?A \<approx> ?C

goal (1 subgoal):
 1. elts (vtimes (vcard (i \<Uplus> j)) k) \<approx> elts (vcard (i \<Uplus> j)) \<times> elts k
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
elts (vtimes (vcard (i \<Uplus> j)) k) \<approx> elts (vcard (i \<Uplus> j)) \<times> elts k

goal (1 subgoal):
 1. elts (vtimes (vcard (i \<Uplus> j)) k) \<approx> elts (vcard (vtimes i k) \<Uplus> vcard (vtimes j k))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
elts (vtimes (vcard (i \<Uplus> j)) k) \<approx> elts (vcard (i \<Uplus> j)) \<times> elts k

goal (1 subgoal):
 1. elts (vtimes (vcard (i \<Uplus> j)) k) \<approx> elts (vcard (vtimes i k) \<Uplus> vcard (vtimes j k))
[PROOF STEP]
have "\<dots> \<approx> (Inl ` elts i \<union> Inr ` elts j) \<times> elts k"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. elts (vcard (i \<Uplus> j)) \<times> elts k \<approx> (ZFC_Cardinals.Inl ` elts i \<union> ZFC_Cardinals.Inr ` elts j) \<times> elts k
[PROOF STEP]
using elts_vcard_vsum_eqpoll times_eqpoll_cong
[PROOF STATE]
proof (prove)
using this:
elts (vcard (?i \<Uplus> ?j)) \<approx> ZFC_Cardinals.Inl ` elts ?i \<union> ZFC_Cardinals.Inr ` elts ?j
\<lbrakk>?A \<approx> ?C; ?B \<approx> ?D\<rbrakk> \<Longrightarrow> ?A \<times> ?B \<approx> ?C \<times> ?D

goal (1 subgoal):
 1. elts (vcard (i \<Uplus> j)) \<times> elts k \<approx> (ZFC_Cardinals.Inl ` elts i \<union> ZFC_Cardinals.Inr ` elts j) \<times> elts k
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
elts (vcard (i \<Uplus> j)) \<times> elts k \<approx> (ZFC_Cardinals.Inl ` elts i \<union> ZFC_Cardinals.Inr ` elts j) \<times> elts k

goal (1 subgoal):
 1. elts (vtimes (vcard (i \<Uplus> j)) k) \<approx> elts (vcard (vtimes i k) \<Uplus> vcard (vtimes j k))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
elts (vcard (i \<Uplus> j)) \<times> elts k \<approx> (ZFC_Cardinals.Inl ` elts i \<union> ZFC_Cardinals.Inr ` elts j) \<times> elts k

goal (1 subgoal):
 1. elts (vtimes (vcard (i \<Uplus> j)) k) \<approx> elts (vcard (vtimes i k) \<Uplus> vcard (vtimes j k))
[PROOF STEP]
have "\<dots> \<approx> (Inl ` elts i) \<times> elts k \<union> (Inr ` elts j) \<times> elts k"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (ZFC_Cardinals.Inl ` elts i \<union> ZFC_Cardinals.Inr ` elts j) \<times> elts k \<approx> ZFC_Cardinals.Inl ` elts i \<times> elts k \<union> ZFC_Cardinals.Inr ` elts j \<times> elts k
[PROOF STEP]
by (simp add: Sigma_Un_distrib1)
[PROOF STATE]
proof (state)
this:
(ZFC_Cardinals.Inl ` elts i \<union> ZFC_Cardinals.Inr ` elts j) \<times> elts k \<approx> ZFC_Cardinals.Inl ` elts i \<times> elts k \<union> ZFC_Cardinals.Inr ` elts j \<times> elts k

goal (1 subgoal):
 1. elts (vtimes (vcard (i \<Uplus> j)) k) \<approx> elts (vcard (vtimes i k) \<Uplus> vcard (vtimes j k))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(ZFC_Cardinals.Inl ` elts i \<union> ZFC_Cardinals.Inr ` elts j) \<times> elts k \<approx> ZFC_Cardinals.Inl ` elts i \<times> elts k \<union> ZFC_Cardinals.Inr ` elts j \<times> elts k

goal (1 subgoal):
 1. elts (vtimes (vcard (i \<Uplus> j)) k) \<approx> elts (vcard (vtimes i k) \<Uplus> vcard (vtimes j k))
[PROOF STEP]
have "\<dots>  \<approx> elts (vtimes i k \<Uplus> vtimes j k)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ZFC_Cardinals.Inl ` elts i \<times> elts k \<union> ZFC_Cardinals.Inr ` elts j \<times> elts k \<approx> elts (vtimes i k \<Uplus> vtimes j k)
[PROOF STEP]
unfolding Plus_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ZFC_Cardinals.Inl ` elts i \<times> elts k \<union> ZFC_Cardinals.Inr ` elts j \<times> elts k \<approx> elts (vtimes i k \<Uplus> vtimes j k)
[PROOF STEP]
by (auto simp: elts_vsum elts_VSigma disjnt_iff intro!: Un_eqpoll_cong times_eqpoll_cong)
[PROOF STATE]
proof (state)
this:
ZFC_Cardinals.Inl ` elts i \<times> elts k \<union> ZFC_Cardinals.Inr ` elts j \<times> elts k \<approx> elts (vtimes i k \<Uplus> vtimes j k)

goal (1 subgoal):
 1. elts (vtimes (vcard (i \<Uplus> j)) k) \<approx> elts (vcard (vtimes i k) \<Uplus> vcard (vtimes j k))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
ZFC_Cardinals.Inl ` elts i \<times> elts k \<union> ZFC_Cardinals.Inr ` elts j \<times> elts k \<approx> elts (vtimes i k \<Uplus> vtimes j k)

goal (1 subgoal):
 1. elts (vtimes (vcard (i \<Uplus> j)) k) \<approx> elts (vcard (vtimes i k) \<Uplus> vcard (vtimes j k))
[PROOF STEP]
have "\<dots>  \<approx> elts (vcard (vtimes i k \<Uplus> vtimes j k))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. elts (vtimes i k \<Uplus> vtimes j k) \<approx> elts (vcard (vtimes i k \<Uplus> vtimes j k))
[PROOF STEP]
by (simp add: cardinal_eqpoll eqpoll_sym)
[PROOF STATE]
proof (state)
this:
elts (vtimes i k \<Uplus> vtimes j k) \<approx> elts (vcard (vtimes i k \<Uplus> vtimes j k))

goal (1 subgoal):
 1. elts (vtimes (vcard (i \<Uplus> j)) k) \<approx> elts (vcard (vtimes i k) \<Uplus> vcard (vtimes j k))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
elts (vtimes i k \<Uplus> vtimes j k) \<approx> elts (vcard (vtimes i k \<Uplus> vtimes j k))

goal (1 subgoal):
 1. elts (vtimes (vcard (i \<Uplus> j)) k) \<approx> elts (vcard (vtimes i k) \<Uplus> vcard (vtimes j k))
[PROOF STEP]
have "\<dots>  \<approx> elts (vcard (vtimes i k) \<Uplus> vcard (vtimes j k))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. elts (vcard (vtimes i k \<Uplus> vtimes j k)) \<approx> elts (vcard (vtimes i k) \<Uplus> vcard (vtimes j k))
[PROOF STEP]
by (metis cadd_assoc cadd_def cardinal_cong cardinal_eqpoll vsum_0_eqpoll vsum_commute_eqpoll)
[PROOF STATE]
proof (state)
this:
elts (vcard (vtimes i k \<Uplus> vtimes j k)) \<approx> elts (vcard (vtimes i k) \<Uplus> vcard (vtimes j k))

goal (1 subgoal):
 1. elts (vtimes (vcard (i \<Uplus> j)) k) \<approx> elts (vcard (vtimes i k) \<Uplus> vcard (vtimes j k))
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
elts (vtimes (vcard (i \<Uplus> j)) k) \<approx> elts (vcard (vtimes i k) \<Uplus> vcard (vtimes j k))
[PROOF STEP]
show "elts (VSigma (vcard (i \<Uplus> j)) (\<lambda>z. k))
             \<approx> elts (vcard (vtimes i k) \<Uplus> vcard (vtimes j k))"
[PROOF STATE]
proof (prove)
using this:
elts (vtimes (vcard (i \<Uplus> j)) k) \<approx> elts (vcard (vtimes i k) \<Uplus> vcard (vtimes j k))

goal (1 subgoal):
 1. elts (vtimes (vcard (i \<Uplus> j)) k) \<approx> elts (vcard (vtimes i k) \<Uplus> vcard (vtimes j k))
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
elts (vtimes (vcard (i \<Uplus> j)) k) \<approx> elts (vcard (vtimes i k) \<Uplus> vcard (vtimes j k))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma cmult_0 [simp]: "0 \<otimes> i = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 \<otimes> i = 0
[PROOF STEP]
using Card_0 Card_def cmult_def
[PROOF STATE]
proof (prove)
using this:
Card 0
Card ?i \<equiv> ?i = vcard ?i
?\<kappa> \<otimes> ?\<mu> \<equiv> vcard (vtimes ?\<kappa> ?\<mu>)

goal (1 subgoal):
 1. 0 \<otimes> i = 0
[PROOF STEP]
by auto


[STATEMENT]
lemma cmult_1 [simp]: assumes "Card \<kappa>" shows "1 \<otimes> \<kappa> = \<kappa>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 1 \<otimes> \<kappa> = \<kappa>
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. 1 \<otimes> \<kappa> = \<kappa>
[PROOF STEP]
have "elts (vtimes (set {0}) \<kappa>) \<approx> elts \<kappa>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. elts (vtimes (set {0}) \<kappa>) \<approx> elts \<kappa>
[PROOF STEP]
by (auto simp: elts_VSigma intro!: times_singleton_eqpoll)
[PROOF STATE]
proof (state)
this:
elts (vtimes (set {0}) \<kappa>) \<approx> elts \<kappa>

goal (1 subgoal):
 1. 1 \<otimes> \<kappa> = \<kappa>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
elts (vtimes (set {0}) \<kappa>) \<approx> elts \<kappa>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
elts (vtimes (set {0}) \<kappa>) \<approx> elts \<kappa>

goal (1 subgoal):
 1. 1 \<otimes> \<kappa> = \<kappa>
[PROOF STEP]
by (metis Card_def assms cardinal_cong cmult_def elts_1 set_of_elts)
[PROOF STATE]
proof (state)
this:
1 \<otimes> \<kappa> = \<kappa>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma cmult_square_le: assumes "Card \<kappa>" shows "\<kappa> \<le> \<kappa> \<otimes> \<kappa>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<kappa> \<le> \<kappa> \<otimes> \<kappa>
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<kappa> \<le> \<kappa> \<otimes> \<kappa>
[PROOF STEP]
have "elts \<kappa> \<lesssim> elts (\<kappa> \<otimes> \<kappa>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. elts \<kappa> \<lesssim> elts (\<kappa> \<otimes> \<kappa>)
[PROOF STEP]
using times_square_lepoll [of "elts \<kappa>"] cmult_def elts_vcard_VSigma_eqpoll eqpoll_sym lepoll_trans2
[PROOF STATE]
proof (prove)
using this:
elts \<kappa> \<lesssim> elts \<kappa> \<times> elts \<kappa>
?\<kappa> \<otimes> ?\<mu> \<equiv> vcard (vtimes ?\<kappa> ?\<mu>)
elts (vcard (vtimes ?i ?j)) \<approx> elts ?i \<times> elts ?j
?A \<approx> ?B \<Longrightarrow> ?B \<approx> ?A
\<lbrakk>?A \<lesssim> ?B; ?B \<approx> ?C\<rbrakk> \<Longrightarrow> ?A \<lesssim> ?C

goal (1 subgoal):
 1. elts \<kappa> \<lesssim> elts (\<kappa> \<otimes> \<kappa>)
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
elts \<kappa> \<lesssim> elts (\<kappa> \<otimes> \<kappa>)

goal (1 subgoal):
 1. \<kappa> \<le> \<kappa> \<otimes> \<kappa>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
elts \<kappa> \<lesssim> elts (\<kappa> \<otimes> \<kappa>)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
elts \<kappa> \<lesssim> elts (\<kappa> \<otimes> \<kappa>)

goal (1 subgoal):
 1. \<kappa> \<le> \<kappa> \<otimes> \<kappa>
[PROOF STEP]
using Card_def assms cmult_def lepoll_cardinal_le
[PROOF STATE]
proof (prove)
using this:
elts \<kappa> \<lesssim> elts (\<kappa> \<otimes> \<kappa>)
Card ?i \<equiv> ?i = vcard ?i
Card \<kappa>
?\<kappa> \<otimes> ?\<mu> \<equiv> vcard (vtimes ?\<kappa> ?\<mu>)
\<lbrakk>elts ?A \<lesssim> elts ?i; Ord ?i\<rbrakk> \<Longrightarrow> vcard ?A \<le> ?i

goal (1 subgoal):
 1. \<kappa> \<le> \<kappa> \<otimes> \<kappa>
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
\<kappa> \<le> \<kappa> \<otimes> \<kappa>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma cmult_le_self: assumes "Card \<kappa>" "\<alpha> \<noteq> 0" shows "\<kappa> \<le> \<kappa> \<otimes> \<alpha>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<kappa> \<le> \<kappa> \<otimes> \<alpha>
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<kappa> \<le> \<kappa> \<otimes> \<alpha>
[PROOF STEP]
have "\<kappa> = vcard \<kappa>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<kappa> = vcard \<kappa>
[PROOF STEP]
using Card_def \<open>Card \<kappa>\<close>
[PROOF STATE]
proof (prove)
using this:
Card ?i \<equiv> ?i = vcard ?i
Card \<kappa>

goal (1 subgoal):
 1. \<kappa> = vcard \<kappa>
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<kappa> = vcard \<kappa>

goal (1 subgoal):
 1. \<kappa> \<le> \<kappa> \<otimes> \<alpha>
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<kappa> = vcard \<kappa>

goal (1 subgoal):
 1. \<kappa> \<le> \<kappa> \<otimes> \<alpha>
[PROOF STEP]
have "\<dots> \<le> vcard (vtimes \<kappa> \<alpha>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vcard \<kappa> \<le> vcard (vtimes \<kappa> \<alpha>)
[PROOF STEP]
apply (rule lepoll_imp_Card_le)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. elts \<kappa> \<lesssim> elts (vtimes \<kappa> \<alpha>)
[PROOF STEP]
apply (simp add: elts_VSigma)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. elts \<kappa> \<lesssim> elts \<kappa> \<times> elts \<alpha>
[PROOF STEP]
by (metis ZFC_in_HOL.ext \<open>\<alpha> \<noteq> 0\<close> elts_0 lepoll_times1)
[PROOF STATE]
proof (state)
this:
vcard \<kappa> \<le> vcard (vtimes \<kappa> \<alpha>)

goal (1 subgoal):
 1. \<kappa> \<le> \<kappa> \<otimes> \<alpha>
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
vcard \<kappa> \<le> vcard (vtimes \<kappa> \<alpha>)

goal (1 subgoal):
 1. \<kappa> \<le> \<kappa> \<otimes> \<alpha>
[PROOF STEP]
have "\<dots> = \<kappa> \<otimes> \<alpha>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vcard (vtimes \<kappa> \<alpha>) = \<kappa> \<otimes> \<alpha>
[PROOF STEP]
by (simp add: cmult_def)
[PROOF STATE]
proof (state)
this:
vcard (vtimes \<kappa> \<alpha>) = \<kappa> \<otimes> \<alpha>

goal (1 subgoal):
 1. \<kappa> \<le> \<kappa> \<otimes> \<alpha>
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
\<kappa> \<le> \<kappa> \<otimes> \<alpha>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<kappa> \<le> \<kappa> \<otimes> \<alpha>

goal (1 subgoal):
 1. \<kappa> \<le> \<kappa> \<otimes> \<alpha>
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
\<kappa> \<le> \<kappa> \<otimes> \<alpha>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma cmult_le_mono: "\<lbrakk>\<kappa>' \<le> \<kappa>; \<mu>' \<le> \<mu>\<rbrakk> \<Longrightarrow> \<kappa>' \<otimes> \<mu>' \<le> \<kappa> \<otimes> \<mu>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<kappa>' \<le> \<kappa>; \<mu>' \<le> \<mu>\<rbrakk> \<Longrightarrow> \<kappa>' \<otimes> \<mu>' \<le> \<kappa> \<otimes> \<mu>
[PROOF STEP]
unfolding cmult_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<kappa>' \<le> \<kappa>; \<mu>' \<le> \<mu>\<rbrakk> \<Longrightarrow> vcard (vtimes \<kappa>' \<mu>') \<le> vcard (vtimes \<kappa> \<mu>)
[PROOF STEP]
by (auto simp: elts_VSigma intro!: lepoll_imp_Card_le times_lepoll_mono subset_imp_lepoll)