42 Goalw [WO1_def] "[| WO1; ALL B:A. EX C:D(B). P(C,B) |] \ |
42 Goalw [WO1_def] "[| WO1; ALL B:A. EX C:D(B). P(C,B) |] \ |
43 \ ==> EX f. ALL B:A. P(f`B,B)"; |
43 \ ==> EX f. ALL B:A. P(f`B,B)"; |
44 by (eres_inst_tac [("x","Union({{C:D(B). P(C,B)}. B:A})")] allE 1); |
44 by (eres_inst_tac [("x","Union({{C:D(B). P(C,B)}. B:A})")] allE 1); |
45 by (etac exE 1); |
45 by (etac exE 1); |
46 by (dtac ex_choice_fun 1); |
46 by (dtac ex_choice_fun 1); |
47 by (fast_tac (claset() addEs [sym RS equals0E]) 1); |
47 by (Fast_tac 1); |
48 by (etac exE 1); |
48 by (etac exE 1); |
49 by (res_inst_tac [("x","lam x:A. f`{C:D(x). P(C,x)}")] exI 1); |
49 by (res_inst_tac [("x","lam x:A. f`{C:D(x). P(C,x)}")] exI 1); |
50 by (Asm_full_simp_tac 1); |
50 by (Asm_full_simp_tac 1); |
51 by (fast_tac (claset() addSDs [RepFunI RSN (2, apply_type)] |
51 by (blast_tac (claset() addSDs [RepFunI RSN (2, apply_type)]) 1); |
52 addSEs [CollectD2]) 1); |
|
53 val lemma1 = result(); |
52 val lemma1 = result(); |
54 |
53 |
55 Goalw [WO1_def] "[| ~Finite(B); WO1 |] ==> |B| + |B| eqpoll B"; |
54 Goalw [WO1_def] "[| ~Finite(B); WO1 |] ==> |B| + |B| eqpoll B"; |
56 by (rtac eqpoll_trans 1); |
55 by (rtac eqpoll_trans 1); |
57 by (fast_tac (claset() addSEs [well_ord_cardinal_eqpoll]) 2); |
56 by (fast_tac (claset() addSEs [well_ord_cardinal_eqpoll]) 2); |