let E be non empty set ; ( 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
; ORDINAL1:def 2 ( 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 )
( ( for u being Element of E holds union u in E ) implies E |= the_axiom_of_unions )proof
consider f0 being
Function of
VAR ,
E;
assume A2:
E |= the_axiom_of_unions
;
for u being Element of E holds union u in E
let u be
Element of
E;
union u in E
set f =
f0 +* (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:25;
then
E,
f0 +* (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 ))))))
by ZF_MODEL:def 5;
then consider g being
Function of
VAR ,
E such that A3:
for
x being
Variable st
g . x <> (f0 +* (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:
(f0 +* (x. 0 ),u) . (x. 0 ) = u
by FUNCT_7:130;
for
a being
set holds
(
a in g . (x. 1) iff ex
X being
set st
(
a in X &
X in u ) )
proof
let a be
set ;
( a in g . (x. 1) iff ex X being set st
( a in X & X in u ) )
A6:
g . (x. 0 ) = (f0 +* (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 ) )
( ex X being set st
( a in X & X in u ) implies a in g . (x. 1) )proof
assume A7:
a in g . (x. 1)
;
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:130;
for
x being
Variable st
(g +* (x. 2),a9) . x <> g . x holds
x. 2
= x
by FUNCT_7:34;
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:34;
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
;
( a in X & X in u )
A13:
(
(g +* (x. 2),a9) . (x. 0 ) = g . (x. 0 ) &
g . (x. 0 ) = (f0 +* (x. 0 ),u) . (x. 0 ) )
by A3, FUNCT_7:34;
(
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;
verum
end;
given X being
set such that A14:
a in X
and A15:
X in u
;
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:130;
(
((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:34;
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:130;
for
x being
Variable st
(g +* (x. 2),a9) . x <> g . x holds
x. 2
= x
by FUNCT_7:34;
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:34;
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:34, 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:34;
verum
end;
then
g . (x. 1) = union u
by TARSKI:def 4;
hence
union u in E
;
verum
end;
assume A20:
for u being Element of E holds union u in E
; E |= the_axiom_of_unions
now let f be
Function of
VAR ,
E;
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:130;
now let h be
Function of
VAR ,
E;
( ( 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
;
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
thus
(
E,
h |= (x. 2) 'in' (x. 1) implies
E,
h |= Ex (x. 3),
(((x. 2) 'in' (x. 3)) '&' ((x. 3) 'in' (x. 0 ))) )
( E,h |= Ex (x. 3),(((x. 2) 'in' (x. 3)) '&' ((x. 3) 'in' (x. 0 ))) implies E,h |= (x. 2) 'in' (x. 1) )proof
assume
E,
h |= (x. 2) 'in' (x. 1)
;
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:130;
A27:
(f +* (x. 1),v) . (x. 0 ) = f . (x. 0 )
by FUNCT_7:34;
(h +* (x. 3),X) . (x. 2) = h . (x. 2)
by FUNCT_7:34;
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:34;
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:34, ZF_MODEL:15;
hence
E,
h |= Ex (x. 3),
(((x. 2) 'in' (x. 3)) '&' ((x. 3) 'in' (x. 0 )))
by ZF_MODEL:20;
verum
end;
assume
E,
h |= Ex (x. 3),
(((x. 2) 'in' (x. 3)) '&' ((x. 3) 'in' (x. 0 )))
;
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:34;
(
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;
verum
end; 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;
verum end; then
( ( for
x being
Variable st
(f +* (x. 1),v) . x <> f . x holds
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:34, 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;
verum end;
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 ))))))
by ZF_MODEL:def 5;
hence
E |= the_axiom_of_unions
by ZF_MODEL:25; verum