let a, b, c be ordinal number ; :: 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 number 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 number st c in b holds
(U -Veblen) . c is normal ) implies ((U -Veblen) . a) . c c= ((U -Veblen) . b) . c )
assume A0: ( a c= b & b in U & omega in U & c in dom ((U -Veblen) . b) ) ; :: thesis: ( ex c being ordinal number 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 number st a c= $1 & $1 in U & c in dom ((U -Veblen) . $1) & ( for c being ordinal number st c in $1 holds
(U -Veblen) . c is normal ) holds
((U -Veblen) . a) . c c= ((U -Veblen) . $1) . c;
01: S₁[ 0 ] ;
02: 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 A1: S₁[b] ; :: thesis: S₁[ succ b]
let a, c be ordinal number ; :: thesis: ( a c= succ b & succ b in U & c in dom ((U -Veblen) . (succ b)) & ( for c being ordinal number st c in succ b holds
(U -Veblen) . c is normal ) implies ((U -Veblen) . a) . c c= ((U -Veblen) . (succ b)) . c )
assume that
A2: a c= succ b and
A3: succ b in U and
A4: c in dom ((U -Veblen) . (succ b)) ; :: thesis: ( ex c being ordinal number st
( c in succ b & not (U -Veblen) . c is normal ) or ((U -Veblen) . a) . c c= ((U -Veblen) . (succ b)) . c )
assume Z0: for c being ordinal number 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 A3, ORDINAL1:def 9;
then A5: (U -Veblen) . (succ b) = criticals ((U -Veblen) . b) by V;
then A6: dom ((U -Veblen) . (succ b)) c= dom ((U -Veblen) . b) by Th05;
Z1: b in succ b by ORDINAL1:6;
then A7: b in U by A3, ORDINAL1:10;
(U -Veblen) . b is normal by Z0, ORDINAL1:6;
then A8: ((U -Veblen) . b) . c c= ((U -Veblen) . (succ b)) . c by A4, A5, Th40;
A9: for c being ordinal number st c in b holds
(U -Veblen) . c is normal by Z0, Z1, ORDINAL1:10;

per cases ( a = succ b or a c= b ) by A2, 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 A1, A4, A6, A7, A9;
hence ((U -Veblen) . a) . c c= ((U -Veblen) . (succ b)) . c by A8, XBOOLE_1:1; :: thesis: verum

end;

end;

end;

03: 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 Z1: ( b <> {} & b is limit_ordinal ) ; :: thesis: ( ex d being ordinal number st
( d in b & not S₁[d] ) or S₁[b] )
assume for d being ordinal number st d in b holds
S₁[d] ; :: thesis: S₁[b]
let a, c be ordinal number ; :: thesis: ( a c= b & b in U & c in dom ((U -Veblen) . b) & ( for c being ordinal number st c in b holds
(U -Veblen) . c is normal ) implies ((U -Veblen) . a) . c c= ((U -Veblen) . b) . c )
assume Z3: a c= b ; :: thesis: ( not b in U or not c in dom ((U -Veblen) . b) or ex c being ordinal number 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 Z3, XBOOLE_0:def 8;

suppose a = b ; :: thesis: ( not b in U or not c in dom ((U -Veblen) . b) or ex c being ordinal number 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 number st
( c in b & not (U -Veblen) . c is normal ) or ((U -Veblen) . a) . c c= ((U -Veblen) . b) . c ) ; :: thesis: verum

end;

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

then B0: a in b by ORDINAL1:11;
assume b in U ; :: thesis: ( not c in dom ((U -Veblen) . b) or ex c being ordinal number st
( c in b & not (U -Veblen) . c is normal ) or ((U -Veblen) . a) . c c= ((U -Veblen) . b) . c )
then B1: b in On U by ORDINAL1:def 9;
then B2: (U -Veblen) . b = criticals ((U -Veblen) | b) by Z1, V;
dom (U -Veblen) = On U by V;
then b c= dom (U -Veblen) by B1, ORDINAL1:def 2;
then B4: dom ((U -Veblen) | b) = b by RELAT_1:62;
assume Z5: c in dom ((U -Veblen) . b) ; :: thesis: ( ex c being ordinal number st
( c in b & not (U -Veblen) . c is normal ) or ((U -Veblen) . a) . c c= ((U -Veblen) . b) . c )
assume Z7: for c being ordinal number st c in b holds
(U -Veblen) . c is normal ; :: thesis: ((U -Veblen) . a) . c c= ((U -Veblen) . b) . c

Z6: now

let c be ordinal number ; :: 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 B4, FUNCT_1:49;
hence ((U -Veblen) | b) . c is normal by Z7; :: thesis: verum

end;

B6: ((U -Veblen) | b) . a in rng ((U -Veblen) | b) by B0, B4, FUNCT_1:def 3;
((U -Veblen) | b) . a = (U -Veblen) . a by C0, FUNCT_1:49, ORDINAL1:11;
hence ((U -Veblen) . a) . c c= ((U -Veblen) . b) . c by B0, B2, B4, Z5, Z6, B6, ThAB; :: thesis: verum

end;

end;

end;

for b being ordinal number holds S₁[b] from ORDINAL2:sch 1(01, 02, 03);
hence ( ex c being ordinal number st
( c in b & not (U -Veblen) . c is normal ) or ((U -Veblen) . a) . c c= ((U -Veblen) . b) . c ) by A0; :: thesis: verum