let W be Universe; for L being DOMAIN-Sequence of W st ( for a, b being Ordinal of W st a in b holds
L . a c= L . b ) & ( for a being Ordinal of W holds
( L . a in Union L & L . a is epsilon-transitive ) ) & Union L is predicatively_closed holds
Union L |= the_axiom_of_power_sets
let L be DOMAIN-Sequence of W; ( ( for a, b being Ordinal of W st a in b holds
L . a c= L . b ) & ( for a being Ordinal of W holds
( L . a in Union L & L . a is epsilon-transitive ) ) & Union L is predicatively_closed implies Union L |= the_axiom_of_power_sets )
assume that
A1:
for a, b being Ordinal of W st a in b holds
L . a c= L . b
and
A2:
for a being Ordinal of W holds
( L . a in Union L & L . a is epsilon-transitive )
and
A3:
Union L is predicatively_closed
; Union L |= the_axiom_of_power_sets
set M = Union L;
A4:
for X being set
for a being Ordinal of W st X in L . a holds
(L . a) /\ (bool X) in Union L
A6:
now for X being set st X in Union L holds
(Union L) /\ (bool X) in Union Ldefpred S1[
set ,
set ]
means $1
in L . $2;
let X be
set ;
( X in Union L implies (Union L) /\ (bool X) in Union L )assume A7:
X in Union L
;
(Union L) /\ (bool X) in Union LA8:
X in bool X
by ZFMISC_1:def 1;
then reconsider D =
(Union L) /\ (bool X) as non
empty set by A7, XBOOLE_0:def 4;
A9:
X in (Union L) /\ (bool X)
by A7, A8, XBOOLE_0:def 4;
A10:
for
d being
Element of
D ex
a being
Ordinal of
W st
S1[
d,
a]
consider f being
Function such that A13:
(
dom f = D & ( for
d being
Element of
D ex
a being
Ordinal of
W st
(
a = f . d &
S1[
d,
a] & ( for
b being
Ordinal of
W st
S1[
d,
b] holds
a c= b ) ) ) )
from ZF_REFLE:sch 1(A10);
A14:
rng f c= W
A17:
(Union L) /\ (bool X) c= bool X
by XBOOLE_1:17;
bool X in W
by A7, CLASSES2:59;
then
D in W
by A17, CLASSES1:def 1;
then
(
rng f = f .: (dom f) &
card D in card W )
by CLASSES2:1, RELAT_1:113;
then
card (rng f) in card W
by A13, CARD_1:67, ORDINAL1:12;
then
rng f in W
by A14, CLASSES1:1;
then reconsider a =
sup (rng f) as
Ordinal of
W by ZF_REFLE:19;
A18:
D c= L . a
A21:
(L . a) /\ (bool X) c= D
by XBOOLE_1:26, ZF_REFLE:16;
D /\ (bool X) = (Union L) /\ ((bool X) /\ (bool X))
by XBOOLE_1:16;
then
D c= (L . a) /\ (bool X)
by A18, XBOOLE_1:26;
then
D = (L . a) /\ (bool X)
by A21;
hence
(Union L) /\ (bool X) in Union L
by A4, A9, A18;
verum end;
Union L is epsilon-transitive
hence
Union L |= the_axiom_of_power_sets
by A6, ZFMODEL1:9; verum