let a, b, c be Ordinal; :: thesis: for U being Universe st a in b & b in U & omega in U & c in dom ((U -Veblen) . b) holds
((U -Veblen) . b) . c is_a_fixpoint_of (U -Veblen) . a
let U be Universe; :: thesis: ( a in b & b in U & omega in U & c in dom ((U -Veblen) . b) implies ((U -Veblen) . b) . c is_a_fixpoint_of (U -Veblen) . a )
assume A1: ( a in b & b in U & omega in U ) ; :: thesis: ( not c in dom ((U -Veblen) . b) or ((U -Veblen) . b) . c is_a_fixpoint_of (U -Veblen) . a )
set F = U -Veblen ;
defpred S₁[ Ordinal] means ( $1 in U implies for a, c being Ordinal st a in $1 & c in dom ((U -Veblen) . $1) holds
((U -Veblen) . $1) . c is_a_fixpoint_of (U -Veblen) . a );
A2: S₁[ 0 ] ;
A3: for b being Ordinal st S₁[b] holds
S₁[ succ b]

proof

let b be Ordinal; :: thesis: ( S₁[b] implies S₁[ succ b] )
assume that
A4: S₁[b] and
A5: succ b in U ; :: thesis: for a, c being Ordinal st a in succ b & c in dom ((U -Veblen) . (succ b)) holds
((U -Veblen) . (succ b)) . c is_a_fixpoint_of (U -Veblen) . a
A6: b in succ b by ORDINAL1:6;
let a, c be Ordinal; :: thesis: ( a in succ b & c in dom ((U -Veblen) . (succ b)) implies ((U -Veblen) . (succ b)) . c is_a_fixpoint_of (U -Veblen) . a )
assume a in succ b ; :: thesis: ( not c in dom ((U -Veblen) . (succ b)) or ((U -Veblen) . (succ b)) . c is_a_fixpoint_of (U -Veblen) . a )
then A7: ( a in b or a in {b} ) by XBOOLE_0:def 3;
succ b in On U by A5, ORDINAL1:def 9;
then A8: (U -Veblen) . (succ b) = criticals ((U -Veblen) . b) by Def15;
assume c in dom ((U -Veblen) . (succ b)) ; :: thesis: ((U -Veblen) . (succ b)) . c is_a_fixpoint_of (U -Veblen) . a
then ((U -Veblen) . (succ b)) . c is_a_fixpoint_of (U -Veblen) . b by A8, Th29;
then ( ((U -Veblen) . (succ b)) . c in dom ((U -Veblen) . b) & ((U -Veblen) . (succ b)) . c = ((U -Veblen) . b) . (((U -Veblen) . (succ b)) . c) ) ;
hence ((U -Veblen) . (succ b)) . c is_a_fixpoint_of (U -Veblen) . a by A4, A5, A6, A7, ORDINAL1:10, TARSKI:def 1; :: thesis: verum

end;

A9: dom (U -Veblen) = On U by Def15;
A10: for b being Ordinal st b <> 0 & b is limit_ordinal & ( for d being Ordinal st d in b holds
S₁[d] ) holds
S₁[b]

proof

let b be Ordinal; :: thesis: ( b <> 0 & b is limit_ordinal & ( for d being Ordinal st d in b holds
S₁[d] ) implies S₁[b] )
assume that
A11: ( b <> 0 & b is limit_ordinal ) and
for d being Ordinal st d in b holds
S₁[d] and
A12: b in U ; :: thesis: for a, c being Ordinal st a in b & c in dom ((U -Veblen) . b) holds
((U -Veblen) . b) . c is_a_fixpoint_of (U -Veblen) . a
A13: b in On U by A12, ORDINAL1:def 9;
then A14: (U -Veblen) . b = criticals ((U -Veblen) | b) by A11, Def15;
b c= On U by A13, ORDINAL1:def 2;
then A15: dom ((U -Veblen) | b) = b by A9, RELAT_1:62;
let a, c be Ordinal; :: thesis: ( a in b & c in dom ((U -Veblen) . b) implies ((U -Veblen) . b) . c is_a_fixpoint_of (U -Veblen) . a )
assume A16: a in b ; :: thesis: ( not c in dom ((U -Veblen) . b) or ((U -Veblen) . b) . c is_a_fixpoint_of (U -Veblen) . a )
then A17: (U -Veblen) . a = ((U -Veblen) | b) . a by FUNCT_1:49;
set g = (U -Veblen) | b;
set X = { z where z is Element of dom (((U -Veblen) | b) . 0) : ( z in dom (((U -Veblen) | b) . 0) & ( for f being Ordinal-Sequence st f in rng ((U -Veblen) | b) holds
z is_a_fixpoint_of f ) ) } ;

now :: thesis: for x being set st x in { z where z is Element of dom (((U -Veblen) | b) . 0) : ( z in dom (((U -Veblen) | b) . 0) & ( for f being Ordinal-Sequence st f in rng ((U -Veblen) | b) holds
z is_a_fixpoint_of f ) ) } holds
x is ordinal

let x be set ; :: thesis: ( x in { z where z is Element of dom (((U -Veblen) | b) . 0) : ( z in dom (((U -Veblen) | b) . 0) & ( for f being Ordinal-Sequence st f in rng ((U -Veblen) | b) holds
z is_a_fixpoint_of f ) ) } implies x is ordinal )
assume x in { z where z is Element of dom (((U -Veblen) | b) . 0) : ( z in dom (((U -Veblen) | b) . 0) & ( for f being Ordinal-Sequence st f in rng ((U -Veblen) | b) holds
z is_a_fixpoint_of f ) ) } ; :: thesis: x is ordinal
then ex a being Element of dom (((U -Veblen) | b) . 0) st
( x = a & a in dom (((U -Veblen) | b) . 0) & ( for f being Ordinal-Sequence st f in rng ((U -Veblen) | b) holds
a is_a_fixpoint_of f ) ) ;
hence x is ordinal ; :: thesis: verum

end;

then reconsider X = { z where z is Element of dom (((U -Veblen) | b) . 0) : ( z in dom (((U -Veblen) | b) . 0) & ( for f being Ordinal-Sequence st f in rng ((U -Veblen) | b) holds
z is_a_fixpoint_of f ) ) } as ordinal-membered set by Th1;
assume c in dom ((U -Veblen) . b) ; :: thesis: ((U -Veblen) . b) . c is_a_fixpoint_of (U -Veblen) . a
then ((U -Veblen) . b) . c in rng ((U -Veblen) . b) by FUNCT_1:def 3;
then ((U -Veblen) . b) . c in X by A14, Th19;
then consider z being Element of dom (((U -Veblen) | b) . 0) such that
A18: ( ((U -Veblen) . b) . c = z & z in dom (((U -Veblen) | b) . 0) & ( for f being Ordinal-Sequence st f in rng ((U -Veblen) | b) holds
z is_a_fixpoint_of f ) ) ;
(U -Veblen) . a in rng ((U -Veblen) | b) by A15, A17, A16, FUNCT_1:def 3;
hence ((U -Veblen) . b) . c is_a_fixpoint_of (U -Veblen) . a by A18; :: thesis: verum

end;

for b being Ordinal holds S₁[b] from ORDINAL2:sch 1(A2, A3, A10);
hence ( not c in dom ((U -Veblen) . b) or ((U -Veblen) . b) . c is_a_fixpoint_of (U -Veblen) . a ) by A1; :: thesis: verum