let l be limit_ordinal non empty Ordinal; :: thesis: for U being Universe st l in U & ( for a being ordinal number st a in l holds
(U -Veblen) . a is normal Ordinal-Sequence of U ) holds
(U -Veblen) . l is normal Ordinal-Sequence of U
let U be Universe; :: thesis: ( l in U & ( for a being ordinal number st a in l holds
(U -Veblen) . a is normal Ordinal-Sequence of U ) implies (U -Veblen) . l is normal Ordinal-Sequence of U )
assume Z0: l in U ; :: thesis: ( ex a being ordinal number st
( a in l & (U -Veblen) . a is not normal Ordinal-Sequence of U ) or (U -Veblen) . l is normal Ordinal-Sequence of U )
assume Z1: for a being ordinal number st a in l holds
(U -Veblen) . a is normal Ordinal-Sequence of U ; :: thesis: (U -Veblen) . l is normal Ordinal-Sequence of U
A0: l in On U by Z0, ORDINAL1:def 9;
then A1: (U -Veblen) . l = criticals ((U -Veblen) | l) by V;
A3: dom (U -Veblen) = On U by V;
l c= On U by A0, ORDINAL1:def 2;
then A2: dom ((U -Veblen) | l) = l by A3, RELAT_1:62;
YY: dom ((U -Veblen) . l) = On U

proof

set F = U -Veblen ;
set G = (U -Veblen) . l;
H1: 0 in l by ORDINAL3:8;
reconsider f0 = (U -Veblen) . 0 as normal Ordinal-Sequence of U by Z1, ORDINAL3:8;
H2: dom f0 = On U by FUNCT_2:def 1;
H2a: f0 = ((U -Veblen) | l) . 0 by FUNCT_1:49, ORDINAL3:8;
then f0 in rng ((U -Veblen) | l) by A2, H1, FUNCT_1:def 3;
hence dom ((U -Veblen) . l) c= On U by A1, H2, ThA5; :: according to XBOOLE_0:def 10 :: thesis: On U c= dom ((U -Veblen) . l)

now

let c be ordinal number ; :: thesis: ( c in dom ((U -Veblen) | l) implies ((U -Veblen) | l) . c is Ordinal-Sequence of U )
assume C1: c in dom ((U -Veblen) | l) ; :: thesis: ((U -Veblen) | l) . c is Ordinal-Sequence of U
then ((U -Veblen) | l) . c = (U -Veblen) . c by FUNCT_1:47;
hence ((U -Veblen) | l) . c is Ordinal-Sequence of U by A2, C1, Z1; :: thesis: verum

end;

then reconsider lg = lims ((U -Veblen) | l) as Ordinal-Sequence of U by Z0, A2, ThL1;
H3: dom lg = On U by FUNCT_2:def 1;
rng lg c= rng ((U -Veblen) . l)

proof

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in rng lg or y in rng ((U -Veblen) . l) )
assume y in rng lg ; :: thesis: y in rng ((U -Veblen) . l)
then consider x being set such that
G1: ( x in dom lg & y = lg . x ) by FUNCT_1:def 3;
reconsider x = x as Ordinal by G1;
G2: ( x in U & y in On U ) by H3, G1, ORDINAL1:def 9;
set Y = { a where a is Element of dom (((U -Veblen) | l) . 0) : ( a in dom (((U -Veblen) | l) . 0) & ( for f being Ordinal-Sequence st f in rng ((U -Veblen) | l) holds
a is_a_fixpoint_of f ) ) } ;
G4: { a where a is Element of dom (((U -Veblen) | l) . 0) : ( a in dom (((U -Veblen) | l) . 0) & ( for f being Ordinal-Sequence st f in rng ((U -Veblen) | l) holds
a is_a_fixpoint_of f ) ) } is ordinal-membered by ThA1;

now

let f be Ordinal-Sequence; :: thesis: ( f in rng ((U -Veblen) | l) implies y is_a_fixpoint_of f )
assume f in rng ((U -Veblen) | l) ; :: thesis: y is_a_fixpoint_of f
then consider z being set such that
G3: ( z in l & f = ((U -Veblen) | l) . z ) by A2, FUNCT_1:def 3;
f = (U -Veblen) . z by G3, FUNCT_1:49;
hence y is_a_fixpoint_of f by Z0, Z1, G3, G1, G2, Th53; :: thesis: verum

end;

then y in { a where a is Element of dom (((U -Veblen) | l) . 0) : ( a in dom (((U -Veblen) | l) . 0) & ( for f being Ordinal-Sequence st f in rng ((U -Veblen) | l) holds
a is_a_fixpoint_of f ) ) } by H2, H2a, G2;
hence y in rng ((U -Veblen) . l) by A1, G4, ThN1a; :: thesis: verum

end;

then F1: Union lg c= Union ((U -Veblen) . l) by ZFMISC_1:77;
On U c= Union lg

proof

let a be ordinal number ; :: according to ORDINAL1:def 5 :: thesis: ( not a in On U or a in Union lg )
assume E1: a in On U ; :: thesis: a in Union lg
E2: a in succ a by ORDINAL1:6;
set X = { ((((U -Veblen) | l) . b) . (succ a)) where b is Element of dom ((U -Veblen) | l) : b in dom ((U -Veblen) | l) } ;
On U is limit_ordinal by CLASSES2:51;
then E3: succ a in On U by E1, ORDINAL1:28;
then E4: lg . (succ a) = union { ((((U -Veblen) | l) . b) . (succ a)) where b is Element of dom ((U -Veblen) | l) : b in dom ((U -Veblen) | l) } by H3, LIM;
E5: f0 . (succ a) in { ((((U -Veblen) | l) . b) . (succ a)) where b is Element of dom ((U -Veblen) | l) : b in dom ((U -Veblen) | l) } by H2a, A2, H1;
E6: f0 . a in f0 . (succ a) by E2, E3, H2, ORDINAL2:def 12;
a c= f0 . a by H2, E1, ORDINAL4:10;
then a in f0 . (succ a) by E6, ORDINAL1:12;
then a in lg . (succ a) by E4, E5, TARSKI:def 4;
hence a in Union lg by H3, E3, CARD_5:2; :: thesis: verum

end;

then F2: On U c= Union ((U -Veblen) . l) by F1, XBOOLE_1:1;
F3: rng ((U -Veblen) . l) c= U

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in rng ((U -Veblen) . l) or x in U )
assume x in rng ((U -Veblen) . l) ; :: thesis: x in U
then consider y being set such that
D1: ( y in dom ((U -Veblen) . l) & x = ((U -Veblen) . l) . y ) by FUNCT_1:def 3;
x is_a_fixpoint_of f0 by A1, A2, H1, H2a, D1, ThA2;
then ( x in dom f0 & x = f0 . x ) by ABIAN:def 3;
hence x in U ; :: thesis: verum

end;

assume On U c/= dom ((U -Veblen) . l) ; :: thesis: contradiction
then dom ((U -Veblen) . l) in On U by ORDINAL1:16;
then reconsider d = dom ((U -Veblen) . l) as Ordinal of U by ORDINAL1:def 9;
H5: card d in card U by CLASSES2:1;
card (rng ((U -Veblen) . l)) c= card d by CARD_1:12;
then card (rng ((U -Veblen) . l)) in card U by H5, ORDINAL1:12;
then reconsider r = rng ((U -Veblen) . l) as Element of U by F3, CLASSES1:1;
union r in U ;
then Union ((U -Veblen) . l) in On U by ORDINAL1:def 9;
then Union ((U -Veblen) . l) in Union ((U -Veblen) . l) by F2;
hence contradiction ; :: thesis: verum

end;

ZZ: rng ((U -Veblen) . l) c= On U

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in rng ((U -Veblen) . l) or x in On U )
assume x in rng ((U -Veblen) . l) ; :: thesis: x in On U
then consider y being set such that
C1: ( y in dom ((U -Veblen) . l) & x = ((U -Veblen) . l) . y ) by FUNCT_1:def 3;
reconsider y = y as Ordinal by C1;
C2: 0 in l by ORDINAL3:8;
then x is_a_fixpoint_of ((U -Veblen) | l) . 0 by A1, C1, A2, ThA2;
then x in dom (((U -Veblen) | l) . 0) by ABIAN:def 3;
then ( x in dom ((U -Veblen) . 0) & (U -Veblen) . 0 is Ordinal-Sequence of U ) by Z1, C2, FUNCT_1:49;
hence x in On U by FUNCT_2:def 1; :: thesis: verum

end;

now

let a be ordinal number ; :: thesis: ( a in l implies ((U -Veblen) | l) . a is normal )
assume B1: a in l ; :: thesis: ((U -Veblen) | l) . a is normal
then ((U -Veblen) | l) . a = (U -Veblen) . a by FUNCT_1:49;
hence ((U -Veblen) | l) . a is normal by Z1, B1; :: thesis: verum

end;

then (U -Veblen) . l is continuous by A1, A2, ThAA;
hence (U -Veblen) . l is normal Ordinal-Sequence of U by A1, YY, ZZ, FUNCT_2:2; :: thesis: verum