7 |
7 |
8 open WO_AC; |
8 open WO_AC; |
9 |
9 |
10 goal thy "!!A. [| well_ord(Union(A),r); 0~:A; B:A |] \ |
10 goal thy "!!A. [| well_ord(Union(A),r); 0~:A; B:A |] \ |
11 \ ==> (THE b. first(b,B,r)) : B"; |
11 \ ==> (THE b. first(b,B,r)) : B"; |
12 by (fast_tac (AC_cs addSEs [well_ord_imp_ex1_first RS theI RS |
12 by (fast_tac (!claset addSEs [well_ord_imp_ex1_first RS theI RS |
13 (first_def RS def_imp_iff RS iffD1 RS conjunct1)]) 1); |
13 (first_def RS def_imp_iff RS iffD1 RS conjunct1)]) 1); |
14 val first_in_B = result(); |
14 val first_in_B = result(); |
15 |
15 |
16 goal thy "!!A. [| well_ord(Union(A), R); 0~:A |] ==> EX f. f:(PROD X:A. X)"; |
16 goal thy "!!A. [| well_ord(Union(A), R); 0~:A |] ==> EX f. f:(PROD X:A. X)"; |
17 by (fast_tac (AC_cs addSEs [first_in_B] addSIs [lam_type]) 1); |
17 by (fast_tac (!claset addSEs [first_in_B] addSIs [lam_type]) 1); |
18 val ex_choice_fun = result(); |
18 val ex_choice_fun = result(); |
19 |
19 |
20 goal thy "!!A. well_ord(A, R) ==> EX f. f:(PROD X: Pow(A)-{0}. X)"; |
20 goal thy "!!A. well_ord(A, R) ==> EX f. f:(PROD X: Pow(A)-{0}. X)"; |
21 by (fast_tac (AC_cs addSEs [well_ord_subset RS ex_choice_fun]) 1); |
21 by (fast_tac (!claset addSEs [well_ord_subset RS ex_choice_fun]) 1); |
22 val ex_choice_fun_Pow = result(); |
22 val ex_choice_fun_Pow = result(); |