let l be limit_ordinal non empty Ordinal; :: thesis: for U being Universe st l in U & ( for a being Ordinal st a in l holds
(U -Veblen) . a is normal Ordinal-Sequence of U ) holds
lims ((U -Veblen) | l) is continuous non-decreasing Ordinal-Sequence of U
let U be Universe; :: thesis: ( l in U & ( for a being Ordinal st a in l holds
(U -Veblen) . a is normal Ordinal-Sequence of U ) implies lims ((U -Veblen) | l) is continuous non-decreasing Ordinal-Sequence of U )
set G = U -Veblen ;
assume that
A1: l in U and
A2: for a being Ordinal st a in l holds
(U -Veblen) . a is normal Ordinal-Sequence of U ; :: thesis: lims ((U -Veblen) | l) is continuous non-decreasing Ordinal-Sequence of U
0 in l by ORDINAL3:8;
then omega c= l by ORDINAL1:def 11;
then A3: ( omega in U & l in On U ) by A1, CLASSES1:def 1, ORDINAL1:def 9;
then A4: ( (U -Veblen) . l = criticals ((U -Veblen) | l) & dom (U -Veblen) = On U ) by Def15;
l c= On U by A3, ORDINAL1:def 2;
then A5: dom ((U -Veblen) | l) = l by A4, RELAT_1:62;
set g = (U -Veblen) | l;

now :: thesis: for a being Ordinal st a in dom ((U -Veblen) | l) holds
((U -Veblen) | l) . a is Ordinal-Sequence of U

let a be Ordinal; :: thesis: ( a in dom ((U -Veblen) | l) implies ((U -Veblen) | l) . a is Ordinal-Sequence of U )
assume A6: a in dom ((U -Veblen) | l) ; :: thesis: ((U -Veblen) | l) . a is Ordinal-Sequence of U
then ((U -Veblen) | l) . a = (U -Veblen) . a by A5, FUNCT_1:49;
hence ((U -Veblen) | l) . a is Ordinal-Sequence of U by A2, A5, A6; :: thesis: verum

end;

then reconsider f = lims ((U -Veblen) | l) as Ordinal-Sequence of U by A1, A5, Th56;
((U -Veblen) | l) . 0 = (U -Veblen) . 0 by FUNCT_1:49, ORDINAL3:8;
then reconsider g0 = ((U -Veblen) | l) . 0 as Ordinal-Sequence of U by A2, ORDINAL3:8;
A7: dom f = On U by FUNCT_2:def 1;
deffunc H₁( object ) -> set = { ((((U -Veblen) | l) . b) . $1) where b is Element of dom ((U -Veblen) | l) : b in dom ((U -Veblen) | l) } ;
A8: f is non-decreasing

proof

let a be Ordinal; :: according to ORDINAL5:def 2 :: thesis: for b₁ being set holds
( not a in b₁ or not b₁ in dom f or f . a c= f . b₁ )
let b be Ordinal; :: thesis: ( not a in b or not b in dom f or f . a c= f . b )
assume A9: ( a in b & b in dom f ) ; :: thesis: f . a c= f . b
then a in dom f by ORDINAL1:10;
then A10: ( f . a = union H₁(a) & f . b = union H₁(b) ) by A9, Def12;
let c be Ordinal; :: according to ORDINAL1:def 5 :: thesis: ( not c in f . a or c in f . b )
assume c in f . a ; :: thesis: c in f . b
then consider x being set such that
A11: ( c in x & x in H₁(a) ) by A10, TARSKI:def 4;
consider xa being Element of dom ((U -Veblen) | l) such that
A12: ( x = (((U -Veblen) | l) . xa) . a & xa in dom ((U -Veblen) | l) ) by A11;
((U -Veblen) | l) . xa = (U -Veblen) . xa by A5, FUNCT_1:49;
then reconsider h = ((U -Veblen) | l) . xa as increasing Ordinal-Sequence of U by A2, A5;
dom h = On U by FUNCT_2:def 1;
then h . a in h . b by A7, A9, ORDINAL2:def 12;
then h . a c= h . b by ORDINAL1:def 2;
then ( c in h . b & h . b in H₁(b) ) by A11, A12;
hence c in f . b by A10, TARSKI:def 4; :: thesis: verum

end;

f is continuous

proof

let a be Ordinal; :: according to ORDINAL2:def 13 :: thesis: for b₁ being set holds
( not a in dom f or a = 0 or not a is limit_ordinal or not b₁ = f . a or b₁ is_limes_of f | a )
let b be Ordinal; :: thesis: ( not a in dom f or a = 0 or not a is limit_ordinal or not b = f . a or b is_limes_of f | a )
assume A13: ( a in dom f & a <> 0 & a is limit_ordinal & b = f . a ) ; :: thesis: b is_limes_of f | a
then A14: b = union H₁(a) by Def12;
A15: a c= dom f by A13, ORDINAL1:def 2;
then A16: dom (f | a) = a by RELAT_1:62;
A17: b = Union (f | a)

proof

thus b c= Union (f | a) :: according to XBOOLE_0:def 10 :: thesis: Union (f | a) c= b

proof

let c be Ordinal; :: according to ORDINAL1:def 5 :: thesis: ( not c in b or c in Union (f | a) )
assume c in b ; :: thesis: c in Union (f | a)
then consider x being set such that
A18: ( c in x & x in H₁(a) ) by A14, TARSKI:def 4;
consider xa being Element of dom ((U -Veblen) | l) such that
A19: ( x = (((U -Veblen) | l) . xa) . a & xa in dom ((U -Veblen) | l) ) by A18;
((U -Veblen) | l) . xa = (U -Veblen) . xa by A5, FUNCT_1:49;
then reconsider h = ((U -Veblen) | l) . xa as normal Ordinal-Sequence of U by A2, A5;
A20: dom h = On U by FUNCT_2:def 1;
then A21: h . a is_limes_of h | a by A7, A13, ORDINAL2:def 13;
A22: h | a is increasing by ORDINAL4:15;
A23: dom (h | a) = a by A7, A15, A20, RELAT_1:62;
then Union (h | a) is_limes_of h | a by A13, A22, ORDINAL5:6;
then lim (h | a) = Union (h | a) by ORDINAL2:def 10;
then h . a = Union (h | a) by A21, ORDINAL2:def 10;
then consider y being object such that
A24: ( y in a & c in (h | a) . y ) by A18, A19, A23, CARD_5:2;
A25: y in On U by A7, A13, A24, ORDINAL1:10;
(h | a) . y = h . y by A24, FUNCT_1:49;
then (h | a) . y in H₁(y) by A19;
then c in union H₁(y) by A24, TARSKI:def 4;
then c in f . y by A7, A25, Def12;
then c in (f | a) . y by A24, FUNCT_1:49;
hence c in Union (f | a) by A16, A24, CARD_5:2; :: thesis: verum

end;

let c be Ordinal; :: according to ORDINAL1:def 5 :: thesis: ( not c in Union (f | a) or c in b )
assume c in Union (f | a) ; :: thesis: c in b
then consider x being object such that
A26: ( x in dom (f | a) & c in (f | a) . x ) by CARD_5:2;
A27: (f | a) . x = f . x by A16, A26, FUNCT_1:49;
x in dom f by A26, RELAT_1:57;
then f . x = union H₁(x) by Def12;
then consider y being set such that
A28: ( c in y & y in H₁(x) ) by A26, A27, TARSKI:def 4;
consider z being Element of dom ((U -Veblen) | l) such that
A29: ( y = (((U -Veblen) | l) . z) . x & z in dom ((U -Veblen) | l) ) by A28;
((U -Veblen) | l) . z = (U -Veblen) . z by A5, FUNCT_1:49;
then reconsider h = ((U -Veblen) | l) . z as normal Ordinal-Sequence of U by A2, A5;
dom h = On U by FUNCT_2:def 1;
then h . x in h . a by A26, A16, A13, A7, ORDINAL2:def 12;
then h . x c= h . a by ORDINAL1:def 2;
then ( c in h . a & h . a in H₁(a) ) by A28, A29;
hence c in b by A14, TARSKI:def 4; :: thesis: verum

end;

f | a is non-decreasing by A8, Th13;
hence b is_limes_of f | a by A13, A16, A17, ORDINAL5:6; :: thesis: verum

end;

hence lims ((U -Veblen) | l) is continuous non-decreasing Ordinal-Sequence of U by A8; :: thesis: verum