let W be Universe; :: thesis: for D being non empty set

for Phi being Function of D,(Funcs ((On W),(On W))) st card D in card W holds

ex phi being Ordinal-Sequence of W st

( phi is increasing & phi is continuous & phi . (0-element_of W) = 0-element_of W & ( for a being Ordinal of W holds phi . (succ a) = sup ({(phi . a)} \/ ((uncurry Phi) .: [:D,{(succ a)}:])) ) & ( for a being Ordinal of W st a <> 0-element_of W & a is limit_ordinal holds

phi . a = sup (phi | a) ) )

deffunc H_{1}( set , Sequence) -> set = sup $2;

let D be non empty set ; :: thesis: for Phi being Function of D,(Funcs ((On W),(On W))) st card D in card W holds

ex phi being Ordinal-Sequence of W st

( phi is increasing & phi is continuous & phi . (0-element_of W) = 0-element_of W & ( for a being Ordinal of W holds phi . (succ a) = sup ({(phi . a)} \/ ((uncurry Phi) .: [:D,{(succ a)}:])) ) & ( for a being Ordinal of W st a <> 0-element_of W & a is limit_ordinal holds

phi . a = sup (phi | a) ) )

let Phi be Function of D,(Funcs ((On W),(On W))); :: thesis: ( card D in card W implies ex phi being Ordinal-Sequence of W st

( phi is increasing & phi is continuous & phi . (0-element_of W) = 0-element_of W & ( for a being Ordinal of W holds phi . (succ a) = sup ({(phi . a)} \/ ((uncurry Phi) .: [:D,{(succ a)}:])) ) & ( for a being Ordinal of W st a <> 0-element_of W & a is limit_ordinal holds

phi . a = sup (phi | a) ) ) )

assume A1: card D in card W ; :: thesis: ex phi being Ordinal-Sequence of W st

( phi is increasing & phi is continuous & phi . (0-element_of W) = 0-element_of W & ( for a being Ordinal of W holds phi . (succ a) = sup ({(phi . a)} \/ ((uncurry Phi) .: [:D,{(succ a)}:])) ) & ( for a being Ordinal of W st a <> 0-element_of W & a is limit_ordinal holds

phi . a = sup (phi | a) ) )

deffunc H_{2}( Ordinal, Ordinal) -> set = sup ({$2} \/ ((uncurry Phi) .: [:D,{(succ $1)}:]));

consider L being Ordinal-Sequence such that

A2: ( dom L = On W & ( 0 in On W implies L . 0 = 0 ) ) and

A3: for A being Ordinal st succ A in On W holds

L . (succ A) = H_{2}(A,L . A)
and

A4: for A being Ordinal st A in On W & A <> 0 & A is limit_ordinal holds

L . A = H_{1}(A,L | A)
from ORDINAL2:sch 11();

defpred S_{2}[ Ordinal] means L . $1 in On W;

A5: for a being Ordinal of W st S_{2}[a] holds

S_{2}[ succ a]

S_{2}[b] ) holds

S_{2}[a]
_{2}[ 0-element_of W]
by A2, ORDINAL1:def 9;

rng L c= On W

take phi ; :: thesis: ( phi is increasing & phi is continuous & phi . (0-element_of W) = 0-element_of W & ( for a being Ordinal of W holds phi . (succ a) = sup ({(phi . a)} \/ ((uncurry Phi) .: [:D,{(succ a)}:])) ) & ( for a being Ordinal of W st a <> 0-element_of W & a is limit_ordinal holds

phi . a = sup (phi | a) ) )

thus A22: phi is increasing :: thesis: ( phi is continuous & phi . (0-element_of W) = 0-element_of W & ( for a being Ordinal of W holds phi . (succ a) = sup ({(phi . a)} \/ ((uncurry Phi) .: [:D,{(succ a)}:])) ) & ( for a being Ordinal of W st a <> 0-element_of W & a is limit_ordinal holds

phi . a = sup (phi | a) ) )

phi . a = sup (phi | a) ) )

phi . a = sup (phi | a) ) )

thus for a being Ordinal of W holds phi . (succ a) = sup ({(phi . a)} \/ ((uncurry Phi) .: [:D,{(succ a)}:])) by A3, ZF_REFLE:7; :: thesis: for a being Ordinal of W st a <> 0-element_of W & a is limit_ordinal holds

phi . a = sup (phi | a)

let a be Ordinal of W; :: thesis: ( a <> 0-element_of W & a is limit_ordinal implies phi . a = sup (phi | a) )

a in On W by ZF_REFLE:7;

hence ( a <> 0-element_of W & a is limit_ordinal implies phi . a = sup (phi | a) ) by A4; :: thesis: verum

for Phi being Function of D,(Funcs ((On W),(On W))) st card D in card W holds

ex phi being Ordinal-Sequence of W st

( phi is increasing & phi is continuous & phi . (0-element_of W) = 0-element_of W & ( for a being Ordinal of W holds phi . (succ a) = sup ({(phi . a)} \/ ((uncurry Phi) .: [:D,{(succ a)}:])) ) & ( for a being Ordinal of W st a <> 0-element_of W & a is limit_ordinal holds

phi . a = sup (phi | a) ) )

deffunc H

let D be non empty set ; :: thesis: for Phi being Function of D,(Funcs ((On W),(On W))) st card D in card W holds

ex phi being Ordinal-Sequence of W st

( phi is increasing & phi is continuous & phi . (0-element_of W) = 0-element_of W & ( for a being Ordinal of W holds phi . (succ a) = sup ({(phi . a)} \/ ((uncurry Phi) .: [:D,{(succ a)}:])) ) & ( for a being Ordinal of W st a <> 0-element_of W & a is limit_ordinal holds

phi . a = sup (phi | a) ) )

let Phi be Function of D,(Funcs ((On W),(On W))); :: thesis: ( card D in card W implies ex phi being Ordinal-Sequence of W st

( phi is increasing & phi is continuous & phi . (0-element_of W) = 0-element_of W & ( for a being Ordinal of W holds phi . (succ a) = sup ({(phi . a)} \/ ((uncurry Phi) .: [:D,{(succ a)}:])) ) & ( for a being Ordinal of W st a <> 0-element_of W & a is limit_ordinal holds

phi . a = sup (phi | a) ) ) )

assume A1: card D in card W ; :: thesis: ex phi being Ordinal-Sequence of W st

( phi is increasing & phi is continuous & phi . (0-element_of W) = 0-element_of W & ( for a being Ordinal of W holds phi . (succ a) = sup ({(phi . a)} \/ ((uncurry Phi) .: [:D,{(succ a)}:])) ) & ( for a being Ordinal of W st a <> 0-element_of W & a is limit_ordinal holds

phi . a = sup (phi | a) ) )

deffunc H

consider L being Ordinal-Sequence such that

A2: ( dom L = On W & ( 0 in On W implies L . 0 = 0 ) ) and

A3: for A being Ordinal st succ A in On W holds

L . (succ A) = H

A4: for A being Ordinal st A in On W & A <> 0 & A is limit_ordinal holds

L . A = H

defpred S

A5: for a being Ordinal of W st S

S

proof

A10:
for a being Ordinal of W st a <> 0-element_of W & a is limit_ordinal & ( for b being Ordinal of W st b in a holds
let a be Ordinal of W; :: thesis: ( S_{2}[a] implies S_{2}[ succ a] )

A6: On W c= W by ORDINAL2:7;

assume L . a in On W ; :: thesis: S_{2}[ succ a]

then reconsider b = L . a as Ordinal of W by ZF_REFLE:7;

card [:D,{(succ a)}:] = card D by CARD_1:69;

then card ((uncurry Phi) .: [:D,{(succ a)}:]) c= card D by CARD_1:66;

then A7: card ((uncurry Phi) .: [:D,{(succ a)}:]) in card W by A1, ORDINAL1:12;

rng Phi c= Funcs ((On W),(On W)) by RELAT_1:def 19;

then A8: rng (uncurry Phi) c= On W by FUNCT_5:41;

(uncurry Phi) .: [:D,{(succ a)}:] c= rng (uncurry Phi) by RELAT_1:111;

then (uncurry Phi) .: [:D,{(succ a)}:] c= On W by A8;

then (uncurry Phi) .: [:D,{(succ a)}:] c= W by A6;

then (uncurry Phi) .: [:D,{(succ a)}:] in W by A7, CLASSES1:1;

then A9: {b} \/ ((uncurry Phi) .: [:D,{(succ a)}:]) in W by CLASSES2:60;

succ a in On W by ZF_REFLE:7;

then L . (succ a) = sup ({b} \/ ((uncurry Phi) .: [:D,{(succ a)}:])) by A3;

then L . (succ a) in W by A9, ZF_REFLE:19;

hence S_{2}[ succ a]
by ORDINAL1:def 9; :: thesis: verum

end;A6: On W c= W by ORDINAL2:7;

assume L . a in On W ; :: thesis: S

then reconsider b = L . a as Ordinal of W by ZF_REFLE:7;

card [:D,{(succ a)}:] = card D by CARD_1:69;

then card ((uncurry Phi) .: [:D,{(succ a)}:]) c= card D by CARD_1:66;

then A7: card ((uncurry Phi) .: [:D,{(succ a)}:]) in card W by A1, ORDINAL1:12;

rng Phi c= Funcs ((On W),(On W)) by RELAT_1:def 19;

then A8: rng (uncurry Phi) c= On W by FUNCT_5:41;

(uncurry Phi) .: [:D,{(succ a)}:] c= rng (uncurry Phi) by RELAT_1:111;

then (uncurry Phi) .: [:D,{(succ a)}:] c= On W by A8;

then (uncurry Phi) .: [:D,{(succ a)}:] c= W by A6;

then (uncurry Phi) .: [:D,{(succ a)}:] in W by A7, CLASSES1:1;

then A9: {b} \/ ((uncurry Phi) .: [:D,{(succ a)}:]) in W by CLASSES2:60;

succ a in On W by ZF_REFLE:7;

then L . (succ a) = sup ({b} \/ ((uncurry Phi) .: [:D,{(succ a)}:])) by A3;

then L . (succ a) in W by A9, ZF_REFLE:19;

hence S

S

S

proof

A19:
S
let a be Ordinal of W; :: thesis: ( a <> 0-element_of W & a is limit_ordinal & ( for b being Ordinal of W st b in a holds

S_{2}[b] ) implies S_{2}[a] )

assume that

A11: ( a <> 0-element_of W & a is limit_ordinal ) and

A12: for b being Ordinal of W st b in a holds

L . b in On W ; :: thesis: S_{2}[a]

A13: dom (L | a) c= a by RELAT_1:58;

then A14: dom (L | a) in W by CLASSES1:def 1;

A15: a in On W by ZF_REFLE:7;

A16: rng (L | a) c= W

then L . a in W by A14, A16, Th11, ZF_REFLE:19;

hence S_{2}[a]
by ORDINAL1:def 9; :: thesis: verum

end;S

assume that

A11: ( a <> 0-element_of W & a is limit_ordinal ) and

A12: for b being Ordinal of W st b in a holds

L . b in On W ; :: thesis: S

A13: dom (L | a) c= a by RELAT_1:58;

then A14: dom (L | a) in W by CLASSES1:def 1;

A15: a in On W by ZF_REFLE:7;

A16: rng (L | a) c= W

proof

L . a = sup (L | a)
by A4, A11, A15;
let e be object ; :: according to TARSKI:def 3 :: thesis: ( not e in rng (L | a) or e in W )

assume e in rng (L | a) ; :: thesis: e in W

then consider u being object such that

A17: u in dom (L | a) and

A18: e = (L | a) . u by FUNCT_1:def 3;

reconsider u = u as Ordinal by A17;

u in On W by A15, A13, A17, ORDINAL1:10;

then reconsider u = u as Ordinal of W by ZF_REFLE:7;

e = L . u by A17, A18, FUNCT_1:47;

then e in On W by A12, A13, A17;

hence e in W by ORDINAL1:def 9; :: thesis: verum

end;assume e in rng (L | a) ; :: thesis: e in W

then consider u being object such that

A17: u in dom (L | a) and

A18: e = (L | a) . u by FUNCT_1:def 3;

reconsider u = u as Ordinal by A17;

u in On W by A15, A13, A17, ORDINAL1:10;

then reconsider u = u as Ordinal of W by ZF_REFLE:7;

e = L . u by A17, A18, FUNCT_1:47;

then e in On W by A12, A13, A17;

hence e in W by ORDINAL1:def 9; :: thesis: verum

then L . a in W by A14, A16, Th11, ZF_REFLE:19;

hence S

rng L c= On W

proof

then reconsider phi = L as Ordinal-Sequence of W by A2, FUNCT_2:def 1, RELSET_1:4;
let e be object ; :: according to TARSKI:def 3 :: thesis: ( not e in rng L or e in On W )

assume e in rng L ; :: thesis: e in On W

then consider u being object such that

A20: u in dom L and

A21: e = L . u by FUNCT_1:def 3;

reconsider u = u as Ordinal of W by A2, A20, ZF_REFLE:7;

for a being Ordinal of W holds S_{2}[a]
from ZF_REFLE:sch 4(A19, A5, A10);

then L . u in On W ;

hence e in On W by A21; :: thesis: verum

end;assume e in rng L ; :: thesis: e in On W

then consider u being object such that

A20: u in dom L and

A21: e = L . u by FUNCT_1:def 3;

reconsider u = u as Ordinal of W by A2, A20, ZF_REFLE:7;

for a being Ordinal of W holds S

then L . u in On W ;

hence e in On W by A21; :: thesis: verum

take phi ; :: thesis: ( phi is increasing & phi is continuous & phi . (0-element_of W) = 0-element_of W & ( for a being Ordinal of W holds phi . (succ a) = sup ({(phi . a)} \/ ((uncurry Phi) .: [:D,{(succ a)}:])) ) & ( for a being Ordinal of W st a <> 0-element_of W & a is limit_ordinal holds

phi . a = sup (phi | a) ) )

thus A22: phi is increasing :: thesis: ( phi is continuous & phi . (0-element_of W) = 0-element_of W & ( for a being Ordinal of W holds phi . (succ a) = sup ({(phi . a)} \/ ((uncurry Phi) .: [:D,{(succ a)}:])) ) & ( for a being Ordinal of W st a <> 0-element_of W & a is limit_ordinal holds

phi . a = sup (phi | a) ) )

proof

thus
phi is continuous
:: thesis: ( phi . (0-element_of W) = 0-element_of W & ( for a being Ordinal of W holds phi . (succ a) = sup ({(phi . a)} \/ ((uncurry Phi) .: [:D,{(succ a)}:])) ) & ( for a being Ordinal of W st a <> 0-element_of W & a is limit_ordinal holds
let A be Ordinal; :: according to ORDINAL2:def 12 :: thesis: for b_{1} being set holds

( not A in b_{1} or not b_{1} in dom phi or phi . A in phi . b_{1} )

let B be Ordinal; :: thesis: ( not A in B or not B in dom phi or phi . A in phi . B )

assume that

A23: A in B and

A24: B in dom phi ; :: thesis: phi . A in phi . B

A in dom phi by A23, A24, ORDINAL1:10;

then reconsider a = A, b = B as Ordinal of W by A2, A24, ZF_REFLE:7;

defpred S_{3}[ Ordinal] means ( a in $1 implies phi . a in phi . $1 );

A25: for b being Ordinal of W st S_{3}[b] holds

S_{3}[ succ b]

S_{3}[c] ) holds

S_{3}[b]
_{3}[ 0-element_of W]
;

for b being Ordinal of W holds S_{3}[b]
from ZF_REFLE:sch 4(A32, A25, A28);

then phi . a in phi . b by A23;

hence phi . A in phi . B ; :: thesis: verum

end;( not A in b

let B be Ordinal; :: thesis: ( not A in B or not B in dom phi or phi . A in phi . B )

assume that

A23: A in B and

A24: B in dom phi ; :: thesis: phi . A in phi . B

A in dom phi by A23, A24, ORDINAL1:10;

then reconsider a = A, b = B as Ordinal of W by A2, A24, ZF_REFLE:7;

defpred S

A25: for b being Ordinal of W st S

S

proof

A28:
for b being Ordinal of W st b <> 0-element_of W & b is limit_ordinal & ( for c being Ordinal of W st c in b holds
let b be Ordinal of W; :: thesis: ( S_{3}[b] implies S_{3}[ succ b] )

assume A26: ( ( a in b implies phi . a in phi . b ) & a in succ b ) ; :: thesis: phi . a in phi . (succ b)

phi . b in {(phi . b)} by TARSKI:def 1;

then A27: phi . b in {(phi . b)} \/ ((uncurry Phi) .: [:D,{(succ b)}:]) by XBOOLE_0:def 3;

succ b in On W by ZF_REFLE:7;

then phi . (succ b) = sup ({(phi . b)} \/ ((uncurry Phi) .: [:D,{(succ b)}:])) by A3;

then phi . b in phi . (succ b) by A27, ORDINAL2:19;

hence phi . a in phi . (succ b) by A26, ORDINAL1:8, ORDINAL1:10; :: thesis: verum

end;assume A26: ( ( a in b implies phi . a in phi . b ) & a in succ b ) ; :: thesis: phi . a in phi . (succ b)

phi . b in {(phi . b)} by TARSKI:def 1;

then A27: phi . b in {(phi . b)} \/ ((uncurry Phi) .: [:D,{(succ b)}:]) by XBOOLE_0:def 3;

succ b in On W by ZF_REFLE:7;

then phi . (succ b) = sup ({(phi . b)} \/ ((uncurry Phi) .: [:D,{(succ b)}:])) by A3;

then phi . b in phi . (succ b) by A27, ORDINAL2:19;

hence phi . a in phi . (succ b) by A26, ORDINAL1:8, ORDINAL1:10; :: thesis: verum

S

S

proof

A32:
S
let b be Ordinal of W; :: thesis: ( b <> 0-element_of W & b is limit_ordinal & ( for c being Ordinal of W st c in b holds

S_{3}[c] ) implies S_{3}[b] )

assume that

A29: ( b <> 0-element_of W & b is limit_ordinal ) and

for c being Ordinal of W st c in b & a in c holds

phi . a in phi . c and

A30: a in b ; :: thesis: phi . a in phi . b

b in On W by ZF_REFLE:7;

then A31: phi . b = sup (phi | b) by A4, A29;

a in On W by ZF_REFLE:7;

then phi . a in rng (phi | b) by A2, A30, FUNCT_1:50;

hence phi . a in phi . b by A31, ORDINAL2:19; :: thesis: verum

end;S

assume that

A29: ( b <> 0-element_of W & b is limit_ordinal ) and

for c being Ordinal of W st c in b & a in c holds

phi . a in phi . c and

A30: a in b ; :: thesis: phi . a in phi . b

b in On W by ZF_REFLE:7;

then A31: phi . b = sup (phi | b) by A4, A29;

a in On W by ZF_REFLE:7;

then phi . a in rng (phi | b) by A2, A30, FUNCT_1:50;

hence phi . a in phi . b by A31, ORDINAL2:19; :: thesis: verum

for b being Ordinal of W holds S

then phi . a in phi . b by A23;

hence phi . A in phi . B ; :: thesis: verum

phi . a = sup (phi | a) ) )

proof

thus
phi . (0-element_of W) = 0-element_of W
by A2, ORDINAL1:def 9; :: thesis: ( ( for a being Ordinal of W holds phi . (succ a) = sup ({(phi . a)} \/ ((uncurry Phi) .: [:D,{(succ a)}:])) ) & ( for a being Ordinal of W st a <> 0-element_of W & a is limit_ordinal holds
let A be Ordinal; :: according to ORDINAL2:def 13 :: thesis: for b_{1} being set holds

( not A in dom phi or A = 0 or not A is limit_ordinal or not b_{1} = phi . A or b_{1} is_limes_of phi | A )

let B be Ordinal; :: thesis: ( not A in dom phi or A = 0 or not A is limit_ordinal or not B = phi . A or B is_limes_of phi | A )

assume that

A33: A in dom phi and

A34: ( A <> 0 & A is limit_ordinal ) and

A35: B = phi . A ; :: thesis: B is_limes_of phi | A

A c= dom phi by A33, ORDINAL1:def 2;

then A36: dom (phi | A) = A by RELAT_1:62;

A37: phi | A is increasing by A22, ORDINAL4:15;

B = sup (phi | A) by A2, A4, A33, A34, A35;

hence B is_limes_of phi | A by A34, A36, A37, ORDINAL4:8; :: thesis: verum

end;( not A in dom phi or A = 0 or not A is limit_ordinal or not b

let B be Ordinal; :: thesis: ( not A in dom phi or A = 0 or not A is limit_ordinal or not B = phi . A or B is_limes_of phi | A )

assume that

A33: A in dom phi and

A34: ( A <> 0 & A is limit_ordinal ) and

A35: B = phi . A ; :: thesis: B is_limes_of phi | A

A c= dom phi by A33, ORDINAL1:def 2;

then A36: dom (phi | A) = A by RELAT_1:62;

A37: phi | A is increasing by A22, ORDINAL4:15;

B = sup (phi | A) by A2, A4, A33, A34, A35;

hence B is_limes_of phi | A by A34, A36, A37, ORDINAL4:8; :: thesis: verum

phi . a = sup (phi | a) ) )

thus for a being Ordinal of W holds phi . (succ a) = sup ({(phi . a)} \/ ((uncurry Phi) .: [:D,{(succ a)}:])) by A3, ZF_REFLE:7; :: thesis: for a being Ordinal of W st a <> 0-element_of W & a is limit_ordinal holds

phi . a = sup (phi | a)

let a be Ordinal of W; :: thesis: ( a <> 0-element_of W & a is limit_ordinal implies phi . a = sup (phi | a) )

a in On W by ZF_REFLE:7;

hence ( a <> 0-element_of W & a is limit_ordinal implies phi . a = sup (phi | a) ) by A4; :: thesis: verum