let E be non empty set ; :: thesis: ( E is epsilon-transitive implies ( E |= the_axiom_of_unions iff for u being Element of E holds union 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_unions iff for u being Element of E holds union u in E )

thus ( E |= the_axiom_of_unions implies for u being Element of E holds union u in E ) :: thesis: ( ( for u being Element of E holds union u in E ) implies E |= the_axiom_of_unions )

hence E |= the_axiom_of_unions by ZF_MODEL:23; :: thesis: verum

assume A1: for X being set st X in E holds

X c= E ; :: according to ORDINAL1:def 2 :: thesis: ( E |= the_axiom_of_unions iff for u being Element of E holds union u in E )

thus ( E |= the_axiom_of_unions implies for u being Element of E holds union u in E ) :: thesis: ( ( for u being Element of E holds union u in E ) implies E |= the_axiom_of_unions )

proof

assume A20:
for u being Element of E holds union u in E
; :: thesis: E |= the_axiom_of_unions
set f0 = the Function of VAR,E;

assume A2: E |= the_axiom_of_unions ; :: thesis: for u being Element of E holds union u in E

let u be Element of E; :: thesis: union 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)) <=> (Ex ((x. 3),(((x. 2) 'in' (x. 3)) '&' ((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)) <=> (Ex ((x. 3),(((x. 2) 'in' (x. 3)) '&' ((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)) <=> (Ex ((x. 3),(((x. 2) 'in' (x. 3)) '&' ((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;

for a being object holds

( a in g . (x. 1) iff ex X being set st

( a in X & X in u ) )

hence union u in E ; :: thesis: verum

end;assume A2: E |= the_axiom_of_unions ; :: thesis: for u being Element of E holds union u in E

let u be Element of E; :: thesis: union 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)) <=> (Ex ((x. 3),(((x. 2) 'in' (x. 3)) '&' ((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)) <=> (Ex ((x. 3),(((x. 2) 'in' (x. 3)) '&' ((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)) <=> (Ex ((x. 3),(((x. 2) 'in' (x. 3)) '&' ((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;

for a being object holds

( a in g . (x. 1) iff ex X being set st

( a in X & X in u ) )

proof

then
g . (x. 1) = union u
by TARSKI:def 4;
let a be object ; :: thesis: ( a in g . (x. 1) iff ex X being set st

( a in X & X in u ) )

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

thus ( a in g . (x. 1) implies ex X being set st

( a in X & X in u ) ) :: thesis: ( ex X being set st

( a in X & X in u ) implies a in g . (x. 1) )

A15: X in u ; :: thesis: a in g . (x. 1)

u c= E by A1;

then reconsider X = X as Element of E by A15;

X c= E by A1;

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

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

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

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

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

then A17: E,(g +* ((x. 2),a9)) +* ((x. 3),X) |= (x. 3) 'in' (x. 0) by A5, A15, A16, A6, ZF_MODEL:13;

A18: (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 A19: E,g +* ((x. 2),a9) |= ((x. 2) 'in' (x. 1)) <=> (Ex ((x. 3),(((x. 2) 'in' (x. 3)) '&' ((x. 3) 'in' (x. 0))))) by A4, ZF_MODEL:16;

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

then E,(g +* ((x. 2),a9)) +* ((x. 3),X) |= (x. 2) 'in' (x. 3) by A14, A18, A16, ZF_MODEL:13;

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

x. 3 = x ) & E,(g +* ((x. 2),a9)) +* ((x. 3),X) |= ((x. 2) 'in' (x. 3)) '&' ((x. 3) 'in' (x. 0)) ) by A17, FUNCT_7:32, ZF_MODEL:15;

then E,g +* ((x. 2),a9) |= Ex ((x. 3),(((x. 2) 'in' (x. 3)) '&' ((x. 3) 'in' (x. 0)))) by ZF_MODEL:20;

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

then (g +* ((x. 2),a9)) . (x. 2) in (g +* ((x. 2),a9)) . (x. 1) by ZF_MODEL:13;

hence a in g . (x. 1) by A18, FUNCT_7:32; :: thesis: verum

end;( a in X & X in u ) )

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

thus ( a in g . (x. 1) implies ex X being set st

( a in X & X in u ) ) :: thesis: ( ex X being set st

( a in X & X in u ) implies a in g . (x. 1) )

proof

given X being set such that A14:
a in X
and
assume A7:
a in g . (x. 1)
; :: thesis: ex X being set st

( a in X & X in u )

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

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

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

A8: (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 A9: E,g +* ((x. 2),a9) |= ((x. 2) 'in' (x. 1)) <=> (Ex ((x. 3),(((x. 2) 'in' (x. 3)) '&' ((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 A7, A8, ZF_MODEL:13;

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

then consider m being Function of VAR,E such that

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

x. 3 = x and

A11: E,m |= ((x. 2) 'in' (x. 3)) '&' ((x. 3) 'in' (x. 0)) by ZF_MODEL:20;

A12: ( m . (x. 0) = (g +* ((x. 2),a9)) . (x. 0) & m . (x. 2) = (g +* ((x. 2),a9)) . (x. 2) ) by A10;

reconsider X = m . (x. 3) as set ;

take X ; :: thesis: ( a in X & X in u )

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

( E,m |= (x. 2) 'in' (x. 3) & E,m |= (x. 3) 'in' (x. 0) ) by A11, ZF_MODEL:15;

hence ( a in X & X in u ) by A5, A8, A13, A12, ZF_MODEL:13; :: thesis: verum

end;( a in X & X in u )

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

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

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

A8: (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 A9: E,g +* ((x. 2),a9) |= ((x. 2) 'in' (x. 1)) <=> (Ex ((x. 3),(((x. 2) 'in' (x. 3)) '&' ((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 A7, A8, ZF_MODEL:13;

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

then consider m being Function of VAR,E such that

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

x. 3 = x and

A11: E,m |= ((x. 2) 'in' (x. 3)) '&' ((x. 3) 'in' (x. 0)) by ZF_MODEL:20;

A12: ( m . (x. 0) = (g +* ((x. 2),a9)) . (x. 0) & m . (x. 2) = (g +* ((x. 2),a9)) . (x. 2) ) by A10;

reconsider X = m . (x. 3) as set ;

take X ; :: thesis: ( a in X & X in u )

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

( E,m |= (x. 2) 'in' (x. 3) & E,m |= (x. 3) 'in' (x. 0) ) by A11, ZF_MODEL:15;

hence ( a in X & X in u ) by A5, A8, A13, A12, ZF_MODEL:13; :: thesis: verum

A15: X in u ; :: thesis: a in g . (x. 1)

u c= E by A1;

then reconsider X = X as Element of E by A15;

X c= E by A1;

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

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

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

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

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

then A17: E,(g +* ((x. 2),a9)) +* ((x. 3),X) |= (x. 3) 'in' (x. 0) by A5, A15, A16, A6, ZF_MODEL:13;

A18: (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 A19: E,g +* ((x. 2),a9) |= ((x. 2) 'in' (x. 1)) <=> (Ex ((x. 3),(((x. 2) 'in' (x. 3)) '&' ((x. 3) 'in' (x. 0))))) by A4, ZF_MODEL:16;

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

then E,(g +* ((x. 2),a9)) +* ((x. 3),X) |= (x. 2) 'in' (x. 3) by A14, A18, A16, ZF_MODEL:13;

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

x. 3 = x ) & E,(g +* ((x. 2),a9)) +* ((x. 3),X) |= ((x. 2) 'in' (x. 3)) '&' ((x. 3) 'in' (x. 0)) ) by A17, FUNCT_7:32, ZF_MODEL:15;

then E,g +* ((x. 2),a9) |= Ex ((x. 3),(((x. 2) 'in' (x. 3)) '&' ((x. 3) 'in' (x. 0)))) by ZF_MODEL:20;

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

then (g +* ((x. 2),a9)) . (x. 2) in (g +* ((x. 2),a9)) . (x. 1) by ZF_MODEL:13;

hence a in g . (x. 1) by A18, FUNCT_7:32; :: thesis: verum

hence union u in E ; :: thesis: verum

now :: thesis: for f being Function of VAR,E holds E,f |= Ex ((x. 1),(All ((x. 2),(((x. 2) 'in' (x. 1)) <=> (Ex ((x. 3),(((x. 2) 'in' (x. 3)) '&' ((x. 3) 'in' (x. 0)))))))))

then
E |= Ex ((x. 1),(All ((x. 2),(((x. 2) 'in' (x. 1)) <=> (Ex ((x. 3),(((x. 2) 'in' (x. 3)) '&' ((x. 3) 'in' (x. 0)))))))))
;let f be Function of VAR,E; :: thesis: E,f |= Ex ((x. 1),(All ((x. 2),(((x. 2) 'in' (x. 1)) <=> (Ex ((x. 3),(((x. 2) 'in' (x. 3)) '&' ((x. 3) 'in' (x. 0)))))))))

reconsider v = union (f . (x. 0)) as Element of E by A20;

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

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

x. 1 = x ) & E,f +* ((x. 1),v) |= All ((x. 2),(((x. 2) 'in' (x. 1)) <=> (Ex ((x. 3),(((x. 2) 'in' (x. 3)) '&' ((x. 3) 'in' (x. 0))))))) ) by FUNCT_7:32, ZF_MODEL:16;

hence E,f |= Ex ((x. 1),(All ((x. 2),(((x. 2) 'in' (x. 1)) <=> (Ex ((x. 3),(((x. 2) 'in' (x. 3)) '&' ((x. 3) 'in' (x. 0))))))))) by ZF_MODEL:20; :: thesis: verum

end;reconsider v = union (f . (x. 0)) as Element of E by A20;

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

A21: (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)) <=> (Ex ((x. 3),(((x. 2) 'in' (x. 3)) '&' ((x. 3) 'in' (x. 0)))))

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

E,h |= ((x. 2) 'in' (x. 1)) <=> (Ex ((x. 3),(((x. 2) 'in' (x. 3)) '&' ((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)) <=> (Ex ((x. 3),(((x. 2) 'in' (x. 3)) '&' ((x. 3) 'in' (x. 0))))) )

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

x. 2 = x ; :: thesis: E,h |= ((x. 2) 'in' (x. 1)) <=> (Ex ((x. 3),(((x. 2) 'in' (x. 3)) '&' ((x. 3) 'in' (x. 0)))))

then A23: h . (x. 1) = (f +* ((x. 1),v)) . (x. 1) ;

( E,h |= (x. 2) 'in' (x. 1) iff E,h |= Ex ((x. 3),(((x. 2) 'in' (x. 3)) '&' ((x. 3) 'in' (x. 0)))) )

end;x. 2 = x ) implies E,h |= ((x. 2) 'in' (x. 1)) <=> (Ex ((x. 3),(((x. 2) 'in' (x. 3)) '&' ((x. 3) 'in' (x. 0))))) )

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

x. 2 = x ; :: thesis: E,h |= ((x. 2) 'in' (x. 1)) <=> (Ex ((x. 3),(((x. 2) 'in' (x. 3)) '&' ((x. 3) 'in' (x. 0)))))

then A23: h . (x. 1) = (f +* ((x. 1),v)) . (x. 1) ;

( E,h |= (x. 2) 'in' (x. 1) iff E,h |= Ex ((x. 3),(((x. 2) 'in' (x. 3)) '&' ((x. 3) 'in' (x. 0)))) )

proof

hence
E,h |= ((x. 2) 'in' (x. 1)) <=> (Ex ((x. 3),(((x. 2) 'in' (x. 3)) '&' ((x. 3) 'in' (x. 0)))))
by ZF_MODEL:19; :: thesis: verum
thus
( E,h |= (x. 2) 'in' (x. 1) implies E,h |= Ex ((x. 3),(((x. 2) 'in' (x. 3)) '&' ((x. 3) 'in' (x. 0)))) )
:: thesis: ( E,h |= Ex ((x. 3),(((x. 2) 'in' (x. 3)) '&' ((x. 3) 'in' (x. 0)))) implies E,h |= (x. 2) 'in' (x. 1) )

then consider m being Function of VAR,E such that

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

x. 3 = x and

A30: E,m |= ((x. 2) 'in' (x. 3)) '&' ((x. 3) 'in' (x. 0)) by ZF_MODEL:20;

E,m |= (x. 3) 'in' (x. 0) by A30, ZF_MODEL:15;

then A31: m . (x. 3) in m . (x. 0) by ZF_MODEL:13;

E,m |= (x. 2) 'in' (x. 3) by A30, ZF_MODEL:15;

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

then A32: m . (x. 2) in union (m . (x. 0)) by A31, TARSKI:def 4;

A33: h . (x. 1) = (f +* ((x. 1),v)) . (x. 1) by A22;

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

( m . (x. 2) = h . (x. 2) & m . (x. 0) = h . (x. 0) ) by A29;

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

end;proof

assume
E,h |= Ex ((x. 3),(((x. 2) 'in' (x. 3)) '&' ((x. 3) 'in' (x. 0))))
; :: thesis: E,h |= (x. 2) 'in' (x. 1)
assume
E,h |= (x. 2) 'in' (x. 1)
; :: thesis: E,h |= Ex ((x. 3),(((x. 2) 'in' (x. 3)) '&' ((x. 3) 'in' (x. 0))))

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

then consider X being set such that

A24: h . (x. 2) in X and

A25: X in f . (x. 0) by A21, A23, TARSKI:def 4;

f . (x. 0) c= E by A1;

then reconsider X = X as Element of E by A25;

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

A26: (h +* ((x. 3),X)) . (x. 3) = X by FUNCT_7:128;

A27: (f +* ((x. 1),v)) . (x. 0) = f . (x. 0) by FUNCT_7:32;

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

then A28: E,h +* ((x. 3),X) |= (x. 2) 'in' (x. 3) by A24, A26, ZF_MODEL:13;

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

then E,h +* ((x. 3),X) |= (x. 3) 'in' (x. 0) by A25, A26, A27, ZF_MODEL:13;

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

x. 3 = x ) & E,h +* ((x. 3),X) |= ((x. 2) 'in' (x. 3)) '&' ((x. 3) 'in' (x. 0)) ) by A28, FUNCT_7:32, ZF_MODEL:15;

hence E,h |= Ex ((x. 3),(((x. 2) 'in' (x. 3)) '&' ((x. 3) 'in' (x. 0)))) by ZF_MODEL:20; :: thesis: verum

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

then consider X being set such that

A24: h . (x. 2) in X and

A25: X in f . (x. 0) by A21, A23, TARSKI:def 4;

f . (x. 0) c= E by A1;

then reconsider X = X as Element of E by A25;

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

A26: (h +* ((x. 3),X)) . (x. 3) = X by FUNCT_7:128;

A27: (f +* ((x. 1),v)) . (x. 0) = f . (x. 0) by FUNCT_7:32;

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

then A28: E,h +* ((x. 3),X) |= (x. 2) 'in' (x. 3) by A24, A26, ZF_MODEL:13;

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

then E,h +* ((x. 3),X) |= (x. 3) 'in' (x. 0) by A25, A26, A27, ZF_MODEL:13;

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

x. 3 = x ) & E,h +* ((x. 3),X) |= ((x. 2) 'in' (x. 3)) '&' ((x. 3) 'in' (x. 0)) ) by A28, FUNCT_7:32, ZF_MODEL:15;

hence E,h |= Ex ((x. 3),(((x. 2) 'in' (x. 3)) '&' ((x. 3) 'in' (x. 0)))) by ZF_MODEL:20; :: thesis: verum

then consider m being Function of VAR,E such that

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

x. 3 = x and

A30: E,m |= ((x. 2) 'in' (x. 3)) '&' ((x. 3) 'in' (x. 0)) by ZF_MODEL:20;

E,m |= (x. 3) 'in' (x. 0) by A30, ZF_MODEL:15;

then A31: m . (x. 3) in m . (x. 0) by ZF_MODEL:13;

E,m |= (x. 2) 'in' (x. 3) by A30, ZF_MODEL:15;

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

then A32: m . (x. 2) in union (m . (x. 0)) by A31, TARSKI:def 4;

A33: h . (x. 1) = (f +* ((x. 1),v)) . (x. 1) by A22;

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

( m . (x. 2) = h . (x. 2) & m . (x. 0) = h . (x. 0) ) by A29;

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

x. 1 = x ) & E,f +* ((x. 1),v) |= All ((x. 2),(((x. 2) 'in' (x. 1)) <=> (Ex ((x. 3),(((x. 2) 'in' (x. 3)) '&' ((x. 3) 'in' (x. 0))))))) ) by FUNCT_7:32, ZF_MODEL:16;

hence E,f |= Ex ((x. 1),(All ((x. 2),(((x. 2) 'in' (x. 1)) <=> (Ex ((x. 3),(((x. 2) 'in' (x. 3)) '&' ((x. 3) 'in' (x. 0))))))))) by ZF_MODEL:20; :: thesis: verum

hence E |= the_axiom_of_unions by ZF_MODEL:23; :: thesis: verum