let E be non empty set ; :: thesis: ( E is epsilon-transitive implies ( E |= the_axiom_of_power_sets iff for u being Element of E holds E /\ (bool u) in E ) )
assume A1:
for X being set st X in E holds
X c= E
; :: according to ORDINAL1:def 2 :: thesis: ( E |= the_axiom_of_power_sets iff for u being Element of E holds E /\ (bool u) in E )
thus
( E |= the_axiom_of_power_sets implies for u being Element of E holds E /\ (bool u) in E )
:: thesis: ( ( for u being Element of E holds E /\ (bool u) in E ) implies E |= the_axiom_of_power_sets )proof
assume
E |= the_axiom_of_power_sets
;
:: thesis: for u being Element of E holds E /\ (bool u) in E
then A2:
E |= Ex (x. 1),
(All (x. 2),(((x. 2) 'in' (x. 1)) <=> (All (x. 3),(((x. 3) 'in' (x. 2)) => ((x. 3) 'in' (x. 0 ))))))
by ZF_MODEL:25;
let u be
Element of
E;
:: thesis: E /\ (bool u) in E
consider f0 being
Function of
VAR ,
E;
set f =
f0 +* (x. 0 ),
u;
A3:
(
(f0 +* (x. 0 ),u) . (x. 0 ) = u & ( for
x being
Variable st
x <> x. 0 holds
(f0 +* (x. 0 ),u) . x = f0 . x ) )
by FUNCT_7:34, FUNCT_7:130;
E,
f0 +* (x. 0 ),
u |= Ex (x. 1),
(All (x. 2),(((x. 2) 'in' (x. 1)) <=> (All (x. 3),(((x. 3) 'in' (x. 2)) => ((x. 3) 'in' (x. 0 ))))))
by A2, ZF_MODEL:def 5;
then consider g being
Function of
VAR ,
E such that A4:
( ( for
x being
Variable st
g . x <> (f0 +* (x. 0 ),u) . x holds
x. 1
= x ) &
E,
g |= All (x. 2),
(((x. 2) 'in' (x. 1)) <=> (All (x. 3),(((x. 3) 'in' (x. 2)) => ((x. 3) 'in' (x. 0 ))))) )
by ZF_MODEL:20;
g . (x. 1) = E /\ (bool u)
proof
thus
for
a being
set st
a in g . (x. 1) holds
a in E /\ (bool u)
:: according to TARSKI:def 3,
XBOOLE_0:def 10 :: thesis: E /\ (bool u) c= g . (x. 1)proof
let a be
set ;
:: thesis: ( a in g . (x. 1) implies a in E /\ (bool u) )
assume A5:
a in g . (x. 1)
;
:: thesis: a in E /\ (bool u)
g . (x. 1) c= E
by A1;
then reconsider a' =
a as
Element of
E by A5;
set h =
g +* (x. 2),
a';
A6:
(
(g +* (x. 2),a') . (x. 2) = a' & ( for
x being
Variable st
x <> x. 2 holds
(g +* (x. 2),a') . x = g . x ) )
by FUNCT_7:34, FUNCT_7:130;
for
x being
Variable st
(g +* (x. 2),a') . x <> g . x holds
x. 2
= x
by A6;
then A7:
E,
g +* (x. 2),
a' |= ((x. 2) 'in' (x. 1)) <=> (All (x. 3),(((x. 3) 'in' (x. 2)) => ((x. 3) 'in' (x. 0 ))))
by A4, ZF_MODEL:16;
(g +* (x. 2),a') . (x. 1) = g . (x. 1)
by A6;
then
E,
g +* (x. 2),
a' |= (x. 2) 'in' (x. 1)
by A5, A6, ZF_MODEL:13;
then A8:
E,
g +* (x. 2),
a' |= All (x. 3),
(((x. 3) 'in' (x. 2)) => ((x. 3) 'in' (x. 0 )))
by A7, ZF_MODEL:19;
a' c= u
proof
let b be
set ;
:: according to TARSKI:def 3 :: thesis: ( not b in a' or b in u )
assume A9:
b in a'
;
:: thesis: b in u
a' c= E
by A1;
then reconsider b' =
b as
Element of
E by A9;
set m =
(g +* (x. 2),a') +* (x. 3),
b';
A10:
(
((g +* (x. 2),a') +* (x. 3),b') . (x. 3) = b' & ( for
x being
Variable st
x <> x. 3 holds
((g +* (x. 2),a') +* (x. 3),b') . x = (g +* (x. 2),a') . x ) )
by FUNCT_7:34, FUNCT_7:130;
for
x being
Variable st
((g +* (x. 2),a') +* (x. 3),b') . x <> (g +* (x. 2),a') . x holds
x. 3
= x
by A10;
then A11:
E,
(g +* (x. 2),a') +* (x. 3),
b' |= ((x. 3) 'in' (x. 2)) => ((x. 3) 'in' (x. 0 ))
by A8, ZF_MODEL:16;
((g +* (x. 2),a') +* (x. 3),b') . (x. 2) = (g +* (x. 2),a') . (x. 2)
by A10;
then
E,
(g +* (x. 2),a') +* (x. 3),
b' |= (x. 3) 'in' (x. 2)
by A6, A9, A10, ZF_MODEL:13;
then A12:
E,
(g +* (x. 2),a') +* (x. 3),
b' |= (x. 3) 'in' (x. 0 )
by A11, ZF_MODEL:18;
(
((g +* (x. 2),a') +* (x. 3),b') . (x. 0 ) = (g +* (x. 2),a') . (x. 0 ) &
(g +* (x. 2),a') . (x. 0 ) = g . (x. 0 ) &
g . (x. 0 ) = (f0 +* (x. 0 ),u) . (x. 0 ) )
by A4, A6, A10;
hence
b in u
by A3, A10, A12, ZF_MODEL:13;
:: thesis: verum
end;
hence
a in E /\ (bool u)
by XBOOLE_0:def 4;
:: thesis: verum
end;
let a be
set ;
:: according to TARSKI:def 3 :: thesis: ( not a in E /\ (bool u) or a in g . (x. 1) )
assume A13:
a in E /\ (bool u)
;
:: thesis: a in g . (x. 1)
then A14:
(
a in E &
a in bool u )
by XBOOLE_0:def 4;
reconsider a =
a as
Element of
E by A13, XBOOLE_0:def 4;
set h =
g +* (x. 2),
a;
A15:
(
(g +* (x. 2),a) . (x. 2) = a & ( for
x being
Variable st
x <> x. 2 holds
(g +* (x. 2),a) . x = g . x ) )
by FUNCT_7:34, FUNCT_7:130;
for
x being
Variable st
(g +* (x. 2),a) . x <> g . x holds
x. 2
= x
by A15;
then A16:
E,
g +* (x. 2),
a |= ((x. 2) 'in' (x. 1)) <=> (All (x. 3),(((x. 3) 'in' (x. 2)) => ((x. 3) 'in' (x. 0 ))))
by A4, ZF_MODEL:16;
now let m be
Function of
VAR ,
E;
:: thesis: ( ( for x being Variable st m . x <> (g +* (x. 2),a) . x holds
x. 3 = x ) implies E,m |= ((x. 3) 'in' (x. 2)) => ((x. 3) 'in' (x. 0 )) )assume A17:
for
x being
Variable st
m . x <> (g +* (x. 2),a) . x holds
x. 3
= x
;
:: thesis: E,m |= ((x. 3) 'in' (x. 2)) => ((x. 3) 'in' (x. 0 ))now assume
E,
m |= (x. 3) 'in' (x. 2)
;
:: thesis: E,m |= (x. 3) 'in' (x. 0 )then
(
m . (x. 3) in m . (x. 2) &
m . (x. 2) = (g +* (x. 2),a) . (x. 2) &
a c= u )
by A14, A17, ZF_MODEL:13;
then
(
m . (x. 3) in u &
m . (x. 0 ) = (g +* (x. 2),a) . (x. 0 ) &
(g +* (x. 2),a) . (x. 0 ) = g . (x. 0 ) &
g . (x. 0 ) = (f0 +* (x. 0 ),u) . (x. 0 ) )
by A4, A15, A17;
hence
E,
m |= (x. 3) 'in' (x. 0 )
by A3, ZF_MODEL:13;
:: thesis: verum end; hence
E,
m |= ((x. 3) 'in' (x. 2)) => ((x. 3) 'in' (x. 0 ))
by ZF_MODEL:18;
:: thesis: verum end;
then
E,
g +* (x. 2),
a |= All (x. 3),
(((x. 3) 'in' (x. 2)) => ((x. 3) 'in' (x. 0 )))
by ZF_MODEL:16;
then
E,
g +* (x. 2),
a |= (x. 2) 'in' (x. 1)
by A16, ZF_MODEL:19;
then
(
(g +* (x. 2),a) . (x. 2) in (g +* (x. 2),a) . (x. 1) &
(g +* (x. 2),a) . (x. 1) = g . (x. 1) )
by A15, ZF_MODEL:13;
hence
a in g . (x. 1)
by A15;
:: thesis: verum
end;
hence
E /\ (bool u) in E
;
:: thesis: verum
end;
assume A18:
for u being Element of E holds E /\ (bool u) in E
; :: thesis: E |= the_axiom_of_power_sets
E |= Ex (x. 1),(All (x. 2),(((x. 2) 'in' (x. 1)) <=> (All (x. 3),(((x. 3) 'in' (x. 2)) => ((x. 3) 'in' (x. 0 ))))))
proof
let f be
Function of
VAR ,
E;
:: according to ZF_MODEL:def 5 :: thesis: E,f |= Ex (x. 1),(All (x. 2),(((x. 2) 'in' (x. 1)) <=> (All (x. 3),(((x. 3) 'in' (x. 2)) => ((x. 3) 'in' (x. 0 ))))))
reconsider v =
E /\ (bool (f . (x. 0 ))) as
Element of
E by A18;
set g =
f +* (x. 1),
v;
A19:
(
(f +* (x. 1),v) . (x. 1) = v & ( for
x being
Variable st
x <> x. 1 holds
(f +* (x. 1),v) . x = f . x ) )
by FUNCT_7:34, FUNCT_7:130;
now let h be
Function of
VAR ,
E;
:: thesis: ( ( for x being Variable st h . x <> (f +* (x. 1),v) . x holds
x. 2 = x ) implies E,h |= ((x. 2) 'in' (x. 1)) <=> (All (x. 3),(((x. 3) 'in' (x. 2)) => ((x. 3) 'in' (x. 0 )))) )assume A20:
for
x being
Variable st
h . x <> (f +* (x. 1),v) . x holds
x. 2
= x
;
:: thesis: E,h |= ((x. 2) 'in' (x. 1)) <=> (All (x. 3),(((x. 3) 'in' (x. 2)) => ((x. 3) 'in' (x. 0 ))))now thus
(
E,
h |= (x. 2) 'in' (x. 1) implies
E,
h |= All (x. 3),
(((x. 3) 'in' (x. 2)) => ((x. 3) 'in' (x. 0 ))) )
:: thesis: ( E,h |= All (x. 3),(((x. 3) 'in' (x. 2)) => ((x. 3) 'in' (x. 0 ))) implies E,h |= (x. 2) 'in' (x. 1) )assume A24:
E,
h |= All (x. 3),
(((x. 3) 'in' (x. 2)) => ((x. 3) 'in' (x. 0 )))
;
:: thesis: E,h |= (x. 2) 'in' (x. 1)
h . (x. 2) c= f . (x. 0 )
proof
let a be
set ;
:: according to TARSKI:def 3 :: thesis: ( not a in h . (x. 2) or a in f . (x. 0 ) )
assume A25:
a in h . (x. 2)
;
:: thesis: a in f . (x. 0 )
h . (x. 2) c= E
by A1;
then reconsider a' =
a as
Element of
E by A25;
set m =
h +* (x. 3),
a';
A26:
(
(h +* (x. 3),a') . (x. 3) = a' & ( for
x being
Variable st
x <> x. 3 holds
(h +* (x. 3),a') . x = h . x ) )
by FUNCT_7:34, FUNCT_7:130;
( ( for
x being
Variable st
(h +* (x. 3),a') . x <> h . x holds
x. 3
= x ) &
(h +* (x. 3),a') . (x. 2) = h . (x. 2) )
by A26;
then
(
E,
h +* (x. 3),
a' |= ((x. 3) 'in' (x. 2)) => ((x. 3) 'in' (x. 0 )) &
E,
h +* (x. 3),
a' |= (x. 3) 'in' (x. 2) )
by A24, A25, A26, ZF_MODEL:13, ZF_MODEL:16;
then
E,
h +* (x. 3),
a' |= (x. 3) 'in' (x. 0 )
by ZF_MODEL:18;
then
(
(h +* (x. 3),a') . (x. 3) in (h +* (x. 3),a') . (x. 0 ) &
(h +* (x. 3),a') . (x. 0 ) = h . (x. 0 ) &
h . (x. 0 ) = (f +* (x. 1),v) . (x. 0 ) &
(f +* (x. 1),v) . (x. 0 ) = f . (x. 0 ) )
by A19, A20, A26, ZF_MODEL:13;
hence
a in f . (x. 0 )
by A26;
:: thesis: verum
end; then
(
h . (x. 2) in bool (f . (x. 0 )) &
h . (x. 1) = (f +* (x. 1),v) . (x. 1) )
by A20;
then
h . (x. 2) in h . (x. 1)
by A19, XBOOLE_0:def 4;
hence
E,
h |= (x. 2) 'in' (x. 1)
by ZF_MODEL:13;
:: thesis: verum end; hence
E,
h |= ((x. 2) 'in' (x. 1)) <=> (All (x. 3),(((x. 3) 'in' (x. 2)) => ((x. 3) 'in' (x. 0 ))))
by ZF_MODEL:19;
:: thesis: verum end;
then A27:
E,
f +* (x. 1),
v |= All (x. 2),
(((x. 2) 'in' (x. 1)) <=> (All (x. 3),(((x. 3) 'in' (x. 2)) => ((x. 3) 'in' (x. 0 )))))
by ZF_MODEL:16;
for
x being
Variable st
(f +* (x. 1),v) . x <> f . x holds
x. 1
= x
by A19;
hence
E,
f |= Ex (x. 1),
(All (x. 2),(((x. 2) 'in' (x. 1)) <=> (All (x. 3),(((x. 3) 'in' (x. 2)) => ((x. 3) 'in' (x. 0 ))))))
by A27, ZF_MODEL:20;
:: thesis: verum
end;
hence
E |= the_axiom_of_power_sets
by ZF_MODEL:25; :: thesis: verum