let a, b, c be Ordinal; :: thesis: ( a c= b & 0 in c implies c |^|^ a c= c |^|^ b )
assume that
A1: a c= b and
A2: 0 in c ; :: thesis: c |^|^ a c= c |^|^ b
( succ 0 c= c & succ 0 = 0 + 1 ) by A2, ORDINAL1:21;
then A3: ( 1 c< c or 1 = c ) ;
per cases ( c = 1 or 1 in c ) by A3, ORDINAL1:11;
suppose c = 1 ; :: thesis: c |^|^ a c= c |^|^ b
then ( c |^|^ a = 1 & c |^|^ b = 1 ) by Th17;
hence c |^|^ a c= c |^|^ b ; :: thesis: verum
end;
suppose A4: 1 in c ; :: thesis: c |^|^ a c= c |^|^ b
defpred S1[ Ordinal] means for a, b being Ordinal st a c= b & b c= $1 holds
c |^|^ a c= c |^|^ b;
A5: S1[ 0 ]
proof
let a, b be Ordinal; :: thesis: ( a c= b & b c= 0 implies c |^|^ a c= c |^|^ b )
assume A6: ( a c= b & b c= 0 ) ; :: thesis: c |^|^ a c= c |^|^ b
then b = {} ;
hence c |^|^ a c= c |^|^ b by A6; :: thesis: verum
end;
A7: now :: thesis: for d being Ordinal st S1[d] holds
S1[ succ d]
let d be Ordinal; :: thesis: ( S1[d] implies S1[ succ d] )
assume A8: S1[d] ; :: thesis: S1[ succ d]
c |^|^ (succ d) = exp (c,(c |^|^ d)) by Th14;
then A9: c |^|^ d c= c |^|^ (succ d) by A4, ORDINAL4:32;
thus S1[ succ d] :: thesis: verum
proof
let a, b be Ordinal; :: thesis: ( a c= b & b c= succ d implies c |^|^ a c= c |^|^ b )
assume A10: ( a c= b & b c= succ d ) ; :: thesis: c |^|^ a c= c |^|^ b
A11: a c= succ d by A10;
per cases ( b c= d or ( b = succ d & a = succ d ) or ( b = succ d & a c= d ) ) by A10, A11, Th1;
suppose b c= d ; :: thesis: c |^|^ a c= c |^|^ b
hence c |^|^ a c= c |^|^ b by A8, A10; :: thesis: verum
end;
suppose ( b = succ d & a = succ d ) ; :: thesis: c |^|^ a c= c |^|^ b
hence c |^|^ a c= c |^|^ b ; :: thesis: verum
end;
suppose A12: ( b = succ d & a c= d ) ; :: thesis: c |^|^ a c= c |^|^ b
then c |^|^ a c= c |^|^ d by A8;
hence c |^|^ a c= c |^|^ b by A9, A12; :: thesis: verum
end;
end;
end;
end;
A13: now :: thesis: for d being Ordinal st d <> 0 & d is limit_ordinal & ( for e being Ordinal st e in d holds
S1[e] ) holds
S1[d]
let d be Ordinal; :: thesis: ( d <> 0 & d is limit_ordinal & ( for e being Ordinal st e in d holds
S1[e] ) implies S1[d] )
assume that
A14: ( d <> 0 & d is limit_ordinal ) and
A15: for e being Ordinal st e in d holds
S1[e] ; :: thesis: S1[d]
deffunc H1( Ordinal) -> Ordinal = c |^|^ $1;
consider f being Ordinal-Sequence such that
A16: ( dom f = d & ( for e being Ordinal st e in d holds
f . e = H1(e) ) ) from ORDINAL2:sch 3();
 f is non-decreasing
proof
let a be Ordinal; :: according to ORDINAL5:def 2 :: thesis: for b being Ordinal st a in b & b in dom f holds
f . a c= f . b
let b be Ordinal; :: thesis: ( a in b & b in dom f implies f . a c= f . b )
assume A17: ( a in b & b in dom f ) ; :: thesis: f . a c= f . b
then ( a c= b & S1[b] ) by A15, A16, ORDINAL1:def 2;
then ( c |^|^ a c= c |^|^ b & a in d & f . b = H1(b) ) by A16, A17, ORDINAL1:12;
hence f . a c= f . b by A16; :: thesis: verum
end;
then A18: Union f is_limes_of f by A14, A16, Th6;
c |^|^ d = lim f by A14, A16, Th15;
then A19: c |^|^ d = Union f by A18, ORDINAL2:def 10;
thus S1[d] :: thesis: verum
proof
let a, b be Ordinal; :: thesis: ( a c= b & b c= d implies c |^|^ a c= c |^|^ b )
assume A20: ( a c= b & b c= d ) ; :: thesis: c |^|^ a c= c |^|^ b
then A21: ( ( b c< d or b = d ) & ( a c< b or a = b ) ) ;
per cases ( b in d or ( b = d & a in d ) or ( b = d & a = d ) ) by A21, ORDINAL1:11;
suppose b in d ; :: thesis: c |^|^ a c= c |^|^ b
hence H1(a) c= H1(b) by A20, A15; :: thesis: verum
end;
suppose A22: ( b = d & a in d ) ; :: thesis: c |^|^ a c= c |^|^ b
then ( f . a in rng f & f . a = H1(a) ) by A16, FUNCT_1:def 3;
hence H1(a) c= H1(b) by A19, A22, ZFMISC_1:74; :: thesis: verum
end;
suppose ( b = d & a = d ) ; :: thesis: c |^|^ a c= c |^|^ b
hence H1(a) c= H1(b) ; :: thesis: verum
end;
end;
end;
end;
for b being Ordinal holds S1[b] from ORDINAL2:sch 1(A5, A7, A13);
hence c |^|^ a c= c |^|^ b by A1; :: thesis: verum
end;
end;