let a, b, c be ordinal number ; :: 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 number 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 number st S₁[b] holds
S₁[ succ b]

proof

let b be ordinal number ; :: thesis: ( S₁[b] implies S₁[ succ b] )
assume that
A4: S₁[b] and
A5: succ b in U ; :: thesis: for a, c being ordinal number 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 number ; :: 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 A9: ((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) ) by ABIAN:def 3;
hence ((U -Veblen) . (succ b)) . c is_a_fixpoint_of (U -Veblen) . a by A4, A5, A6, A7, A9, ORDINAL1:10, TARSKI:def 1; :: thesis: verum

end;

A10: dom (U -Veblen) = On U by Def15;
A11: for b being ordinal number st b <> {} & b is limit_ordinal & ( for d being ordinal number st d in b holds
S₁[d] ) holds
S₁[b]

proof

let b be ordinal number ; :: thesis: ( b <> {} & b is limit_ordinal & ( for d being ordinal number st d in b holds
S₁[d] ) implies S₁[b] )
assume that
A12: ( b <> {} & b is limit_ordinal ) and
for d being ordinal number st d in b holds
S₁[d] and
A13: b in U ; :: thesis: for a, c being ordinal number st a in b & c in dom ((U -Veblen) . b) holds
((U -Veblen) . b) . c is_a_fixpoint_of (U -Veblen) . a
A14: b in On U by A13, ORDINAL1:def 9;
then A15: (U -Veblen) . b = criticals ((U -Veblen) | b) by A12, Def15;
b c= On U by A14, ORDINAL1:def 2;
then A16: dom ((U -Veblen) | b) = b by A10, RELAT_1:62;
let a, c be ordinal number ; :: thesis: ( a in b & c in dom ((U -Veblen) . b) implies ((U -Veblen) . b) . c is_a_fixpoint_of (U -Veblen) . a )
assume A17: a in b ; :: thesis: ( not c in dom ((U -Veblen) . b) or ((U -Veblen) . b) . c is_a_fixpoint_of (U -Veblen) . a )
then A18: (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 A15, Th19;
then consider z being Element of dom (((U -Veblen) | b) . 0) such that
A19: ( ((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 A16, A18, A17, FUNCT_1:def 3;
hence ((U -Veblen) . b) . c is_a_fixpoint_of (U -Veblen) . a by A19; :: thesis: verum

end;

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