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 H_{1}( 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 = H_{1}(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)

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

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 H

consider xi being Ordinal-Sequence of W such that

A4: for b being Ordinal of W holds xi . b = H

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

then
xi = (succ a) +^ phi
by A6, A5, ORDINAL3:def 1;
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;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

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