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 Z0: ( 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 );
00: S₁[ 0 ] ;
01: 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
Z1: S₁[b] and
Z2: 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
A0: 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 A1: ( a in b or a in {b} ) by XBOOLE_0:def 3;
succ b in On U by Z2, ORDINAL1:def 9;
then A2: (U -Veblen) . (succ b) = criticals ((U -Veblen) . b) by V;
assume c in dom ((U -Veblen) . (succ b)) ; :: thesis: ((U -Veblen) . (succ b)) . c is_a_fixpoint_of (U -Veblen) . a
then A3: ((U -Veblen) . (succ b)) . c is_a_fixpoint_of (U -Veblen) . b by A2, Th02;
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 Z1, Z2, A0, A1, A3, ORDINAL1:10, TARSKI:def 1; :: thesis: verum

end;

F1: dom (U -Veblen) = On U by V;
02: 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
Z1: ( b <> {} & b is limit_ordinal ) and
for d being ordinal number st d in b holds
S₁[d] and
Z3: 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
B2: b in On U by Z3, ORDINAL1:def 9;
then B0: (U -Veblen) . b = criticals ((U -Veblen) | b) by Z1, V;
b c= On U by B2, ORDINAL1:def 2;
then B3: dom ((U -Veblen) | b) = b by F1, 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 Z4: a in b ; :: thesis: ( not c in dom ((U -Veblen) . b) or ((U -Veblen) . b) . c is_a_fixpoint_of (U -Veblen) . a )
then B1: (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

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 EXCH9;
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 B0, ThN1a;
then consider z being Element of dom (((U -Veblen) | b) . 0) such that
B4: ( ((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 B3, B1, Z4, FUNCT_1:def 3;
hence ((U -Veblen) . b) . c is_a_fixpoint_of (U -Veblen) . a by B4; :: thesis: verum

end;

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