equal
deleted
inserted
replaced
1 (* Title: ZF/AC/AC1_WO2.ML |
|
2 ID: $Id$ |
|
3 Author: Krzysztof Grabczewski |
|
4 |
|
5 The proof of AC1 ==> WO2 |
|
6 *) |
|
7 |
|
8 (*Establishing the existence of a bijection -- hence the need for uresult*) |
|
9 val [prem] = goal thy "f \\<in> (\\<Pi>X \\<in> Pow(x) - {0}. X) ==> \ |
|
10 \ ?g(f) \\<in> bij(x, LEAST i. HH(\\<lambda>X \\<in> Pow(x)-{0}. {f`X}, x, i) = {x})"; |
|
11 by (resolve_tac [bij_Least_HH_x RS bij_converse_bij] 1); |
|
12 by (rtac f_subsets_imp_UN_HH_eq_x 1); |
|
13 by (resolve_tac [lam_type RS apply_type] 1 THEN (assume_tac 2)); |
|
14 by (fast_tac (claset() addSDs [prem RS apply_type]) 1); |
|
15 by (fast_tac (claset() addSIs [prem RS Pi_weaken_type]) 1); |
|
16 val lemma1 = uresult() |> standard; |
|
17 |
|
18 Goalw [AC1_def, WO2_def, eqpoll_def] "AC1 ==> WO2"; |
|
19 by (rtac allI 1); |
|
20 by (eres_inst_tac [("x","Pow(A)-{0}")] allE 1); |
|
21 by (fast_tac (claset() addSDs [lemma1] addSIs [Ord_Least]) 1); |
|
22 qed "AC1_WO2"; |
|