let a, b be Ordinal; for l being limit_ordinal non empty Ordinal
for U being Universe st l in U & a in U & b in l & ( for c being Ordinal st c in l holds
(U -Veblen) . c is normal Ordinal-Sequence of U ) holds
(lims ((U -Veblen) | l)) . a is_a_fixpoint_of (U -Veblen) . b
let l be limit_ordinal non empty Ordinal; for U being Universe st l in U & a in U & b in l & ( for c being Ordinal st c in l holds
(U -Veblen) . c is normal Ordinal-Sequence of U ) holds
(lims ((U -Veblen) | l)) . a is_a_fixpoint_of (U -Veblen) . b
let U be Universe; ( l in U & a in U & b in l & ( for c being Ordinal st c in l holds
(U -Veblen) . c is normal Ordinal-Sequence of U ) implies (lims ((U -Veblen) | l)) . a is_a_fixpoint_of (U -Veblen) . b )
assume that
A1:
l in U
and
A2:
a in U
and
A3:
b in l
and
A4:
for c being Ordinal st c in l holds
(U -Veblen) . c is normal Ordinal-Sequence of U
; (lims ((U -Veblen) | l)) . a is_a_fixpoint_of (U -Veblen) . b
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) } ;
A5:
0 in l
by ORDINAL3:8;
reconsider f0 = (U -Veblen) . 0, f = (U -Veblen) . b as normal Ordinal-Sequence of U by A3, A4, ORDINAL3:8;
A6:
( f0 = ((U -Veblen) | l) . 0 & f = ((U -Veblen) | l) . b )
by A3, FUNCT_1:49, ORDINAL3:8;
then A7: dom (lims ((U -Veblen) | l)) =
dom f0
by Def12
.=
On U
by FUNCT_2:def 1
;
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;
then A10:
(((U -Veblen) | l) . b) . a in { ((((U -Veblen) | l) . d) . a) where d is Element of dom ((U -Veblen) | l) : d in dom ((U -Veblen) | l) }
by A3;
then reconsider lg = lims ((U -Veblen) | l) as Ordinal-Sequence of U by A1, A9, Th56;
A12:
a in On U
by A2, ORDINAL1:def 9;
then A13:
lg . a = union { ((((U -Veblen) | l) . d) . a) where d is Element of dom ((U -Veblen) | l) : d in dom ((U -Veblen) | l) }
by A7, Def12;
A14:
( dom f = On U & dom f0 = On U )
by FUNCT_2:def 1;
A15:
for x being set st x in { ((((U -Veblen) | l) . d) . a) where d is Element of dom ((U -Veblen) | l) : d in dom ((U -Veblen) | l) } holds
ex y being set st
( x c= y & y in { ((((U -Veblen) | l) . d) . a) where d is Element of dom ((U -Veblen) | l) : d in dom ((U -Veblen) | l) } & y is_a_fixpoint_of f )
proof
let x be
set ;
( x in { ((((U -Veblen) | l) . d) . a) where d is Element of dom ((U -Veblen) | l) : d in dom ((U -Veblen) | l) } implies ex y being set st
( x c= y & y in { ((((U -Veblen) | l) . d) . a) where d is Element of dom ((U -Veblen) | l) : d in dom ((U -Veblen) | l) } & y is_a_fixpoint_of f ) )
assume A16:
x in { ((((U -Veblen) | l) . d) . a) where d is Element of dom ((U -Veblen) | l) : d in dom ((U -Veblen) | l) }
;
ex y being set st
( x c= y & y in { ((((U -Veblen) | l) . d) . a) where d is Element of dom ((U -Veblen) | l) : d in dom ((U -Veblen) | l) } & y is_a_fixpoint_of f )
then consider d being
Element of
dom ((U -Veblen) | l) such that A17:
(
x = (((U -Veblen) | l) . d) . a &
d in dom ((U -Veblen) | l) )
;
reconsider f2 =
(U -Veblen) . d as
normal Ordinal-Sequence of
U by A4, A9;
A18:
f2 = ((U -Veblen) | l) . d
by A9, FUNCT_1:49;
A19:
dom f2 = On U
by FUNCT_2:def 1;
omega c= l
by A5, ORDINAL1:def 11;
then A20:
(
d in U &
omega in U )
by A9, A1, CLASSES1:def 1, ORDINAL1:10;
A21:
b in U
by A1, A3, ORDINAL1:10;
A22:
for
c being
Ordinal st
c in b holds
(U -Veblen) . c is
normal
by A4, A3, ORDINAL1:10;
per cases
( d c= b or b in d )
by ORDINAL1:16;
suppose
d c= b
;
ex y being set st
( x c= y & y in { ((((U -Veblen) | l) . d) . a) where d is Element of dom ((U -Veblen) | l) : d in dom ((U -Veblen) | l) } & y is_a_fixpoint_of f )then A23:
x c= (((U -Veblen) | l) . b) . a
by A12, A6, A14, A17, A18, A20, A21, A22, Th60;
take y =
(((U -Veblen) | l) . (succ b)) . a;
( x c= y & y in { ((((U -Veblen) | l) . d) . a) where d is Element of dom ((U -Veblen) | l) : d in dom ((U -Veblen) | l) } & y is_a_fixpoint_of f )A24:
(
b in succ b &
succ b in l )
by A3, ORDINAL1:6, ORDINAL1:28;
then reconsider f1 =
(U -Veblen) . (succ b) as
normal Ordinal-Sequence of
U by A4;
A25:
f1 = ((U -Veblen) | l) . (succ b)
by A24, FUNCT_1:49;
succ b in U
by A24, A1, ORDINAL1:10;
then
succ b in On U
by ORDINAL1:def 9;
then A26:
(
f1 = criticals f &
dom f1 = On U )
by Def15, FUNCT_2:def 1;
then
f . a c= y
by A12, A25, Th45;
hence
x c= y
by A23, A6;
( y in { ((((U -Veblen) | l) . d) . a) where d is Element of dom ((U -Veblen) | l) : d in dom ((U -Veblen) | l) } & y is_a_fixpoint_of f )thus
y in { ((((U -Veblen) | l) . d) . a) where d is Element of dom ((U -Veblen) | l) : d in dom ((U -Veblen) | l) }
by A9, A24;
y is_a_fixpoint_of fthus
y is_a_fixpoint_of f
by A12, A25, A26, Th29;
verum end;
end;
thus
(lims ((U -Veblen) | l)) . a in dom ((U -Veblen) . b)
by A13, A14, ORDINAL1:def 9; ABIAN:def 3 (lims ((U -Veblen) | l)) . a = ((U -Veblen) . b) . ((lims ((U -Veblen) | l)) . a)
hence
(lims ((U -Veblen) | l)) . a = ((U -Veblen) . b) . ((lims ((U -Veblen) | l)) . a)
by A13, A10, A15, Th36; verum