1123
|
1 |
(* Title: ZF/AC/WO1_WO8.ML
|
|
2 |
ID: $Id$
|
|
3 |
Author: Krzysztof Gr`abczewski
|
|
4 |
|
|
5 |
The proof of WO8 <-> WO1 (Rubin & Rubin p. 6)
|
|
6 |
*)
|
|
7 |
|
|
8 |
(* ********************************************************************** *)
|
|
9 |
(* Trivial implication "WO1 ==> WO8" *)
|
|
10 |
(* ********************************************************************** *)
|
|
11 |
|
|
12 |
goalw thy WO_defs "!!Z. WO1 ==> WO8";
|
|
13 |
by (fast_tac ZF_cs 1);
|
|
14 |
result();
|
|
15 |
|
|
16 |
(* ********************************************************************** *)
|
|
17 |
(* The proof of "WO8 ==> WO1" - faithful image of Rubin & Rubin's proof *)
|
|
18 |
(* ********************************************************************** *)
|
|
19 |
|
|
20 |
goalw thy WO_defs "!!Z. WO8 ==> WO1";
|
|
21 |
by (resolve_tac [allI] 1);
|
|
22 |
by (eres_inst_tac [("x","{{x}. x:A}")] allE 1);
|
|
23 |
by (eresolve_tac [impE] 1);
|
|
24 |
by (fast_tac (AC_cs addSEs [lam_sing_bij RS bij_is_inj RS
|
|
25 |
well_ord_rvimage]) 2);
|
|
26 |
by (res_inst_tac [("x","lam a:{{x}. x:A}. THE x. a={x}")] exI 1);
|
|
27 |
by (fast_tac (ZF_cs addSEs [RepFunE, singleton_eq_iff RS iffD1 RS sym]
|
|
28 |
addSIs [lam_type, singletonI]
|
|
29 |
addIs [the_equality RS ssubst]) 1);
|
|
30 |
result(); |