1123
|
1 |
(* Title: ZF/AC/WO_AC.ML
|
|
2 |
ID: $Id$
|
|
3 |
Author: Krzysztof Gr`abczewski
|
|
4 |
|
|
5 |
Lemmas used in the proofs like WO? ==> AC?
|
|
6 |
*)
|
|
7 |
|
|
8 |
open WO_AC;
|
|
9 |
|
|
10 |
goal thy "!!A. [| well_ord(Union(A),r); 0~:A; B:A |] \
|
|
11 |
\ ==> (THE b. first(b,B,r)) : B";
|
|
12 |
by (fast_tac (AC_cs addSEs [well_ord_imp_ex1_first RS theI RS
|
|
13 |
(first_def RS def_imp_iff RS iffD1 RS conjunct1)]) 1);
|
|
14 |
val first_in_B = result();
|
|
15 |
|
|
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);
|
|
18 |
val ex_choice_fun = result();
|
|
19 |
|
|
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);
|
1196
|
22 |
val ex_choice_fun_Pow = result();
|