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
(U -Veblen) . l is normal 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 (U -Veblen) . l is normal Ordinal-Sequence of U )
assume A1: l in U ; :: thesis: ( ex a being Ordinal 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 A2: for a being Ordinal st a in l holds
(U -Veblen) . a is normal Ordinal-Sequence of U ; :: thesis: (U -Veblen) . l is normal Ordinal-Sequence of U
A3: l in On U by A1, ORDINAL1:def 9;
then A4: (U -Veblen) . l = criticals ((U -Veblen) | l) by Def15;
A5: dom (U -Veblen) = On U by Def15;
l c= On U by A3, ORDINAL1:def 2;
then A6: dom ((U -Veblen) | l) = l by A5, RELAT_1:62;
A7: dom ((U -Veblen) . l) = On U
proof
set F = U -Veblen ;
set G = (U -Veblen) . l;
A8: 0 in l by ORDINAL3:8;
reconsider f0 = (U -Veblen) . 0 as normal Ordinal-Sequence of U by A2, ORDINAL3:8;
A9: dom f0 = On U by FUNCT_2:def 1;
A10: f0 = ((U -Veblen) | l) . 0 by FUNCT_1:49, ORDINAL3:8;
then f0 in rng ((U -Veblen) | l) by A6, A8, FUNCT_1:def 3;
hence dom ((U -Veblen) . l) c= On U by A4, A9, Th49; :: according to XBOOLE_0:def 10 :: thesis: On U c= dom ((U -Veblen) . l)
now :: thesis: for c being Ordinal st c in dom ((U -Veblen) | l) holds
((U -Veblen) | l) . c is Ordinal-Sequence of U
let c be Ordinal; :: thesis: ( c in dom ((U -Veblen) | l) implies ((U -Veblen) | l) . c is Ordinal-Sequence of U )
assume A11: 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 A6, A11, A2; :: thesis: verum
end;
then reconsider lg = lims ((U -Veblen) | l) as Ordinal-Sequence of U by A1, A6, Th56;
A12: dom lg = On U by FUNCT_2:def 1;
rng lg c= rng ((U -Veblen) . l)
proof
let y be object ; :: 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 object such that
A13: ( x in dom lg & y = lg . x ) by FUNCT_1:def 3;
reconsider x = x as Ordinal by A13;
y = lg . x by A13;
then A14: ( x in U & y in On U ) by A12, A13, 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 ) ) } ;
A15: { 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 Th46;
now :: thesis: for f being Ordinal-Sequence st f in rng ((U -Veblen) | l) holds
y is_a_fixpoint_of f
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 object such that
A16: ( z in l & f = ((U -Veblen) | l) . z ) by A6, FUNCT_1:def 3;
f = (U -Veblen) . z by A16, FUNCT_1:49;
hence y is_a_fixpoint_of f by A1, A2, A16, A13, A14, Th61; :: 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 A9, A10, A14;
hence y in rng ((U -Veblen) . l) by A4, A15, Th19; :: thesis: verum
end;
then A17: Union lg c= Union ((U -Veblen) . l) by ZFMISC_1:77;
On U c= Union lg
proof
let a be Ordinal; :: according to ORDINAL1:def 5 :: thesis: ( not a in On U or a in Union lg )
assume A18: a in On U ; :: thesis: a in Union lg
A19: 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 A20: succ a in On U by A18, ORDINAL1:28;
then A21: 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 A12, Def12;
A22: 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 A10, A6, A8;
A23: f0 . a in f0 . (succ a) by A19, A20, A9, ORDINAL2:def 12;
a c= f0 . a by A9, A18, ORDINAL4:10;
then a in f0 . (succ a) by A23, ORDINAL1:12;
then a in lg . (succ a) by A21, A22, TARSKI:def 4;
hence a in Union lg by A12, A20, CARD_5:2; :: thesis: verum
end;
then A24: On U c= Union ((U -Veblen) . l) by A17;
A25: rng ((U -Veblen) . l) c= U
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in rng ((U -Veblen) . l) or x in U )
reconsider xx = x as set by TARSKI:1;
assume x in rng ((U -Veblen) . l) ; :: thesis: x in U
then consider y being object such that
A26: ( y in dom ((U -Veblen) . l) & x = ((U -Veblen) . l) . y ) by FUNCT_1:def 3;
x is_a_fixpoint_of f0 by A4, A6, A8, A10, A26, Th47;
then ( xx in dom f0 & xx = f0 . xx ) ;
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;
A27: 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 A27, ORDINAL1:12;
then reconsider r = rng ((U -Veblen) . l) as Element of U by A25, 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 A24;
hence contradiction ; :: thesis: verum
end;
A28: rng ((U -Veblen) . l) c= On U
proof
let x be object ; :: 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 object such that
A29: ( y in dom ((U -Veblen) . l) & x = ((U -Veblen) . l) . y ) by FUNCT_1:def 3;
reconsider y = y as Ordinal by A29;
A30: 0 in l by ORDINAL3:8;
then x is_a_fixpoint_of ((U -Veblen) | l) . 0 by A4, A29, A6, Th47;
then x in dom (((U -Veblen) | l) . 0) ;
then ( x in dom ((U -Veblen) . 0) & (U -Veblen) . 0 is Ordinal-Sequence of U ) by A2, A30, FUNCT_1:49;
hence x in On U by FUNCT_2:def 1; :: thesis: verum
end;
now :: thesis: for a being Ordinal st a in l holds
((U -Veblen) | l) . a is normal
let a be Ordinal; :: thesis: ( a in l implies ((U -Veblen) | l) . a is normal )
assume A31: 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 A2, A31; :: thesis: verum
end;
then (U -Veblen) . l is continuous by A4, A6, Th53;
hence (U -Veblen) . l is normal Ordinal-Sequence of U by A4, A7, A28, FUNCT_2:2; :: thesis: verum