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 )

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)))))))))

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 A23:
for u being Element of E holds E /\ (bool u) in E
; :: thesis: E |= the_axiom_of_power_sets
set f0 = the Function of VAR,E;

assume A2: E |= the_axiom_of_power_sets ; :: thesis: for u being Element of E holds E /\ (bool u) in E

let u be Element of E; :: thesis: E /\ (bool u) in E

set f = the Function of VAR,E +* ((x. 0),u);

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 A2, ZF_MODEL:23;

then E, the Function of VAR,E +* ((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))))))))) ;

then consider g being Function of VAR,E such that

A3: for x being Variable st g . x <> ( the Function of VAR,E +* ((x. 0),u)) . x holds

x. 1 = x and

A4: 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;

A5: ( the Function of VAR,E +* ((x. 0),u)) . (x. 0) = u by FUNCT_7:128;

g . (x. 1) = E /\ (bool u)

end;assume A2: E |= the_axiom_of_power_sets ; :: thesis: for u being Element of E holds E /\ (bool u) in E

let u be Element of E; :: thesis: E /\ (bool u) in E

set f = the Function of VAR,E +* ((x. 0),u);

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 A2, ZF_MODEL:23;

then E, the Function of VAR,E +* ((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))))))))) ;

then consider g being Function of VAR,E such that

A3: for x being Variable st g . x <> ( the Function of VAR,E +* ((x. 0),u)) . x holds

x. 1 = x and

A4: 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;

A5: ( the Function of VAR,E +* ((x. 0),u)) . (x. 0) = u by FUNCT_7:128;

g . (x. 1) = E /\ (bool u)

proof

hence
E /\ (bool u) in E
; :: thesis: verum
thus
for a being object 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)

assume A15: a in E /\ (bool u) ; :: thesis: a in g . (x. 1)

then A16: a in bool u by XBOOLE_0:def 4;

reconsider a = a as Element of E by A15, XBOOLE_0:def 4;

set h = g +* ((x. 2),a);

A17: (g +* ((x. 2),a)) . (x. 2) = a by FUNCT_7:128;

A22: (g +* ((x. 2),a)) . (x. 1) = g . (x. 1) by FUNCT_7:32;

for x being Variable st (g +* ((x. 2),a)) . x <> g . x holds

x. 2 = x by FUNCT_7:32;

then 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;

then E,g +* ((x. 2),a) |= (x. 2) 'in' (x. 1) by A21, ZF_MODEL:19;

hence a in g . (x. 1) by A17, A22, ZF_MODEL:13; :: thesis: verum

end;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 object ; :: according to TARSKI:def 3 :: thesis: ( not a in E /\ (bool u) or a in g . (x. 1) )
let a be object ; :: thesis: ( a in g . (x. 1) implies a in E /\ (bool u) )

assume A6: a in g . (x. 1) ; :: thesis: a in E /\ (bool u)

g . (x. 1) c= E by A1;

then reconsider a9 = a as Element of E by A6;

set h = g +* ((x. 2),a9);

A7: (g +* ((x. 2),a9)) . (x. 2) = a9 by FUNCT_7:128;

for x being Variable st (g +* ((x. 2),a9)) . x <> g . x holds

x. 2 = x by FUNCT_7:32;

then A8: E,g +* ((x. 2),a9) |= ((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),a9)) . (x. 1) = g . (x. 1) by FUNCT_7:32;

then E,g +* ((x. 2),a9) |= (x. 2) 'in' (x. 1) by A6, A7, ZF_MODEL:13;

then A9: E,g +* ((x. 2),a9) |= All ((x. 3),(((x. 3) 'in' (x. 2)) => ((x. 3) 'in' (x. 0)))) by A8, ZF_MODEL:19;

a9 c= u

end;assume A6: a in g . (x. 1) ; :: thesis: a in E /\ (bool u)

g . (x. 1) c= E by A1;

then reconsider a9 = a as Element of E by A6;

set h = g +* ((x. 2),a9);

A7: (g +* ((x. 2),a9)) . (x. 2) = a9 by FUNCT_7:128;

for x being Variable st (g +* ((x. 2),a9)) . x <> g . x holds

x. 2 = x by FUNCT_7:32;

then A8: E,g +* ((x. 2),a9) |= ((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),a9)) . (x. 1) = g . (x. 1) by FUNCT_7:32;

then E,g +* ((x. 2),a9) |= (x. 2) 'in' (x. 1) by A6, A7, ZF_MODEL:13;

then A9: E,g +* ((x. 2),a9) |= All ((x. 3),(((x. 3) 'in' (x. 2)) => ((x. 3) 'in' (x. 0)))) by A8, ZF_MODEL:19;

a9 c= u

proof

hence
a in E /\ (bool u)
by XBOOLE_0:def 4; :: thesis: verum
let b be object ; :: according to TARSKI:def 3 :: thesis: ( not b in a9 or b in u )

assume A10: b in a9 ; :: thesis: b in u

a9 c= E by A1;

then reconsider b9 = b as Element of E by A10;

set m = (g +* ((x. 2),a9)) +* ((x. 3),b9);

A11: ((g +* ((x. 2),a9)) +* ((x. 3),b9)) . (x. 3) = b9 by FUNCT_7:128;

for x being Variable st ((g +* ((x. 2),a9)) +* ((x. 3),b9)) . x <> (g +* ((x. 2),a9)) . x holds

x. 3 = x by FUNCT_7:32;

then A12: E,(g +* ((x. 2),a9)) +* ((x. 3),b9) |= ((x. 3) 'in' (x. 2)) => ((x. 3) 'in' (x. 0)) by A9, ZF_MODEL:16;

((g +* ((x. 2),a9)) +* ((x. 3),b9)) . (x. 2) = (g +* ((x. 2),a9)) . (x. 2) by FUNCT_7:32;

then E,(g +* ((x. 2),a9)) +* ((x. 3),b9) |= (x. 3) 'in' (x. 2) by A7, A10, A11, ZF_MODEL:13;

then A13: E,(g +* ((x. 2),a9)) +* ((x. 3),b9) |= (x. 3) 'in' (x. 0) by A12, ZF_MODEL:18;

A14: ( ((g +* ((x. 2),a9)) +* ((x. 3),b9)) . (x. 0) = (g +* ((x. 2),a9)) . (x. 0) & (g +* ((x. 2),a9)) . (x. 0) = g . (x. 0) ) by FUNCT_7:32;

g . (x. 0) = ( the Function of VAR,E +* ((x. 0),u)) . (x. 0) by A3;

hence b in u by A5, A11, A13, A14, ZF_MODEL:13; :: thesis: verum

end;assume A10: b in a9 ; :: thesis: b in u

a9 c= E by A1;

then reconsider b9 = b as Element of E by A10;

set m = (g +* ((x. 2),a9)) +* ((x. 3),b9);

A11: ((g +* ((x. 2),a9)) +* ((x. 3),b9)) . (x. 3) = b9 by FUNCT_7:128;

for x being Variable st ((g +* ((x. 2),a9)) +* ((x. 3),b9)) . x <> (g +* ((x. 2),a9)) . x holds

x. 3 = x by FUNCT_7:32;

then A12: E,(g +* ((x. 2),a9)) +* ((x. 3),b9) |= ((x. 3) 'in' (x. 2)) => ((x. 3) 'in' (x. 0)) by A9, ZF_MODEL:16;

((g +* ((x. 2),a9)) +* ((x. 3),b9)) . (x. 2) = (g +* ((x. 2),a9)) . (x. 2) by FUNCT_7:32;

then E,(g +* ((x. 2),a9)) +* ((x. 3),b9) |= (x. 3) 'in' (x. 2) by A7, A10, A11, ZF_MODEL:13;

then A13: E,(g +* ((x. 2),a9)) +* ((x. 3),b9) |= (x. 3) 'in' (x. 0) by A12, ZF_MODEL:18;

A14: ( ((g +* ((x. 2),a9)) +* ((x. 3),b9)) . (x. 0) = (g +* ((x. 2),a9)) . (x. 0) & (g +* ((x. 2),a9)) . (x. 0) = g . (x. 0) ) by FUNCT_7:32;

g . (x. 0) = ( the Function of VAR,E +* ((x. 0),u)) . (x. 0) by A3;

hence b in u by A5, A11, A13, A14, ZF_MODEL:13; :: thesis: verum

assume A15: a in E /\ (bool u) ; :: thesis: a in g . (x. 1)

then A16: a in bool u by XBOOLE_0:def 4;

reconsider a = a as Element of E by A15, XBOOLE_0:def 4;

set h = g +* ((x. 2),a);

A17: (g +* ((x. 2),a)) . (x. 2) = a by FUNCT_7:128;

now :: thesis: for m being Function of VAR,E st ( for x being Variable st m . x <> (g +* ((x. 2),a)) . x holds

x. 3 = x ) holds

E,m |= ((x. 3) 'in' (x. 2)) => ((x. 3) 'in' (x. 0))

then A21:
E,g +* ((x. 2),a) |= All ((x. 3),(((x. 3) 'in' (x. 2)) => ((x. 3) 'in' (x. 0))))
by ZF_MODEL:16;x. 3 = x ) holds

E,m |= ((x. 3) 'in' (x. 2)) => ((x. 3) 'in' (x. 0))

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 A18: 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))

end;x. 3 = x ) implies E,m |= ((x. 3) 'in' (x. 2)) => ((x. 3) 'in' (x. 0)) )

assume A18: 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 :: thesis: ( E,m |= (x. 3) 'in' (x. 2) implies E,m |= (x. 3) 'in' (x. 0) )

hence
E,m |= ((x. 3) 'in' (x. 2)) => ((x. 3) 'in' (x. 0))
by ZF_MODEL:18; :: thesis: verumassume
E,m |= (x. 3) 'in' (x. 2)
; :: thesis: E,m |= (x. 3) 'in' (x. 0)

then A19: m . (x. 3) in m . (x. 2) by ZF_MODEL:13;

A20: ( (g +* ((x. 2),a)) . (x. 0) = g . (x. 0) & g . (x. 0) = ( the Function of VAR,E +* ((x. 0),u)) . (x. 0) ) by A3, FUNCT_7:32;

( m . (x. 2) = (g +* ((x. 2),a)) . (x. 2) & m . (x. 0) = (g +* ((x. 2),a)) . (x. 0) ) by A18;

hence E,m |= (x. 3) 'in' (x. 0) by A5, A16, A17, A19, A20, ZF_MODEL:13; :: thesis: verum

end;then A19: m . (x. 3) in m . (x. 2) by ZF_MODEL:13;

A20: ( (g +* ((x. 2),a)) . (x. 0) = g . (x. 0) & g . (x. 0) = ( the Function of VAR,E +* ((x. 0),u)) . (x. 0) ) by A3, FUNCT_7:32;

( m . (x. 2) = (g +* ((x. 2),a)) . (x. 2) & m . (x. 0) = (g +* ((x. 2),a)) . (x. 0) ) by A18;

hence E,m |= (x. 3) 'in' (x. 0) by A5, A16, A17, A19, A20, ZF_MODEL:13; :: thesis: verum

A22: (g +* ((x. 2),a)) . (x. 1) = g . (x. 1) by FUNCT_7:32;

for x being Variable st (g +* ((x. 2),a)) . x <> g . x holds

x. 2 = x by FUNCT_7:32;

then 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;

then E,g +* ((x. 2),a) |= (x. 2) 'in' (x. 1) by A21, ZF_MODEL:19;

hence a in g . (x. 1) by A17, A22, ZF_MODEL:13; :: thesis: verum

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

hence
E |= the_axiom_of_power_sets
by ZF_MODEL:23; :: thesis: verum
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 A23;

set g = f +* ((x. 1),v);

A24: (f +* ((x. 1),v)) . (x. 1) = v by FUNCT_7:128;

for x being Variable st (f +* ((x. 1),v)) . x <> f . x holds

x. 1 = x by FUNCT_7:32;

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 A37, ZF_MODEL:20; :: thesis: verum

end;reconsider v = E /\ (bool (f . (x. 0))) as Element of E by A23;

set g = f +* ((x. 1),v);

A24: (f +* ((x. 1),v)) . (x. 1) = v by FUNCT_7:128;

now :: thesis: for h being Function of VAR,E st ( for x being Variable st h . x <> (f +* ((x. 1),v)) . x holds

x. 2 = x ) holds

E,h |= ((x. 2) 'in' (x. 1)) <=> (All ((x. 3),(((x. 3) 'in' (x. 2)) => ((x. 3) 'in' (x. 0)))))

then A37:
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;x. 2 = x ) holds

E,h |= ((x. 2) 'in' (x. 1)) <=> (All ((x. 3),(((x. 3) 'in' (x. 2)) => ((x. 3) 'in' (x. 0)))))

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 A25: 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)))))

end;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 A25: 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 :: thesis: ( ( E,h |= (x. 2) 'in' (x. 1) implies E,h |= All ((x. 3),(((x. 3) 'in' (x. 2)) => ((x. 3) 'in' (x. 0)))) ) & ( E,h |= All ((x. 3),(((x. 3) 'in' (x. 2)) => ((x. 3) 'in' (x. 0)))) implies E,h |= (x. 2) 'in' (x. 1) ) )

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: verumthus
( 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) )

A32: h . (x. 2) c= f . (x. 0)

then h . (x. 2) in h . (x. 1) by A24, A32, XBOOLE_0:def 4;

hence E,h |= (x. 2) 'in' (x. 1) by ZF_MODEL:13; :: thesis: verum

end;proof

assume A31:
E,h |= All ((x. 3),(((x. 3) 'in' (x. 2)) => ((x. 3) 'in' (x. 0))))
; :: thesis: E,h |= (x. 2) 'in' (x. 1)
assume
E,h |= (x. 2) 'in' (x. 1)
; :: thesis: E,h |= All ((x. 3),(((x. 3) 'in' (x. 2)) => ((x. 3) 'in' (x. 0))))

then A26: h . (x. 2) in h . (x. 1) by ZF_MODEL:13;

h . (x. 1) = v by A24, A25;

then A27: h . (x. 2) in bool (f . (x. 0)) by A26, XBOOLE_0:def 4;

end;then A26: h . (x. 2) in h . (x. 1) by ZF_MODEL:13;

h . (x. 1) = v by A24, A25;

then A27: h . (x. 2) in bool (f . (x. 0)) by A26, XBOOLE_0:def 4;

now :: thesis: for m being Function of VAR,E st ( for x being Variable st m . x <> h . x holds

x. 3 = x ) holds

E,m |= ((x. 3) 'in' (x. 2)) => ((x. 3) 'in' (x. 0))

hence
E,h |= All ((x. 3),(((x. 3) 'in' (x. 2)) => ((x. 3) 'in' (x. 0))))
by ZF_MODEL:16; :: thesis: verumx. 3 = x ) holds

E,m |= ((x. 3) 'in' (x. 2)) => ((x. 3) 'in' (x. 0))

let m be Function of VAR,E; :: thesis: ( ( for x being Variable st m . x <> h . x holds

x. 3 = x ) implies E,m |= ((x. 3) 'in' (x. 2)) => ((x. 3) 'in' (x. 0)) )

assume A28: for x being Variable st m . x <> h . x holds

x. 3 = x ; :: thesis: E,m |= ((x. 3) 'in' (x. 2)) => ((x. 3) 'in' (x. 0))

end;x. 3 = x ) implies E,m |= ((x. 3) 'in' (x. 2)) => ((x. 3) 'in' (x. 0)) )

assume A28: for x being Variable st m . x <> h . x holds

x. 3 = x ; :: thesis: E,m |= ((x. 3) 'in' (x. 2)) => ((x. 3) 'in' (x. 0))

now :: thesis: ( E,m |= (x. 3) 'in' (x. 2) implies E,m |= (x. 3) 'in' (x. 0) )

hence
E,m |= ((x. 3) 'in' (x. 2)) => ((x. 3) 'in' (x. 0))
by ZF_MODEL:18; :: thesis: verumassume
E,m |= (x. 3) 'in' (x. 2)
; :: thesis: E,m |= (x. 3) 'in' (x. 0)

then A29: m . (x. 3) in m . (x. 2) by ZF_MODEL:13;

A30: ( m . (x. 2) = h . (x. 2) & f . (x. 0) = (f +* ((x. 1),v)) . (x. 0) ) by A28, FUNCT_7:32;

( (f +* ((x. 1),v)) . (x. 0) = h . (x. 0) & h . (x. 0) = m . (x. 0) ) by A25, A28;

hence E,m |= (x. 3) 'in' (x. 0) by A27, A29, A30, ZF_MODEL:13; :: thesis: verum

end;then A29: m . (x. 3) in m . (x. 2) by ZF_MODEL:13;

A30: ( m . (x. 2) = h . (x. 2) & f . (x. 0) = (f +* ((x. 1),v)) . (x. 0) ) by A28, FUNCT_7:32;

( (f +* ((x. 1),v)) . (x. 0) = h . (x. 0) & h . (x. 0) = m . (x. 0) ) by A25, A28;

hence E,m |= (x. 3) 'in' (x. 0) by A27, A29, A30, ZF_MODEL:13; :: thesis: verum

A32: h . (x. 2) c= f . (x. 0)

proof

h . (x. 1) = (f +* ((x. 1),v)) . (x. 1)
by A25;
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in h . (x. 2) or a in f . (x. 0) )

assume A33: a in h . (x. 2) ; :: thesis: a in f . (x. 0)

h . (x. 2) c= E by A1;

then reconsider a9 = a as Element of E by A33;

set m = h +* ((x. 3),a9);

A34: (h +* ((x. 3),a9)) . (x. 3) = a9 by FUNCT_7:128;

for x being Variable st (h +* ((x. 3),a9)) . x <> h . x holds

x. 3 = x by FUNCT_7:32;

then A35: E,h +* ((x. 3),a9) |= ((x. 3) 'in' (x. 2)) => ((x. 3) 'in' (x. 0)) by A31, ZF_MODEL:16;

(h +* ((x. 3),a9)) . (x. 2) = h . (x. 2) by FUNCT_7:32;

then E,h +* ((x. 3),a9) |= (x. 3) 'in' (x. 2) by A33, A34, ZF_MODEL:13;

then E,h +* ((x. 3),a9) |= (x. 3) 'in' (x. 0) by A35, ZF_MODEL:18;

then A36: (h +* ((x. 3),a9)) . (x. 3) in (h +* ((x. 3),a9)) . (x. 0) by ZF_MODEL:13;

( (h +* ((x. 3),a9)) . (x. 0) = h . (x. 0) & (f +* ((x. 1),v)) . (x. 0) = f . (x. 0) ) by FUNCT_7:32;

hence a in f . (x. 0) by A25, A34, A36; :: thesis: verum

end;assume A33: a in h . (x. 2) ; :: thesis: a in f . (x. 0)

h . (x. 2) c= E by A1;

then reconsider a9 = a as Element of E by A33;

set m = h +* ((x. 3),a9);

A34: (h +* ((x. 3),a9)) . (x. 3) = a9 by FUNCT_7:128;

for x being Variable st (h +* ((x. 3),a9)) . x <> h . x holds

x. 3 = x by FUNCT_7:32;

then A35: E,h +* ((x. 3),a9) |= ((x. 3) 'in' (x. 2)) => ((x. 3) 'in' (x. 0)) by A31, ZF_MODEL:16;

(h +* ((x. 3),a9)) . (x. 2) = h . (x. 2) by FUNCT_7:32;

then E,h +* ((x. 3),a9) |= (x. 3) 'in' (x. 2) by A33, A34, ZF_MODEL:13;

then E,h +* ((x. 3),a9) |= (x. 3) 'in' (x. 0) by A35, ZF_MODEL:18;

then A36: (h +* ((x. 3),a9)) . (x. 3) in (h +* ((x. 3),a9)) . (x. 0) by ZF_MODEL:13;

( (h +* ((x. 3),a9)) . (x. 0) = h . (x. 0) & (f +* ((x. 1),v)) . (x. 0) = f . (x. 0) ) by FUNCT_7:32;

hence a in f . (x. 0) by A25, A34, A36; :: thesis: verum

then h . (x. 2) in h . (x. 1) by A24, A32, XBOOLE_0:def 4;

hence E,h |= (x. 2) 'in' (x. 1) by ZF_MODEL:13; :: thesis: verum

for x being Variable st (f +* ((x. 1),v)) . x <> f . x holds

x. 1 = x by FUNCT_7:32;

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 A37, ZF_MODEL:20; :: thesis: verum