let A, B, C be Ordinal; (A +^ B) +^ C = A +^ (B +^ C)
defpred S1[ Ordinal] means (A +^ B) +^ $1 = A +^ (B +^ $1);
A1:
for C being Ordinal st S1[C] holds
S1[ succ C]
A3:
for C being Ordinal st C <> 0 & C is limit_ordinal & ( for D being Ordinal st D in C holds
S1[D] ) holds
S1[C]
proof
deffunc H1(
Ordinal)
-> set =
(A +^ B) +^ $1;
let C be
Ordinal;
( C <> 0 & C is limit_ordinal & ( for D being Ordinal st D in C holds
S1[D] ) implies S1[C] )
assume that A4:
C <> 0
and A5:
C is
limit_ordinal
and A6:
for
D being
Ordinal st
D in C holds
S1[
D]
;
S1[C]
consider L being
Ordinal-Sequence such that A7:
(
dom L = C & ( for
D being
Ordinal st
D in C holds
L . D = H1(
D) ) )
from ORDINAL2:sch 3();
deffunc H2(
Ordinal)
-> set =
A +^ $1;
consider L1 being
Ordinal-Sequence such that A8:
(
dom L1 = B +^ C & ( for
D being
Ordinal st
D in B +^ C holds
L1 . D = H2(
D) ) )
from ORDINAL2:sch 3();
A9:
rng L c= rng L1
proof
let x be
object ;
TARSKI:def 3 ( not x in rng L or x in rng L1 )
assume
x in rng L
;
x in rng L1
then consider y being
object such that A10:
y in dom L
and A11:
x = L . y
by FUNCT_1:def 3;
reconsider y =
y as
Ordinal by A10;
A12:
B +^ y in B +^ C
by A7, A10, ORDINAL2:32;
L . y = (A +^ B) +^ y
by A7, A10;
then A13:
L . y = A +^ (B +^ y)
by A6, A7, A10;
L1 . (B +^ y) = A +^ (B +^ y)
by A7, A8, A10, ORDINAL2:32;
hence
x in rng L1
by A8, A11, A13, A12, FUNCT_1:def 3;
verum
end;
A14:
B +^ C <> {}
by A4, Th26;
B +^ C is
limit_ordinal
by A4, A5, Th29;
then A15:
A +^ (B +^ C) =
sup L1
by A8, A14, ORDINAL2:29
.=
sup (rng L1)
;
(A +^ B) +^ C =
sup L
by A4, A5, A7, ORDINAL2:29
.=
sup (rng L)
;
hence
(A +^ B) +^ C c= A +^ (B +^ C)
by A15, A9, ORDINAL2:22;
XBOOLE_0:def 10 A +^ (B +^ C) c= (A +^ B) +^ C
let x be
object ;
TARSKI:def 3 ( not x in A +^ (B +^ C) or x in (A +^ B) +^ C )
assume A16:
x in A +^ (B +^ C)
;
x in (A +^ B) +^ C
then reconsider x9 =
x as
Ordinal ;
A23:
(A +^ B) +^ {} = A +^ B
by ORDINAL2:27;
(A +^ B) +^ {} c= (A +^ B) +^ C
by ORDINAL2:33, XBOOLE_1:2;
hence
x in (A +^ B) +^ C
by A23, A17;
verum
end;
(A +^ B) +^ {} =
A +^ B
by ORDINAL2:27
.=
A +^ (B +^ {})
by ORDINAL2:27
;
then A24:
S1[ 0 ]
;
for C being Ordinal holds S1[C]
from ORDINAL2:sch 1(A24, A1, A3);
hence
(A +^ B) +^ C = A +^ (B +^ C)
; verum