let W be Universe; :: thesis: for L being DOMAIN-Sequence of W st omega in W & ( for a, b being Ordinal of W st a in b holds
L . a c= L . b ) & ( for a being Ordinal of W st a <> {} & a is limit_ordinal holds
L . a = Union (L | a) ) holds
ex phi being Ordinal-Sequence of W st
( phi is increasing & phi is continuous & ( for a being Ordinal of W st phi . a = a & {} <> a holds
L . a <==> Union L ) )
let L be DOMAIN-Sequence of W; :: thesis: ( omega in W & ( for a, b being Ordinal of W st a in b holds
L . a c= L . b ) & ( for a being Ordinal of W st a <> {} & a is limit_ordinal holds
L . a = Union (L | a) ) implies ex phi being Ordinal-Sequence of W st
( phi is increasing & phi is continuous & ( for a being Ordinal of W st phi . a = a & {} <> a holds
L . a <==> Union L ) ) )
assume ( omega in W & ( for a, b being Ordinal of W st a in b holds
L . a c= L . b ) & ( for a being Ordinal of W st a <> {} & a is limit_ordinal holds
L . a = Union (L | a) ) ) ; :: thesis: ex phi being Ordinal-Sequence of W st
( phi is increasing & phi is continuous & ( for a being Ordinal of W st phi . a = a & {} <> a holds
L . a <==> Union L ) )
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 st phi . a = a & {} <> a holds
L . a is_elementary_subsystem_of Union L by Th30;
take phi ; :: thesis: ( phi is increasing & phi is continuous & ( for a being Ordinal of W st phi . a = a & {} <> a holds
L . a <==> Union L ) )
thus ( phi is increasing & phi is continuous ) by A1; :: thesis: for a being Ordinal of W st phi . a = a & {} <> a holds
L . a <==> Union L
let a be Ordinal of W; :: thesis: ( phi . a = a & {} <> a implies L . a <==> Union L )
assume ( phi . a = a & {} <> a ) ; :: thesis: L . a <==> Union L
hence L . a <==> Union L by A2, Th9; :: thesis: verum