24 THEN (assume_tac 1)); |
24 THEN (assume_tac 1)); |
25 by (resolve_tac [subset_refl RSN (2, restrict_bij RS bij_converse_bij) RS |
25 by (resolve_tac [subset_refl RSN (2, restrict_bij RS bij_converse_bij) RS |
26 (well_ord_Memrel RSN (2, bij_ordertype_vimage)) RS |
26 (well_ord_Memrel RSN (2, bij_ordertype_vimage)) RS |
27 (ordertype_Memrel RSN (2, trans))] 1 |
27 (ordertype_Memrel RSN (2, trans))] 1 |
28 THEN (REPEAT (assume_tac 1))); |
28 THEN (REPEAT (assume_tac 1))); |
29 val Ord_lepoll_imp_ex_well_ord = result(); |
29 qed "Ord_lepoll_imp_ex_well_ord"; |
30 |
30 |
31 goal thy "!!X. [| Ord(a); a lepoll X |] ==> \ |
31 goal thy "!!X. [| Ord(a); a lepoll X |] ==> \ |
32 \ EX Y. Y<=X & (EX R. R<=X*X & ordertype(Y,R)=a)"; |
32 \ EX Y. Y<=X & (EX R. R<=X*X & ordertype(Y,R)=a)"; |
33 by (dtac Ord_lepoll_imp_ex_well_ord 1 THEN (assume_tac 1)); |
33 by (dtac Ord_lepoll_imp_ex_well_ord 1 THEN (assume_tac 1)); |
34 by (step_tac ZF_cs 1); |
34 by (step_tac ZF_cs 1); |
35 by (REPEAT (ares_tac [exI, conjI] 1)); |
35 by (REPEAT (ares_tac [exI, conjI] 1)); |
36 by (etac ordertype_Int 2); |
36 by (etac ordertype_Int 2); |
37 by (fast_tac ZF_cs 1); |
37 by (fast_tac ZF_cs 1); |
38 val Ord_lepoll_imp_eq_ordertype = result(); |
38 qed "Ord_lepoll_imp_eq_ordertype"; |
39 |
39 |
40 goal thy "!!X. ALL a. Ord(a) --> a lepoll X ==> \ |
40 goal thy "!!X. ALL a. Ord(a) --> a lepoll X ==> \ |
41 \ ALL a. Ord(a) --> \ |
41 \ ALL a. Ord(a) --> \ |
42 \ a:{a. Z:Pow(X)*Pow(X*X), EX Y R. Z=<Y,R> & ordertype(Y,R)=a}"; |
42 \ a:{a. Z:Pow(X)*Pow(X*X), EX Y R. Z=<Y,R> & ordertype(Y,R)=a}"; |
43 by (REPEAT (resolve_tac [allI,impI] 1)); |
43 by (REPEAT (resolve_tac [allI,impI] 1)); |
44 by (REPEAT (eresolve_tac [allE, impE] 1)); |
44 by (REPEAT (eresolve_tac [allE, impE] 1)); |
45 by (assume_tac 1); |
45 by (assume_tac 1); |
46 by (dtac Ord_lepoll_imp_eq_ordertype 1 THEN (assume_tac 1)); |
46 by (dtac Ord_lepoll_imp_eq_ordertype 1 THEN (assume_tac 1)); |
47 by (fast_tac (ZF_cs addSIs [ReplaceI] addEs [sym]) 1); |
47 by (fast_tac (ZF_cs addSIs [ReplaceI] addEs [sym]) 1); |
48 val Ords_lepoll_set_lemma = result(); |
48 qed "Ords_lepoll_set_lemma"; |
49 |
49 |
50 goal thy "!!X. ALL a. Ord(a) --> a lepoll X ==> P"; |
50 goal thy "!!X. ALL a. Ord(a) --> a lepoll X ==> P"; |
51 by (eresolve_tac [Ords_lepoll_set_lemma RS Ords_in_set] 1); |
51 by (eresolve_tac [Ords_lepoll_set_lemma RS Ords_in_set] 1); |
52 val Ords_lepoll_set = result(); |
52 qed "Ords_lepoll_set"; |
53 |
53 |
54 goal thy "EX a. Ord(a) & ~a lepoll X"; |
54 goal thy "EX a. Ord(a) & ~a lepoll X"; |
55 by (rtac swap 1); |
55 by (rtac swap 1); |
56 by (fast_tac ZF_cs 1); |
56 by (fast_tac ZF_cs 1); |
57 by (rtac Ords_lepoll_set 1); |
57 by (rtac Ords_lepoll_set 1); |
58 by (fast_tac ZF_cs 1); |
58 by (fast_tac ZF_cs 1); |
59 val ex_Ord_not_lepoll = result(); |
59 qed "ex_Ord_not_lepoll"; |
60 |
60 |
61 goalw thy [Hartog_def] "~ Hartog(A) lepoll A"; |
61 goalw thy [Hartog_def] "~ Hartog(A) lepoll A"; |
62 by (resolve_tac [ex_Ord_not_lepoll RS exE] 1); |
62 by (resolve_tac [ex_Ord_not_lepoll RS exE] 1); |
63 by (rtac LeastI 1); |
63 by (rtac LeastI 1); |
64 by (REPEAT (fast_tac ZF_cs 1)); |
64 by (REPEAT (fast_tac ZF_cs 1)); |
65 val HartogI = result(); |
65 qed "HartogI"; |
66 |
66 |
67 val HartogE = HartogI RS notE; |
67 val HartogE = HartogI RS notE; |
68 |
68 |
69 goalw thy [Hartog_def] "Ord(Hartog(A))"; |
69 goalw thy [Hartog_def] "Ord(Hartog(A))"; |
70 by (rtac Ord_Least 1); |
70 by (rtac Ord_Least 1); |
71 val Ord_Hartog = result(); |
71 qed "Ord_Hartog"; |
72 |
72 |
73 goalw thy [Hartog_def] "!!i. [| i < Hartog(A); ~ i lepoll A |] ==> P"; |
73 goalw thy [Hartog_def] "!!i. [| i < Hartog(A); ~ i lepoll A |] ==> P"; |
74 by (fast_tac (ZF_cs addEs [less_LeastE]) 1); |
74 by (fast_tac (ZF_cs addEs [less_LeastE]) 1); |
75 val less_HartogE1 = result(); |
75 qed "less_HartogE1"; |
76 |
76 |
77 goal thy "!!i. [| i < Hartog(A); i eqpoll Hartog(A) |] ==> P"; |
77 goal thy "!!i. [| i < Hartog(A); i eqpoll Hartog(A) |] ==> P"; |
78 by (fast_tac (ZF_cs addEs [less_HartogE1, eqpoll_sym RS eqpoll_imp_lepoll |
78 by (fast_tac (ZF_cs addEs [less_HartogE1, eqpoll_sym RS eqpoll_imp_lepoll |
79 RS lepoll_trans RS HartogE]) 1); |
79 RS lepoll_trans RS HartogE]) 1); |
80 val less_HartogE = result(); |
80 qed "less_HartogE"; |
81 |
81 |
82 goal thy "Card(Hartog(A))"; |
82 goal thy "Card(Hartog(A))"; |
83 by (fast_tac (ZF_cs addSIs [CardI, Ord_Hartog] addEs [less_HartogE]) 1); |
83 by (fast_tac (ZF_cs addSIs [CardI, Ord_Hartog] addEs [less_HartogE]) 1); |
84 val Card_Hartog = result(); |
84 qed "Card_Hartog"; |