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

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 )

let f be Function of VAR,E; :: according to ZF_MODEL:def 5 :: thesis: E,f |= the_axiom_of_pairs

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

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

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

assume A20:
for u, v being Element of E holds {u,v} in E
; :: thesis: E |= the_axiom_of_pairs
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 ) )

hence {u,v} in E ; :: thesis: verum

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

then
h . (x. 2) = {u,v}
by TARSKI:def 2;
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) )

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;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 A16:
( a = u or a = v )
; :: thesis: a in h . (x. 2)
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;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

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

hence {u,v} in E ; :: thesis: verum

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

hence
E,f |= the_axiom_of_pairs
by ZF_MODEL:21; :: thesis: verum( 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;

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

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

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