let E be non empty set ; ( 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
; ORDINAL1:def 2 ( 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. 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 )
( ( 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
;
for u, v being Element of E holds {u,v} in E
let u,
v be
Element of
E;
{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 ;
( a in h . (x. 2) iff ( a = u or a = v ) )
thus
( not
a in h . (x. 2) or
a = u or
a = v )
( ( a = u or a = v ) implies a in h . (x. 2) )proof
assume A11:
a in h . (x. 2)
;
( 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;
verum
end;
assume A16:
(
a = u or
a = v )
;
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;
verum
end;
then
h . (x. 2) = {u,v}
by TARSKI:def 2;
hence
{u,v} in E
;
verum
end;
assume A20:
for u, v being Element of E holds {u,v} in E
; E |= the_axiom_of_pairs
let f be Function of VAR,E; ZF_MODEL:def 5 E,f |= the_axiom_of_pairs
now 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;
( ( 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 )
;
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 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;
( ( 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
;
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;
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;
verum end;
hence
E,f |= the_axiom_of_pairs
by ZF_MODEL:21; verum