26 lam <x,y>:K*K. <x \<union> y, x, y>, |
26 lam <x,y>:K*K. <x \<union> y, x, y>, |
27 rmult(K,Memrel(K), K*K, rmult(K,Memrel(K), K,Memrel(K))))" |
27 rmult(K,Memrel(K), K*K, rmult(K,Memrel(K), K,Memrel(K))))" |
28 |
28 |
29 definition |
29 definition |
30 jump_cardinal :: "i=>i" where |
30 jump_cardinal :: "i=>i" where |
31 \<comment>\<open>This definition is more complex than Kunen's but it more easily proved to |
31 \<comment> \<open>This definition is more complex than Kunen's but it more easily proved to |
32 be a cardinal\<close> |
32 be a cardinal\<close> |
33 "jump_cardinal(K) == |
33 "jump_cardinal(K) == |
34 \<Union>X\<in>Pow(K). {z. r \<in> Pow(K*K), well_ord(X,r) & z = ordertype(X,r)}" |
34 \<Union>X\<in>Pow(K). {z. r \<in> Pow(K*K), well_ord(X,r) & z = ordertype(X,r)}" |
35 |
35 |
36 definition |
36 definition |
37 csucc :: "i=>i" where |
37 csucc :: "i=>i" where |
38 \<comment>\<open>needed because @{term "jump_cardinal(K)"} might not be the successor |
38 \<comment> \<open>needed because @{term "jump_cardinal(K)"} might not be the successor |
39 of @{term K}\<close> |
39 of @{term K}\<close> |
40 "csucc(K) == \<mu> L. Card(L) & K<L" |
40 "csucc(K) == \<mu> L. Card(L) & K<L" |
41 |
41 |
42 |
42 |
43 lemma Card_Union [simp,intro,TC]: |
43 lemma Card_Union [simp,intro,TC]: |