let W be Universe; ( omega in W implies ex phi being Ordinal-Sequence of W st
( phi is increasing & phi is continuous & ( for a being Ordinal of W
for M being non empty set st phi . a = a & {} <> a & M = Rank a holds
M is_elementary_subsystem_of W ) ) )
deffunc H1( Ordinal, set ) -> set = Rank $1;
deffunc H2( Ordinal, set ) -> set = Rank (succ $1);
consider L being Sequence such that
A1:
( dom L = On W & ( 0 in On W implies L . 0 = Rank (1-element_of W) ) )
and
A2:
for A being Ordinal st succ A in On W holds
L . (succ A) = H2(A,L . A)
and
A3:
for A being Ordinal st A in On W & A <> 0 & A is limit_ordinal holds
L . A = H1(A,L | A)
from ORDINAL2:sch 5();
A4:
for a being Ordinal of W st a <> {} & a is limit_ordinal holds
L . a = Rank a
by A3, ZF_REFLE:7;
A5:
for a being Ordinal of W holds L . (succ a) = Rank (succ a)
by A2, ZF_REFLE:7;
A6:
for a being Ordinal of W st a <> {} holds
L . a = Rank a
rng L c= W
then reconsider L = L as Sequence of W by RELAT_1:def 19;
then reconsider L = L as DOMAIN-Sequence of W by A1, RELAT_1:def 9, ZF_REFLE:def 2;
A14:
Union L = W
A19:
0-element_of W in On W
by ZF_REFLE:7;
A20:
for a, b being Ordinal of W st a in b holds
L . a c= L . b
A24:
for a being Ordinal of W st a <> {} & a is limit_ordinal holds
L . a = Union (L | a)
proof
let a be
Ordinal of
W;
( a <> {} & a is limit_ordinal implies L . a = Union (L | a) )
assume that A25:
a <> {}
and A26:
a is
limit_ordinal
;
L . a = Union (L | a)
A27:
a in On W
by ZF_REFLE:7;
A28:
L . a = Rank a
by A4, A25, A26;
thus
L . a c= Union (L | a)
XBOOLE_0:def 10 Union (L | a) c= L . aproof
let e be
object ;
TARSKI:def 3 ( not e in L . a or e in Union (L | a) )
assume
e in L . a
;
e in Union (L | a)
then consider B being
Ordinal such that A29:
B in a
and A30:
e in Rank B
by A25, A26, A28, CLASSES1:31;
B in On W
by A27, A29, ORDINAL1:10;
then reconsider B =
B as
Ordinal of
W by ZF_REFLE:7;
A31:
(
succ B in On W &
Union (L | a) = union (rng (L | a)) )
by CARD_3:def 4, ZF_REFLE:7;
L . (succ B) = Rank (succ B)
by A5;
then A32:
Rank B c= L . (succ B)
by CLASSES1:33;
succ B in a
by A26, A29, ORDINAL1:28;
then
L . (succ B) c= Union (L | a)
by A1, A31, FUNCT_1:50, ZFMISC_1:74;
then
Rank B c= Union (L | a)
by A32;
hence
e in Union (L | a)
by A30;
verum
end;
let e be
object ;
TARSKI:def 3 ( not e in Union (L | a) or e in L . a )
assume
e in Union (L | a)
;
e in L . a
then
e in union (rng (L | a))
by CARD_3:def 4;
then consider X being
set such that A33:
e in X
and A34:
X in rng (L | a)
by TARSKI:def 4;
consider u being
object such that A35:
u in dom (L | a)
and A36:
X = (L | a) . u
by A34, FUNCT_1:def 3;
reconsider u =
u as
Ordinal by A35;
A37:
X = L . u
by A35, A36, FUNCT_1:47;
A38:
dom (L | a) c= a
by RELAT_1:58;
then
u in On W
by A27, A35, ORDINAL1:10;
then reconsider u =
u as
Ordinal of
W by ZF_REFLE:7;
L . u c= L . a
by A20, A35, A38;
hence
e in L . a
by A33, A37;
verum
end;
assume
omega in W
; ex phi being Ordinal-Sequence of W st
( phi is increasing & phi is continuous & ( for a being Ordinal of W
for M being non empty set st phi . a = a & {} <> a & M = Rank a holds
M is_elementary_subsystem_of W ) )
then consider phi being Ordinal-Sequence of W such that
A39:
( phi is increasing & phi is continuous )
and
A40:
for a being Ordinal of W st phi . a = a & {} <> a holds
L . a is_elementary_subsystem_of Union L
by A20, A24, Th30;
take
phi
; ( phi is increasing & phi is continuous & ( for a being Ordinal of W
for M being non empty set st phi . a = a & {} <> a & M = Rank a holds
M is_elementary_subsystem_of W ) )
thus
( phi is increasing & phi is continuous )
by A39; for a being Ordinal of W
for M being non empty set st phi . a = a & {} <> a & M = Rank a holds
M is_elementary_subsystem_of W
let a be Ordinal of W; for M being non empty set st phi . a = a & {} <> a & M = Rank a holds
M is_elementary_subsystem_of W
let M be non empty set ; ( phi . a = a & {} <> a & M = Rank a implies M is_elementary_subsystem_of W )
assume that
A41:
phi . a = a
and
A42:
{} <> a
and
A43:
M = Rank a
; M is_elementary_subsystem_of W
M = L . a
by A6, A42, A43;
hence
M is_elementary_subsystem_of W
by A40, A14, A41, A42; verum