1461

1 
(* Title: ZF/AC/AC1_WO2.ML

1123

2 
ID: $Id$

1461

3 
Author: Krzysztof Grabczewski

1123

4 


5 
The proof of AC1 ==> WO2


6 
*)


7 


8 
open AC1_WO2;


9 


10 
val [prem] = goal thy "f : (PROD X:Pow(x)  {0}. X) ==> \

1461

11 
\ ?g(f) : bij(x, LEAST i. HH(lam X:Pow(x){0}. {f`X}, x, i) = {x})";

1123

12 
by (resolve_tac [bij_Least_HH_x RS bij_converse_bij] 1);

1206

13 
by (rtac f_subsets_imp_UN_HH_eq_x 1);

1123

14 
by (resolve_tac [lam_type RS apply_type] 1 THEN (assume_tac 2));


15 
by (fast_tac (AC_cs addSDs [equals0D, prem RS apply_type]) 1);


16 
by (fast_tac (AC_cs addSIs [prem RS Pi_weaken_type]) 1);


17 
val lemma1 = uresult();


18 


19 
goalw thy [AC1_def, WO2_def, eqpoll_def] "!!Z. AC1 ==> WO2";

1206

20 
by (rtac allI 1);

1123

21 
by (eres_inst_tac [("x","Pow(A){0}")] allE 1);


22 
by (fast_tac (AC_cs addSDs [lemma1] addSIs [Ord_Least]) 1);

1196

23 
qed "AC1_WO2";
