let E be non empty set ; :: thesis: ( E is epsilon-transitive implies ( E |= the_axiom_of_pairs iff for u, v being Element of E holds {u,v} 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_pairs iff for u, v being Element of E holds {u,v} in E )
A2: for a being set
for u being Element of E st a in u holds
a is Element of E

proof

let a be set ; :: thesis: for u being Element of E st a in u holds
a is Element of E
let u be Element of E; :: thesis: ( a in u implies a is Element of E )
assume A3: a in u ; :: thesis: a is Element of E
u c= E by A1;
hence a is Element of E by A3; :: thesis: verum

end;

A4: ( E |= All ((x. 1),(Ex ((x. 2),(All ((x. 3),(((x. 3) 'in' (x. 2)) <=> (((x. 3) '=' (x. 0)) 'or' ((x. 3) '=' (x. 1))))))))) iff E |= Ex ((x. 2),(All ((x. 3),(((x. 3) 'in' (x. 2)) <=> (((x. 3) '=' (x. 0)) 'or' ((x. 3) '=' (x. 1))))))) ) by ZF_MODEL:23;
thus ( E |= the_axiom_of_pairs implies for u, v being Element of E holds {u,v} in E ) :: thesis: ( ( for u, v being Element of E holds {u,v} in E ) implies E |= the_axiom_of_pairs )

proof

set fv = the Function of VAR,E;
assume A5: E |= the_axiom_of_pairs ; :: thesis: for u, v being Element of E holds {u,v} in E
let u, v be Element of E; :: thesis: {u,v} in E
set g = the Function of VAR,E +* ((x. 0),u);
set f = ( the Function of VAR,E +* ((x. 0),u)) +* ((x. 1),v);
E,( the Function of VAR,E +* ((x. 0),u)) +* ((x. 1),v) |= Ex ((x. 2),(All ((x. 3),(((x. 3) 'in' (x. 2)) <=> (((x. 3) '=' (x. 0)) 'or' ((x. 3) '=' (x. 1))))))) by A4, A5, ZF_MODEL:23;
then consider h being Function of VAR,E such that
A6: for x being Variable st h . x <> (( the Function of VAR,E +* ((x. 0),u)) +* ((x. 1),v)) . x holds
x. 2 = x and
A7: E,h |= All ((x. 3),(((x. 3) 'in' (x. 2)) <=> (((x. 3) '=' (x. 0)) 'or' ((x. 3) '=' (x. 1))))) by ZF_MODEL:20;
A8: (( the Function of VAR,E +* ((x. 0),u)) +* ((x. 1),v)) . (x. 1) = v by FUNCT_7:128;
A9: ( the Function of VAR,E +* ((x. 0),u)) . (x. 0) = u by FUNCT_7:128;
then A10: (( the Function of VAR,E +* ((x. 0),u)) +* ((x. 1),v)) . (x. 0) = u by FUNCT_7:32;
for a being object holds
( a in h . (x. 2) iff ( a = u or a = v ) )

proof

let a be object ; :: thesis: ( a in h . (x. 2) iff ( a = u or a = v ) )
thus ( not a in h . (x. 2) or a = u or a = v ) :: thesis: ( ( a = u or a = v ) implies a in h . (x. 2) )

proof

assume A11: a in h . (x. 2) ; :: thesis: ( a = u or a = v )
then reconsider a9 = a as Element of E by A2;
set f3 = h +* ((x. 3),a9);
A12: (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 E,h +* ((x. 3),a9) |= ((x. 3) 'in' (x. 2)) <=> (((x. 3) '=' (x. 0)) 'or' ((x. 3) '=' (x. 1))) by A7, ZF_MODEL:16;
then A13: ( E,h +* ((x. 3),a9) |= (x. 3) 'in' (x. 2) iff E,h +* ((x. 3),a9) |= ((x. 3) '=' (x. 0)) 'or' ((x. 3) '=' (x. 1)) ) by ZF_MODEL:19;
(h +* ((x. 3),a9)) . (x. 2) = h . (x. 2) by FUNCT_7:32;
then ( E,h +* ((x. 3),a9) |= (x. 3) '=' (x. 0) or E,h +* ((x. 3),a9) |= (x. 3) '=' (x. 1) ) by A11, A12, A13, ZF_MODEL:13, ZF_MODEL:17;
then A14: ( (h +* ((x. 3),a9)) . (x. 3) = (h +* ((x. 3),a9)) . (x. 0) or (h +* ((x. 3),a9)) . (x. 3) = (h +* ((x. 3),a9)) . (x. 1) ) by ZF_MODEL:12;
A15: (h +* ((x. 3),a9)) . (x. 1) = h . (x. 1) by FUNCT_7:32;
( (h +* ((x. 3),a9)) . (x. 0) = h . (x. 0) & h . (x. 0) = (( the Function of VAR,E +* ((x. 0),u)) +* ((x. 1),v)) . (x. 0) ) by A6, FUNCT_7:32;
hence ( a = u or a = v ) by A9, A8, A6, A12, A14, A15, FUNCT_7:32; :: thesis: verum

end;

assume A16: ( a = u or a = v ) ; :: thesis: a in h . (x. 2)
then reconsider a9 = a as Element of E ;
set f3 = h +* ((x. 3),a9);
A17: (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 E,h +* ((x. 3),a9) |= ((x. 3) 'in' (x. 2)) <=> (((x. 3) '=' (x. 0)) 'or' ((x. 3) '=' (x. 1))) by A7, ZF_MODEL:16;
then A18: ( E,h +* ((x. 3),a9) |= (x. 3) 'in' (x. 2) iff E,h +* ((x. 3),a9) |= ((x. 3) '=' (x. 0)) 'or' ((x. 3) '=' (x. 1)) ) by ZF_MODEL:19;
A19: ( (h +* ((x. 3),a9)) . (x. 1) = h . (x. 1) & h . (x. 1) = (( the Function of VAR,E +* ((x. 0),u)) +* ((x. 1),v)) . (x. 1) ) by A6, FUNCT_7:32;
( (h +* ((x. 3),a9)) . (x. 0) = h . (x. 0) & h . (x. 0) = (( the Function of VAR,E +* ((x. 0),u)) +* ((x. 1),v)) . (x. 0) ) by A6, FUNCT_7:32;
then ( E,h +* ((x. 3),a9) |= (x. 3) '=' (x. 0) or E,h +* ((x. 3),a9) |= (x. 3) '=' (x. 1) ) by A8, A10, A16, A17, A19, ZF_MODEL:12;
then (h +* ((x. 3),a9)) . (x. 3) in (h +* ((x. 3),a9)) . (x. 2) by A18, ZF_MODEL:13, ZF_MODEL:17;
hence a in h . (x. 2) by A17, FUNCT_7:32; :: thesis: verum

end;

then h . (x. 2) = {u,v} by TARSKI:def 2;
hence {u,v} in E ; :: thesis: verum

end;

assume A20: for u, v being Element of E holds {u,v} in E ; :: thesis: E |= the_axiom_of_pairs
let f be Function of VAR,E; :: according to ZF_MODEL:def 5 :: thesis: E,f |= the_axiom_of_pairs

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

let g be Function of VAR,E; :: thesis: ( ( for x being Variable holds
( not g . x <> f . x or x. 0 = x or x. 1 = x ) ) implies E,g |= Ex ((x. 2),(All ((x. 3),(((x. 3) 'in' (x. 2)) <=> (((x. 3) '=' (x. 0)) 'or' ((x. 3) '=' (x. 1))))))) )
assume for x being Variable holds
( not g . x <> f . x or x. 0 = x or x. 1 = x ) ; :: thesis: E,g |= Ex ((x. 2),(All ((x. 3),(((x. 3) 'in' (x. 2)) <=> (((x. 3) '=' (x. 0)) 'or' ((x. 3) '=' (x. 1)))))))
reconsider w = {(g . (x. 0)),(g . (x. 1))} as Element of E by A20;
set h = g +* ((x. 2),w);
A21: (g +* ((x. 2),w)) . (x. 2) = w by FUNCT_7:128;

now :: thesis: for m being Function of VAR,E st ( for x being Variable st m . x <> (g +* ((x. 2),w)) . x holds
x. 3 = x ) holds
E,m |= ((x. 3) 'in' (x. 2)) <=> (((x. 3) '=' (x. 0)) 'or' ((x. 3) '=' (x. 1)))

let m be Function of VAR,E; :: thesis: ( ( for x being Variable st m . x <> (g +* ((x. 2),w)) . x holds
x. 3 = x ) implies E,m |= ((x. 3) 'in' (x. 2)) <=> (((x. 3) '=' (x. 0)) 'or' ((x. 3) '=' (x. 1))) )
A22: ( (g +* ((x. 2),w)) . (x. 0) = g . (x. 0) & (g +* ((x. 2),w)) . (x. 1) = g . (x. 1) ) by FUNCT_7:32;
A23: ( E,m |= (x. 3) 'in' (x. 2) iff m . (x. 3) in m . (x. 2) ) by ZF_MODEL:13;
A24: ( E,m |= ((x. 3) '=' (x. 0)) 'or' ((x. 3) '=' (x. 1)) iff ( E,m |= (x. 3) '=' (x. 0) or E,m |= (x. 3) '=' (x. 1) ) ) by ZF_MODEL:17;
A25: ( E,m |= (x. 3) '=' (x. 1) iff m . (x. 3) = m . (x. 1) ) by ZF_MODEL:12;
A26: ( E,m |= (x. 3) '=' (x. 0) iff m . (x. 3) = m . (x. 0) ) by ZF_MODEL:12;
assume A27: for x being Variable st m . x <> (g +* ((x. 2),w)) . x holds
x. 3 = x ; :: thesis: E,m |= ((x. 3) 'in' (x. 2)) <=> (((x. 3) '=' (x. 0)) 'or' ((x. 3) '=' (x. 1)))
then A28: m . (x. 2) = (g +* ((x. 2),w)) . (x. 2) ;
( m . (x. 0) = (g +* ((x. 2),w)) . (x. 0) & m . (x. 1) = (g +* ((x. 2),w)) . (x. 1) ) by A27;
hence E,m |= ((x. 3) 'in' (x. 2)) <=> (((x. 3) '=' (x. 0)) 'or' ((x. 3) '=' (x. 1))) by A21, A22, A28, A23, A26, A25, A24, TARSKI:def 2, ZF_MODEL:19; :: thesis: verum

end;

then A29: E,g +* ((x. 2),w) |= All ((x. 3),(((x. 3) 'in' (x. 2)) <=> (((x. 3) '=' (x. 0)) 'or' ((x. 3) '=' (x. 1))))) by ZF_MODEL:16;
for x being Variable st (g +* ((x. 2),w)) . x <> g . x holds
x. 2 = x by FUNCT_7:32;
hence E,g |= Ex ((x. 2),(All ((x. 3),(((x. 3) 'in' (x. 2)) <=> (((x. 3) '=' (x. 0)) 'or' ((x. 3) '=' (x. 1))))))) by A29, ZF_MODEL:20; :: thesis: verum

end;

hence E,f |= the_axiom_of_pairs by ZF_MODEL:21; :: thesis: verum