let a be ordinal number ; :: thesis: for l being limit_ordinal non empty Ordinal
for U being Universe st l in U & ( for c being ordinal number 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 number 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 number st c in l holds
a is_a_fixpoint_of (U -Veblen) . c ) implies a is_a_fixpoint_of lims ((U -Veblen) | l) )
assume Z0: l in U ; :: thesis: ( ex c being ordinal number st
( c in l & not a is_a_fixpoint_of (U -Veblen) . c ) or a is_a_fixpoint_of lims ((U -Veblen) | l) )
assume Z1: for c being ordinal number 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) } ;
A0: 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 Z0, CLASSES1:def 1;
(U -Veblen) . 0 = U exp o by V;
then reconsider f0 = (U -Veblen) . 0 as normal Ordinal-Sequence of U ;
A2: f0 = ((U -Veblen) | l) . 0 by FUNCT_1:49, ORDINAL3:8;
then A1: ( dom (lims ((U -Veblen) | l)) = dom f0 & dom f0 = On U ) by LIM, FUNCT_2:def 1;
B3: a is_a_fixpoint_of f0 by Z1, ORDINAL3:8;
then A3: ( a in On U & a = f0 . a ) by A1, ABIAN:def 3;
A5: dom (U -Veblen) = On U by V;
l in On U by Z0, ORDINAL1:def 9;
then l c= dom (U -Veblen) by A5, ORDINAL1:def 2;
then A6: dom ((U -Veblen) | l) = l by RELAT_1:62;
set lg = lims ((U -Veblen) | l);
thus a in dom (lims ((U -Veblen) | l)) by A1, B3, ABIAN:def 3; :: according to ABIAN:def 3 :: thesis: a = (lims ((U -Veblen) | l)) . a
A4: (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 A1, A3, LIM;
{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 A0, A6, A3, A2;
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 set ; :: 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
A7: ( x = (((U -Veblen) | l) . d) . a & d in dom ((U -Veblen) | l) ) ;
((U -Veblen) | l) . d = (U -Veblen) . d by A7, FUNCT_1:47;
then a is_a_fixpoint_of ((U -Veblen) | l) . d by Z1, A6;
then x = a by A7, ABIAN:def 3;
hence x in {a} by TARSKI:def 1; :: thesis: verum

end;

hence a = (lims ((U -Veblen) | l)) . a by A4, ZFMISC_1:25; :: thesis: verum