let a be Ordinal; :: thesis: for l being limit_ordinal non empty Ordinal
for U being Universe st l in U & ( for c being Ordinal st c in l holds
a is_a_fixpoint_of (U -Veblen) . c ) holds
a is_a_fixpoint_of lims ((U -Veblen) | l)
let l be limit_ordinal non empty Ordinal; :: thesis: for U being Universe st l in U & ( for c being Ordinal st c in l holds
a is_a_fixpoint_of (U -Veblen) . c ) holds
a is_a_fixpoint_of lims ((U -Veblen) | l)
let U be Universe; :: thesis: ( l in U & ( for c being Ordinal st c in l holds
a is_a_fixpoint_of (U -Veblen) . c ) implies a is_a_fixpoint_of lims ((U -Veblen) | l) )
assume A1: l in U ; :: thesis: ( ex c being Ordinal st
( c in l & not a is_a_fixpoint_of (U -Veblen) . c ) or a is_a_fixpoint_of lims ((U -Veblen) | l) )
assume A2: for c being Ordinal st c in l holds
a is_a_fixpoint_of (U -Veblen) . c ; :: thesis: a is_a_fixpoint_of lims ((U -Veblen) | l)
set F = U -Veblen ;
set g = (U -Veblen) | l;
set X = { ((((U -Veblen) | l) . d) . a) where d is Element of dom ((U -Veblen) | l) : d in dom ((U -Veblen) | l) } ;
set u = union { ((((U -Veblen) | l) . d) . a) where d is Element of dom ((U -Veblen) | l) : d in dom ((U -Veblen) | l) } ;
A3: 0 in l by ORDINAL3:8;
then omega c= l by ORDINAL1:def 11;
then reconsider o = omega as non trivial Ordinal of U by A1, CLASSES1:def 1;
(U -Veblen) . 0 = U exp o by Def15;
then reconsider f0 = (U -Veblen) . 0 as normal Ordinal-Sequence of U ;
A4: f0 = ((U -Veblen) | l) . 0 by FUNCT_1:49, ORDINAL3:8;
then A5: ( dom (lims ((U -Veblen) | l)) = dom f0 & dom f0 = On U ) by Def12, FUNCT_2:def 1;
A6: a is_a_fixpoint_of f0 by A2, ORDINAL3:8;
then A7: ( a in On U & a = f0 . a ) by A5;
A8: dom (U -Veblen) = On U by Def15;
l in On U by A1, ORDINAL1:def 9;
then l c= dom (U -Veblen) by A8, ORDINAL1:def 2;
then A9: dom ((U -Veblen) | l) = l by RELAT_1:62;
set lg = lims ((U -Veblen) | l);
thus a in dom (lims ((U -Veblen) | l)) by A5, A6; :: according to ABIAN:def 3 :: thesis: a = (lims ((U -Veblen) | l)) . a
A10: (lims ((U -Veblen) | l)) . a = union { ((((U -Veblen) | l) . d) . a) where d is Element of dom ((U -Veblen) | l) : d in dom ((U -Veblen) | l) } by A5, A7, Def12;
{a} = { ((((U -Veblen) | l) . d) . a) where d is Element of dom ((U -Veblen) | l) : d in dom ((U -Veblen) | l) }
proof
a in { ((((U -Veblen) | l) . d) . a) where d is Element of dom ((U -Veblen) | l) : d in dom ((U -Veblen) | l) } by A3, A9, A7, A4;
hence {a} c= { ((((U -Veblen) | l) . d) . a) where d is Element of dom ((U -Veblen) | l) : d in dom ((U -Veblen) | l) } by ZFMISC_1:31; :: according to XBOOLE_0:def 10 :: thesis: { ((((U -Veblen) | l) . d) . a) where d is Element of dom ((U -Veblen) | l) : d in dom ((U -Veblen) | l) } c= {a}
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { ((((U -Veblen) | l) . d) . a) where d is Element of dom ((U -Veblen) | l) : d in dom ((U -Veblen) | l) } or x in {a} )
assume x in { ((((U -Veblen) | l) . d) . a) where d is Element of dom ((U -Veblen) | l) : d in dom ((U -Veblen) | l) } ; :: thesis: x in {a}
then consider d being Element of dom ((U -Veblen) | l) such that
A11: ( x = (((U -Veblen) | l) . d) . a & d in dom ((U -Veblen) | l) ) ;
((U -Veblen) | l) . d = (U -Veblen) . d by A11, FUNCT_1:47;
then a is_a_fixpoint_of ((U -Veblen) | l) . d by A2, A9;
then x = a by A11;
hence x in {a} by TARSKI:def 1; :: thesis: verum
end;
hence a = (lims ((U -Veblen) | l)) . a by A10, ZFMISC_1:25; :: thesis: verum