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
A4:
( ( E |= All (x. 0 ),(All (x. 1),(Ex (x. 2),(All (x. 3),(((x. 3) 'in' (x. 2)) <=> (((x. 3) '=' (x. 0 )) 'or' ((x. 3) '=' (x. 1))))))) implies E |= All (x. 1),(Ex (x. 2),(All (x. 3),(((x. 3) 'in' (x. 2)) <=> (((x. 3) '=' (x. 0 )) 'or' ((x. 3) '=' (x. 1)))))) ) & ( E |= All (x. 1),(Ex (x. 2),(All (x. 3),(((x. 3) 'in' (x. 2)) <=> (((x. 3) '=' (x. 0 )) 'or' ((x. 3) '=' (x. 1)))))) implies E |= All (x. 0 ),(All (x. 1),(Ex (x. 2),(All (x. 3),(((x. 3) 'in' (x. 2)) <=> (((x. 3) '=' (x. 0 )) 'or' ((x. 3) '=' (x. 1))))))) ) & ( E |= All (x. 1),(Ex (x. 2),(All (x. 3),(((x. 3) 'in' (x. 2)) <=> (((x. 3) '=' (x. 0 )) 'or' ((x. 3) '=' (x. 1)))))) implies E |= Ex (x. 2),(All (x. 3),(((x. 3) 'in' (x. 2)) <=> (((x. 3) '=' (x. 0 )) 'or' ((x. 3) '=' (x. 1))))) ) & ( E |= Ex (x. 2),(All (x. 3),(((x. 3) 'in' (x. 2)) <=> (((x. 3) '=' (x. 0 )) 'or' ((x. 3) '=' (x. 1))))) implies E |= All (x. 1),(Ex (x. 2),(All (x. 3),(((x. 3) 'in' (x. 2)) <=> (((x. 3) '=' (x. 0 )) 'or' ((x. 3) '=' (x. 1)))))) ) )
by ZF_MODEL:25;
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 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
consider fv being
Function of
VAR ,
E;
set g =
fv +* (x. 0 ),
u;
A6:
(
(fv +* (x. 0 ),u) . (x. 0 ) = u & ( for
x being
Variable st
x <> x. 0 holds
(fv +* (x. 0 ),u) . x = fv . x ) )
by FUNCT_7:34, FUNCT_7:130;
set f =
(fv +* (x. 0 ),u) +* (x. 1),
v;
A7:
(
((fv +* (x. 0 ),u) +* (x. 1),v) . (x. 1) = v & ( for
x being
Variable st
x <> x. 1 holds
((fv +* (x. 0 ),u) +* (x. 1),v) . x = (fv +* (x. 0 ),u) . x ) )
by FUNCT_7:34, FUNCT_7:130;
A8:
((fv +* (x. 0 ),u) +* (x. 1),v) . (x. 0 ) = u
by A6, A7;
E,
(fv +* (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:def 5;
then consider h being
Function of
VAR ,
E such that A9:
( ( for
x being
Variable st
h . x <> ((fv +* (x. 0 ),u) +* (x. 1),v) . x holds
x. 2
= x ) &
E,
h |= All (x. 3),
(((x. 3) 'in' (x. 2)) <=> (((x. 3) '=' (x. 0 )) 'or' ((x. 3) '=' (x. 1)))) )
by ZF_MODEL:20;
for
a being
set holds
(
a in h . (x. 2) iff (
a = u or
a = v ) )
proof
let a be
set ;
:: 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 A10:
a in h . (x. 2)
;
:: thesis: ( a = u or a = v )
then reconsider a' =
a as
Element of
E by A2;
set f3 =
h +* (x. 3),
a';
A11:
(
(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
by A11;
then
E,
h +* (x. 3),
a' |= ((x. 3) 'in' (x. 2)) <=> (((x. 3) '=' (x. 0 )) 'or' ((x. 3) '=' (x. 1)))
by A9, ZF_MODEL:16;
then A12:
(
E,
h +* (x. 3),
a' |= (x. 3) 'in' (x. 2) iff
E,
h +* (x. 3),
a' |= ((x. 3) '=' (x. 0 )) 'or' ((x. 3) '=' (x. 1)) )
by ZF_MODEL:19;
(h +* (x. 3),a') . (x. 2) = h . (x. 2)
by A11;
then
(
E,
h +* (x. 3),
a' |= (x. 3) '=' (x. 0 ) or
E,
h +* (x. 3),
a' |= (x. 3) '=' (x. 1) )
by A10, A11, A12, ZF_MODEL:13, ZF_MODEL:17;
then A13:
(
(h +* (x. 3),a') . (x. 3) = (h +* (x. 3),a') . (x. 0 ) or
(h +* (x. 3),a') . (x. 3) = (h +* (x. 3),a') . (x. 1) )
by ZF_MODEL:12;
(
(h +* (x. 3),a') . (x. 0 ) = h . (x. 0 ) &
h . (x. 0 ) = ((fv +* (x. 0 ),u) +* (x. 1),v) . (x. 0 ) &
(h +* (x. 3),a') . (x. 1) = h . (x. 1) &
h . (x. 1) = ((fv +* (x. 0 ),u) +* (x. 1),v) . (x. 1) )
by A9, A11;
hence
(
a = u or
a = v )
by A6, A7, A11, A13;
:: thesis: verum
end;
assume A14:
(
a = u or
a = v )
;
:: thesis: a in h . (x. 2)
then reconsider a' =
a as
Element of
E ;
set f3 =
h +* (x. 3),
a';
A15:
(
(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
by A15;
then
E,
h +* (x. 3),
a' |= ((x. 3) 'in' (x. 2)) <=> (((x. 3) '=' (x. 0 )) 'or' ((x. 3) '=' (x. 1)))
by A9, ZF_MODEL:16;
then A16:
(
E,
h +* (x. 3),
a' |= (x. 3) 'in' (x. 2) iff
E,
h +* (x. 3),
a' |= ((x. 3) '=' (x. 0 )) 'or' ((x. 3) '=' (x. 1)) )
by ZF_MODEL:19;
(
(h +* (x. 3),a') . (x. 0 ) = h . (x. 0 ) &
h . (x. 0 ) = ((fv +* (x. 0 ),u) +* (x. 1),v) . (x. 0 ) &
(h +* (x. 3),a') . (x. 1) = h . (x. 1) &
h . (x. 1) = ((fv +* (x. 0 ),u) +* (x. 1),v) . (x. 1) )
by A9, A15;
then
(
E,
h +* (x. 3),
a' |= (x. 3) '=' (x. 0 ) or
E,
h +* (x. 3),
a' |= (x. 3) '=' (x. 1) )
by A7, A8, A14, A15, ZF_MODEL:12;
then
(h +* (x. 3),a') . (x. 3) in (h +* (x. 3),a') . (x. 2)
by A16, ZF_MODEL:13, ZF_MODEL:17;
hence
a in h . (x. 2)
by A15;
:: thesis: verum
end;
then
h . (x. 2) = {u,v}
by TARSKI:def 2;
hence
{u,v} in E
;
:: thesis: verum
end;
assume A17:
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 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 A17;
set h =
g +* (x. 2),
w;
A18:
(
(g +* (x. 2),w) . (x. 2) = w & ( for
x being
Variable st
x <> x. 2 holds
(g +* (x. 2),w) . x = g . x ) )
by FUNCT_7:34, FUNCT_7:130;
now 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))) )assume
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 A19:
(
(g +* (x. 2),w) . (x. 0 ) = g . (x. 0 ) &
m . (x. 0 ) = (g +* (x. 2),w) . (x. 0 ) &
(g +* (x. 2),w) . (x. 1) = g . (x. 1) &
m . (x. 1) = (g +* (x. 2),w) . (x. 1) &
m . (x. 2) = (g +* (x. 2),w) . (x. 2) )
by A18;
( (
E,
m |= (x. 3) 'in' (x. 2) implies
m . (x. 3) in m . (x. 2) ) & (
m . (x. 3) in m . (x. 2) implies
E,
m |= (x. 3) 'in' (x. 2) ) & (
E,
m |= (x. 3) '=' (x. 0 ) implies
m . (x. 3) = m . (x. 0 ) ) & (
m . (x. 3) = m . (x. 0 ) implies
E,
m |= (x. 3) '=' (x. 0 ) ) & (
E,
m |= (x. 3) '=' (x. 1) implies
m . (x. 3) = m . (x. 1) ) & (
m . (x. 3) = m . (x. 1) implies
E,
m |= (x. 3) '=' (x. 1) ) & ( not
E,
m |= ((x. 3) '=' (x. 0 )) 'or' ((x. 3) '=' (x. 1)) or
E,
m |= (x. 3) '=' (x. 0 ) or
E,
m |= (x. 3) '=' (x. 1) ) & ( (
E,
m |= (x. 3) '=' (x. 0 ) or
E,
m |= (x. 3) '=' (x. 1) ) implies
E,
m |= ((x. 3) '=' (x. 0 )) 'or' ((x. 3) '=' (x. 1)) ) )
by ZF_MODEL:12, ZF_MODEL:13, ZF_MODEL:17;
hence
E,
m |= ((x. 3) 'in' (x. 2)) <=> (((x. 3) '=' (x. 0 )) 'or' ((x. 3) '=' (x. 1)))
by A18, A19, TARSKI:def 2, ZF_MODEL:19;
:: thesis: verum end; then A20:
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 A18;
hence
E,
g |= Ex (x. 2),
(All (x. 3),(((x. 3) 'in' (x. 2)) <=> (((x. 3) '=' (x. 0 )) 'or' ((x. 3) '=' (x. 1)))))
by A20, ZF_MODEL:20;
:: thesis: verum end;
hence
E,f |= the_axiom_of_pairs
by ZF_MODEL:22; :: thesis: verum