equal
deleted
inserted
replaced
11 definition |
11 definition |
12 Hartog :: "i => i" where |
12 Hartog :: "i => i" where |
13 "Hartog(X) == LEAST i. ~ i \<lesssim> X" |
13 "Hartog(X) == LEAST i. ~ i \<lesssim> X" |
14 |
14 |
15 lemma Ords_in_set: "\<forall>a. Ord(a) --> a \<in> X ==> P" |
15 lemma Ords_in_set: "\<forall>a. Ord(a) --> a \<in> X ==> P" |
16 apply (rule_tac X1 = "{y \<in> X. Ord (y) }" in ON_class [THEN revcut_rl]) |
16 apply (rule_tac X = "{y \<in> X. Ord (y) }" in ON_class [elim_format]) |
17 apply fast |
17 apply fast |
18 done |
18 done |
19 |
19 |
20 lemma Ord_lepoll_imp_ex_well_ord: |
20 lemma Ord_lepoll_imp_ex_well_ord: |
21 "[| Ord(a); a \<lesssim> X |] |
21 "[| Ord(a); a \<lesssim> X |] |