let a, b, c be Ordinal; :: thesis: for U being Universe st a c= b & b in U & omega in U & c in dom ((U -Veblen) . b) & ( for c being Ordinal st c in b holds
(U -Veblen) . c is normal ) holds
((U -Veblen) . a) . c c= ((U -Veblen) . b) . c
let U be Universe; :: thesis: ( a c= b & b in U & omega in U & c in dom ((U -Veblen) . b) & ( for c being Ordinal st c in b holds
(U -Veblen) . c is normal ) implies ((U -Veblen) . a) . c c= ((U -Veblen) . b) . c )
assume A1: ( a c= b & b in U & omega in U & c in dom ((U -Veblen) . b) ) ; :: thesis: ( ex c being Ordinal st
( c in b & not (U -Veblen) . c is normal ) or ((U -Veblen) . a) . c c= ((U -Veblen) . b) . c )
set F = U -Veblen ;
defpred S₁[ Ordinal] means for a, c being Ordinal st a c= $1 & $1 in U & c in dom ((U -Veblen) . $1) & ( for c being Ordinal st c in $1 holds
(U -Veblen) . c is normal ) holds
((U -Veblen) . a) . c c= ((U -Veblen) . $1) . c;
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 A4: S₁[b] ; :: thesis: S₁[ succ b]
let a, c be Ordinal; :: thesis: ( a c= succ b & succ b in U & c in dom ((U -Veblen) . (succ b)) & ( for c being Ordinal st c in succ b holds
(U -Veblen) . c is normal ) implies ((U -Veblen) . a) . c c= ((U -Veblen) . (succ b)) . c )
assume that
A5: a c= succ b and
A6: succ b in U and
A7: c in dom ((U -Veblen) . (succ b)) ; :: thesis: ( ex c being Ordinal st
( c in succ b & not (U -Veblen) . c is normal ) or ((U -Veblen) . a) . c c= ((U -Veblen) . (succ b)) . c )
assume A8: for c being Ordinal st c in succ b holds
(U -Veblen) . c is normal ; :: thesis: ((U -Veblen) . a) . c c= ((U -Veblen) . (succ b)) . c
succ b in On U by A6, ORDINAL1:def 9;
then A9: (U -Veblen) . (succ b) = criticals ((U -Veblen) . b) by Def15;
then A10: dom ((U -Veblen) . (succ b)) c= dom ((U -Veblen) . b) by Th32;
A11: b in succ b by ORDINAL1:6;
then A12: b in U by A6, ORDINAL1:10;
(U -Veblen) . b is normal by A8, ORDINAL1:6;
then A13: ((U -Veblen) . b) . c c= ((U -Veblen) . (succ b)) . c by A7, A9, Th45;
A14: for c being Ordinal st c in b holds
(U -Veblen) . c is normal by A8, A11, ORDINAL1:10;

per cases ( a = succ b or a c= b ) by A5, ORDINAL5:1;

suppose a = succ b ; :: thesis: ((U -Veblen) . a) . c c= ((U -Veblen) . (succ b)) . c

hence ((U -Veblen) . a) . c c= ((U -Veblen) . (succ b)) . c ; :: thesis: verum

end;

suppose a c= b ; :: thesis: ((U -Veblen) . a) . c c= ((U -Veblen) . (succ b)) . c

then ((U -Veblen) . a) . c c= ((U -Veblen) . b) . c by A4, A7, A10, A12, A14;
hence ((U -Veblen) . a) . c c= ((U -Veblen) . (succ b)) . c by A13; :: thesis: verum

end;

end;

end;

A15: 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 A16: ( b <> 0 & b is limit_ordinal ) ; :: thesis: ( ex d being Ordinal st
( d in b & not S₁[d] ) or S₁[b] )
assume for d being Ordinal st d in b holds
S₁[d] ; :: thesis: S₁[b]
let a, c be Ordinal; :: thesis: ( a c= b & b in U & c in dom ((U -Veblen) . b) & ( for c being Ordinal st c in b holds
(U -Veblen) . c is normal ) implies ((U -Veblen) . a) . c c= ((U -Veblen) . b) . c )
assume A17: a c= b ; :: thesis: ( not b in U or not c in dom ((U -Veblen) . b) or ex c being Ordinal st
( c in b & not (U -Veblen) . c is normal ) or ((U -Veblen) . a) . c c= ((U -Veblen) . b) . c )

per cases ( a = b or a c< b ) by A17;

suppose a = b ; :: thesis: ( not b in U or not c in dom ((U -Veblen) . b) or ex c being Ordinal st
( c in b & not (U -Veblen) . c is normal ) or ((U -Veblen) . a) . c c= ((U -Veblen) . b) . c )

hence ( not b in U or not c in dom ((U -Veblen) . b) or ex c being Ordinal st
( c in b & not (U -Veblen) . c is normal ) or ((U -Veblen) . a) . c c= ((U -Veblen) . b) . c ) ; :: thesis: verum

end;

suppose A18: a c< b ; :: thesis: ( not b in U or not c in dom ((U -Veblen) . b) or ex c being Ordinal st
( c in b & not (U -Veblen) . c is normal ) or ((U -Veblen) . a) . c c= ((U -Veblen) . b) . c )

then A19: a in b by ORDINAL1:11;
assume b in U ; :: thesis: ( not c in dom ((U -Veblen) . b) or ex c being Ordinal st
( c in b & not (U -Veblen) . c is normal ) or ((U -Veblen) . a) . c c= ((U -Veblen) . b) . c )
then A20: b in On U by ORDINAL1:def 9;
then A21: (U -Veblen) . b = criticals ((U -Veblen) | b) by A16, Def15;
dom (U -Veblen) = On U by Def15;
then b c= dom (U -Veblen) by A20, ORDINAL1:def 2;
then A22: dom ((U -Veblen) | b) = b by RELAT_1:62;
assume A23: c in dom ((U -Veblen) . b) ; :: thesis: ( ex c being Ordinal st
( c in b & not (U -Veblen) . c is normal ) or ((U -Veblen) . a) . c c= ((U -Veblen) . b) . c )
assume A24: for c being Ordinal st c in b holds
(U -Veblen) . c is normal ; :: thesis: ((U -Veblen) . a) . c c= ((U -Veblen) . b) . c

A25: now :: thesis: for c being Ordinal st c in dom ((U -Veblen) | b) holds
((U -Veblen) | b) . c is normal

let c be Ordinal; :: thesis: ( c in dom ((U -Veblen) | b) implies ((U -Veblen) | b) . c is normal )
assume c in dom ((U -Veblen) | b) ; :: thesis: ((U -Veblen) | b) . c is normal
then ( c in b & ((U -Veblen) | b) . c = (U -Veblen) . c ) by A22, FUNCT_1:49;
hence ((U -Veblen) | b) . c is normal by A24; :: thesis: verum

end;

A26: ((U -Veblen) | b) . a in rng ((U -Veblen) | b) by A19, A22, FUNCT_1:def 3;
((U -Veblen) | b) . a = (U -Veblen) . a by A18, FUNCT_1:49, ORDINAL1:11;
hence ((U -Veblen) . a) . c c= ((U -Veblen) . b) . c by A19, A21, A22, A23, A25, A26, Th54; :: thesis: verum

end;

end;

end;

for b being Ordinal holds S₁[b] from ORDINAL2:sch 1(A2, A3, A15);
hence ( ex c being Ordinal st
( c in b & not (U -Veblen) . c is normal ) or ((U -Veblen) . a) . c c= ((U -Veblen) . b) . c ) by A1; :: thesis: verum