let fi be Ordinal-Sequence; for A, B being Ordinal st A is_limes_of fi holds
B +^ A is_limes_of B +^ fi
let A, B be Ordinal; ( A is_limes_of fi implies B +^ A is_limes_of B +^ fi )
assume A1:
( ( A = 0 & ex B being Ordinal st
( B in dom fi & ( for C being Ordinal st B c= C & C in dom fi holds
fi . C = 0 ) ) ) or ( A <> 0 & ( for B, C being Ordinal st B in A & A in C holds
ex D being Ordinal st
( D in dom fi & ( for E being Ordinal st D c= E & E in dom fi holds
( B in fi . E & fi . E in C ) ) ) ) ) )
; ORDINAL2:def 9 B +^ A is_limes_of B +^ fi
A2:
dom fi = dom (B +^ fi)
by ORDINAL3:def 1;
per cases
( B +^ A = 0 or B +^ A <> 0 )
;
ORDINAL2:def 9case
B +^ A <> 0
;
for b1, b2 being set holds
( not b1 in B +^ A or not B +^ A in b2 or ex b3 being set st
( b3 in dom (B +^ fi) & ( for b4 being set holds
( not b3 c= b4 or not b4 in dom (B +^ fi) or ( b1 in (B +^ fi) . b4 & (B +^ fi) . b4 in b2 ) ) ) ) )now for B1, B2 being Ordinal st B1 in B +^ A & B +^ A in B2 holds
ex A1 being Ordinal st
( A1 in dom (B +^ fi) & ( for C being Ordinal st A1 c= C & C in dom (B +^ fi) holds
( B1 in (B +^ fi) . C & (B +^ fi) . C in B2 ) ) )per cases
( A = {} or A <> {} )
;
suppose A9:
A = {}
;
for B1, B2 being Ordinal st B1 in B +^ A & B +^ A in B2 holds
ex A1 being Ordinal st
( A1 in dom (B +^ fi) & ( for C being Ordinal st A1 c= C & C in dom (B +^ fi) holds
( B1 in (B +^ fi) . C & (B +^ fi) . C in B2 ) ) )then consider A1 being
Ordinal such that A10:
A1 in dom fi
and A11:
for
C being
Ordinal st
A1 c= C &
C in dom fi holds
fi . C = {}
by A1;
let B1,
B2 be
Ordinal;
( B1 in B +^ A & B +^ A in B2 implies ex A1 being Ordinal st
( A1 in dom (B +^ fi) & ( for C being Ordinal st A1 c= C & C in dom (B +^ fi) holds
( B1 in (B +^ fi) . C & (B +^ fi) . C in B2 ) ) ) )assume that A12:
B1 in B +^ A
and A13:
B +^ A in B2
;
ex A1 being Ordinal st
( A1 in dom (B +^ fi) & ( for C being Ordinal st A1 c= C & C in dom (B +^ fi) holds
( B1 in (B +^ fi) . C & (B +^ fi) . C in B2 ) ) )take A1 =
A1;
( A1 in dom (B +^ fi) & ( for C being Ordinal st A1 c= C & C in dom (B +^ fi) holds
( B1 in (B +^ fi) . C & (B +^ fi) . C in B2 ) ) )thus
A1 in dom (B +^ fi)
by A10, ORDINAL3:def 1;
for C being Ordinal st A1 c= C & C in dom (B +^ fi) holds
( B1 in (B +^ fi) . C & (B +^ fi) . C in B2 )let C be
Ordinal;
( A1 c= C & C in dom (B +^ fi) implies ( B1 in (B +^ fi) . C & (B +^ fi) . C in B2 ) )assume that A14:
A1 c= C
and A15:
C in dom (B +^ fi)
;
( B1 in (B +^ fi) . C & (B +^ fi) . C in B2 )
(B +^ fi) . C = B +^ (fi . C)
by A2, A15, ORDINAL3:def 1;
hence
(
B1 in (B +^ fi) . C &
(B +^ fi) . C in B2 )
by A2, A9, A11, A12, A13, A14, A15;
verum end; suppose A16:
A <> {}
;
for B1, B2 being Ordinal st B1 in B +^ A & B +^ A in B2 holds
ex A1 being Ordinal st
( A1 in dom (B +^ fi) & ( for C being Ordinal st A1 c= C & C in dom (B +^ fi) holds
( B1 in (B +^ fi) . C & (B +^ fi) . C in B2 ) ) )let B1,
B2 be
Ordinal;
( B1 in B +^ A & B +^ A in B2 implies ex A1 being Ordinal st
( A1 in dom (B +^ fi) & ( for C being Ordinal st A1 c= C & C in dom (B +^ fi) holds
( B1 in (B +^ fi) . C & (B +^ fi) . C in B2 ) ) ) )assume that A17:
B1 in B +^ A
and A18:
B +^ A in B2
;
ex A1 being Ordinal st
( A1 in dom (B +^ fi) & ( for C being Ordinal st A1 c= C & C in dom (B +^ fi) holds
( B1 in (B +^ fi) . C & (B +^ fi) . C in B2 ) ) )
B1 -^ B in A
by A16, A17, ORDINAL3:60;
then consider A1 being
Ordinal such that A19:
A1 in dom fi
and A20:
for
C being
Ordinal st
A1 c= C &
C in dom fi holds
(
B1 -^ B in fi . C &
fi . C in B2 -^ B )
by A1, A18, ORDINAL3:61;
A21:
B1 c= B +^ (B1 -^ B)
by ORDINAL3:62;
A22:
B c= B +^ A
by ORDINAL3:24;
B +^ A c= B2
by A18, ORDINAL1:def 2;
then
B c= B2
by A22;
then A23:
B +^ (B2 -^ B) = B2
by ORDINAL3:def 5;
take A1 =
A1;
( A1 in dom (B +^ fi) & ( for C being Ordinal st A1 c= C & C in dom (B +^ fi) holds
( B1 in (B +^ fi) . C & (B +^ fi) . C in B2 ) ) )thus
A1 in dom (B +^ fi)
by A19, ORDINAL3:def 1;
for C being Ordinal st A1 c= C & C in dom (B +^ fi) holds
( B1 in (B +^ fi) . C & (B +^ fi) . C in B2 )let C be
Ordinal;
( A1 c= C & C in dom (B +^ fi) implies ( B1 in (B +^ fi) . C & (B +^ fi) . C in B2 ) )assume that A24:
A1 c= C
and A25:
C in dom (B +^ fi)
;
( B1 in (B +^ fi) . C & (B +^ fi) . C in B2 )A26:
(B +^ fi) . C = B +^ (fi . C)
by A2, A25, ORDINAL3:def 1;
reconsider E =
fi . C as
Ordinal ;
B1 -^ B in E
by A2, A20, A24, A25;
then A27:
B +^ (B1 -^ B) in B +^ E
by ORDINAL2:32;
E in B2 -^ B
by A2, A20, A24, A25;
hence
(
B1 in (B +^ fi) . C &
(B +^ fi) . C in B2 )
by A21, A26, A23, A27, ORDINAL1:12, ORDINAL2:32;
verum end; end; end; hence
for
b1,
b2 being
set holds
( not
b1 in B +^ A or not
B +^ A in b2 or ex
b3 being
set st
(
b3 in dom (B +^ fi) & ( for
b4 being
set holds
( not
b3 c= b4 or not
b4 in dom (B +^ fi) or (
b1 in (B +^ fi) . b4 &
(B +^ fi) . b4 in b2 ) ) ) ) )
;
verum end; end;