let a, b, c be Ordinal; ( b in c implies a (+) b in a (+) c )
assume A1:
b in c
; a (+) b in a (+) c
per cases
( a = 0 or a <> 0 )
;
suppose A2:
a <> 0
;
a (+) b in a (+) cdefpred S1[
Nat]
means (CantorNF b) . $1
<> (CantorNF c) . $1;
A3:
ex
i being
Nat st
S1[
i]
consider i being
Nat such that A8:
(
S1[
i] & ( for
j being
Nat st
S1[
j] holds
i <= j ) )
from NAT_1:sch 5(A3);
set A1 =
(CantorNF b) | i;
set A2 =
(CantorNF c) | i;
set B1 =
(CantorNF b) /^ i;
set B2 =
(CantorNF c) /^ i;
A9:
(
i c= dom (CantorNF b) &
i c= dom (CantorNF c) )
A18:
dom ((CantorNF b) | i) =
(dom (CantorNF b)) /\ i
by RELAT_1:61
.=
i
by A9, XBOOLE_1:28
.=
(dom (CantorNF c)) /\ i
by A9, XBOOLE_1:28
.=
dom ((CantorNF c) | i)
by RELAT_1:61
;
for
x being
object st
x in dom ((CantorNF b) | i) holds
((CantorNF b) | i) . x = ((CantorNF c) | i) . x
then A21:
(CantorNF b) | i = (CantorNF c) | i
by A18, FUNCT_1:2;
A22:
Sum^ ((CantorNF b) /^ i) in Sum^ ((CantorNF c) /^ i)
A23:
((CantorNF b) | i) ^ ((CantorNF b) /^ i) is
Cantor-normal-form
;
A24:
((CantorNF c) | i) ^ ((CantorNF c) /^ i) is
Cantor-normal-form
;
A25:
b =
Sum^ (((CantorNF b) | i) ^ ((CantorNF b) /^ i))
.=
(Sum^ ((CantorNF b) | i)) +^ (Sum^ ((CantorNF b) /^ i))
by Th24
.=
(Sum^ ((CantorNF b) | i)) (+) (Sum^ ((CantorNF b) /^ i))
by A23, Th84
;
A26:
c =
Sum^ (((CantorNF c) | i) ^ ((CantorNF c) /^ i))
.=
(Sum^ ((CantorNF c) | i)) +^ (Sum^ ((CantorNF c) /^ i))
by Th24
.=
(Sum^ ((CantorNF c) | i)) (+) (Sum^ ((CantorNF c) /^ i))
by A24, Th84
;
A27:
not
a (+) (Sum^ ((CantorNF b) | i)) is
empty
by A2;
((CantorNF b) /^ i) . 0 <> ((CantorNF c) /^ i) . 0
then
(CantorNF (Sum^ ((CantorNF b) /^ i))) . 0 <> (CantorNF (Sum^ ((CantorNF c) /^ i))) . 0
;
then
(a (+) (Sum^ ((CantorNF b) | i))) (+) (Sum^ ((CantorNF b) /^ i)) in (a (+) (Sum^ ((CantorNF c) | i))) (+) (Sum^ ((CantorNF c) /^ i))
by A21, A22, A27, Lm11;
then
a (+) b in (a (+) (Sum^ ((CantorNF c) | i))) (+) (Sum^ ((CantorNF c) /^ i))
by A25, Th81;
hence
a (+) b in a (+) c
by A26, Th81;
verum end; end;