let W be Universe; :: thesis: for a being Ordinal of W
for phi being Ordinal-Sequence of W st omega in W & phi is increasing & phi is continuous holds
ex b being Ordinal of W st
( a in b & phi . b = b )
let a be Ordinal of W; :: thesis: for phi being Ordinal-Sequence of W st omega in W & phi is increasing & phi is continuous holds
ex b being Ordinal of W st
( a in b & phi . b = b )
let phi be Ordinal-Sequence of W; :: thesis: ( omega in W & phi is increasing & phi is continuous implies ex b being Ordinal of W st
( a in b & phi . b = b ) )
assume that
A1: omega in W and
A2: phi is increasing and
A3: phi is continuous ; :: thesis: ex b being Ordinal of W st
( a in b & phi . b = b )
deffunc H1( Ordinal of W) -> Element of W = (succ a) +^ (phi . $1);
consider xi being Ordinal-Sequence of W such that
A4: for b being Ordinal of W holds xi . b = H1(b) from ORDINAL4:sch 2();
 A5: dom xi = On W by FUNCT_2:def 1;
A6: dom phi = On W by FUNCT_2:def 1;
for A being Ordinal st A in dom phi holds
xi . A = (succ a) +^ (phi . A)
proof
let A be Ordinal; :: thesis: ( A in dom phi implies xi . A = (succ a) +^ (phi . A) )
assume A in dom phi ; :: thesis: xi . A = (succ a) +^ (phi . A)
then reconsider b = A as Ordinal of W by A6, ZF_REFLE:7;
xi . b = (succ a) +^ (phi . b) by A4;
hence xi . A = (succ a) +^ (phi . A) ; :: thesis: verum
end;
then xi = (succ a) +^ phi by A6, A5, ORDINAL3:def 1;
then ( xi is increasing & xi is continuous ) by A2, A3, Th14, Th16;
then consider A being Ordinal such that
A7: A in dom xi and
A8: xi . A = A by A1, ORDINAL4:36;
reconsider b = A as Ordinal of W by A5, A7, ZF_REFLE:7;
A9: b = (succ a) +^ (phi . b) by A4, A8;
take b ; :: thesis: ( a in b & phi . b = b )
A10: ( succ a c= (succ a) +^ (phi . b) & a in succ a ) by ORDINAL1:6, ORDINAL3:24;
A11: phi . b c= (succ a) +^ (phi . b) by ORDINAL3:24;
b c= phi . b by A2, A6, A5, A7, ORDINAL4:10;
hence ( a in b & phi . b = b ) by A10, A9, A11; :: thesis: verum