let W be Universe; :: thesis: ( 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 <==> W ) ) )
assume omega in W ; :: thesis: 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 <==> W ) )
then consider phi being Ordinal-Sequence of W such that
A1: ( phi is increasing & phi is continuous ) and
A2: 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 by Th33;
take phi ; :: thesis: ( 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 <==> W ) )
thus ( phi is increasing & phi is continuous ) by A1; :: thesis: for a being Ordinal of W
for M being non empty set st phi . a = a & {} <> a & M = Rank a holds
M <==> W
let a be Ordinal of W; :: thesis: for M being non empty set st phi . a = a & {} <> a & M = Rank a holds
M <==> W
let M be non empty set ; :: thesis: ( phi . a = a & {} <> a & M = Rank a implies M <==> W )
assume ( phi . a = a & {} <> a & M = Rank a ) ; :: thesis: M <==> W
hence M <==> W by A2, Th9; :: thesis: verum