let a, b, c be Ordinal; :: thesis: ( b in c implies a (+) b in a (+) c )
assume A1: b in c ; :: thesis: a (+) b in a (+) c
per cases ( a = 0 or a <> 0 ) ;
suppose a = 0 ; :: thesis: a (+) b in a (+) c
then ( a (+) b = b & a (+) c = c ) by Th82;
hence a (+) b in a (+) c by A1; :: thesis: verum
end;
suppose A2: a <> 0 ; :: thesis: a (+) b in a (+) c
defpred S1[ Nat] means (CantorNF b) . $1 <> (CantorNF c) . $1;
A3: ex i being Nat st S1[i]
proof
assume A4: for i being Nat holds not S1[i] ; :: thesis: contradiction
A5: dom (CantorNF b) = dom (CantorNF c)
proof
assume dom (CantorNF b) <> dom (CantorNF c) ; :: thesis: contradiction
end;
for x being object st x in dom (CantorNF b) holds
(CantorNF b) . x = (CantorNF c) . x by A4;
then Sum^ (CantorNF b) = Sum^ (CantorNF c) by A5, FUNCT_1:2;
hence contradiction by A1; :: thesis: verum
end;
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) )
proof
assume ( not i c= dom (CantorNF b) or not i c= dom (CantorNF c) ) ; :: thesis: contradiction
per cases then ( not i c= dom (CantorNF b) or not i c= dom (CantorNF c) ) ;
end;
end;
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
proof
let x be object ; :: thesis: ( x in dom ((CantorNF b) | i) implies ((CantorNF b) | i) . x = ((CantorNF c) | i) . x )
assume x in dom ((CantorNF b) | i) ; :: thesis: ((CantorNF b) | i) . x = ((CantorNF c) | i) . x
then A19: x in i by RELAT_1:57;
i in omega by ORDINAL1:def 12;
then x in omega by A19, ORDINAL1:10;
then reconsider m = x as Nat ;
m in Segm i by A19;
then A20: m < i by NAT_1:44;
thus ((CantorNF b) | i) . x = (CantorNF b) . m by A19, FUNCT_1:49
.= (CantorNF c) . m by A8, A20
.= ((CantorNF c) | i) . x by A19, FUNCT_1:49 ; :: thesis: verum
end;
then A21: (CantorNF b) | i = (CantorNF c) | i by A18, FUNCT_1:2;
A22: Sum^ ((CantorNF b) /^ i) in Sum^ ((CantorNF c) /^ i)
proof
Sum^ (CantorNF b) in Sum^ (((CantorNF c) | i) ^ ((CantorNF c) /^ i)) by A1;
then Sum^ (((CantorNF b) | i) ^ ((CantorNF b) /^ i)) in (Sum^ ((CantorNF c) | i)) +^ (Sum^ ((CantorNF c) /^ i)) by Th24;
then (Sum^ ((CantorNF b) | i)) +^ (Sum^ ((CantorNF b) /^ i)) in (Sum^ ((CantorNF c) | i)) +^ (Sum^ ((CantorNF c) /^ i)) by Th24;
hence Sum^ ((CantorNF b) /^ i) in Sum^ ((CantorNF c) /^ i) by A21, ORDINAL3:22; :: thesis: verum
end;
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
proof
( 0 in dom ((CantorNF b) /^ i) or 0 in dom ((CantorNF c) /^ i) )
proof
assume ( not 0 in dom ((CantorNF b) /^ i) & not 0 in dom ((CantorNF c) /^ i) ) ; :: thesis: contradiction
then ( dom ((CantorNF b) /^ i) c= {} & dom ((CantorNF c) /^ i) c= {} ) by ORDINAL1:16;
then ( (CantorNF b) /^ i = {} & (CantorNF c) /^ i = {} ) ;
then ( ((CantorNF b) | i) ^ ((CantorNF b) /^ i) = (CantorNF b) | i & ((CantorNF c) | i) ^ ((CantorNF c) /^ i) = (CantorNF c) | i ) ;
then A28: ( CantorNF b = (CantorNF b) | i & CantorNF c = (CantorNF c) | i ) ;
not i in i ;
then ( not i in (dom (CantorNF b)) /\ i & not i in (dom (CantorNF c)) /\ i ) by XBOOLE_0:def 4;
then A29: ( not i in dom ((CantorNF b) | i) & not i in dom ((CantorNF c) | i) ) by RELAT_1:61;
then (CantorNF b) . i = {} by A28, FUNCT_1:def 2
.= (CantorNF c) . i by A28, A29, FUNCT_1:def 2 ;
hence contradiction by A8; :: thesis: verum
end;
per cases then ( ( 0 in dom ((CantorNF b) /^ i) & 0 in dom ((CantorNF c) /^ i) ) or ( 0 in dom ((CantorNF b) /^ i) & not 0 in dom ((CantorNF c) /^ i) ) or ( not 0 in dom ((CantorNF b) /^ i) & 0 in dom ((CantorNF c) /^ i) ) ) ;
suppose ( 0 in dom ((CantorNF b) /^ i) & 0 in dom ((CantorNF c) /^ i) ) ; :: thesis: ((CantorNF b) /^ i) . 0 <> ((CantorNF c) /^ i) . 0
then ( ((CantorNF b) /^ i) . 0 = (CantorNF b) . (0 + i) & ((CantorNF c) /^ i) . 0 = (CantorNF c) . (0 + i) ) by AFINSQ_2:def 2;
hence ((CantorNF b) /^ i) . 0 <> ((CantorNF c) /^ i) . 0 by A8; :: thesis: verum
end;
suppose ( 0 in dom ((CantorNF b) /^ i) & not 0 in dom ((CantorNF c) /^ i) ) ; :: thesis: ((CantorNF b) /^ i) . 0 <> ((CantorNF c) /^ i) . 0
then ( ((CantorNF b) /^ i) . 0 <> {} & ((CantorNF c) /^ i) . 0 = {} ) by FUNCT_1:def 9, FUNCT_1:def 2;
hence ((CantorNF b) /^ i) . 0 <> ((CantorNF c) /^ i) . 0 ; :: thesis: verum
end;
suppose ( not 0 in dom ((CantorNF b) /^ i) & 0 in dom ((CantorNF c) /^ i) ) ; :: thesis: ((CantorNF b) /^ i) . 0 <> ((CantorNF c) /^ i) . 0
then ( ((CantorNF b) /^ i) . 0 = {} & ((CantorNF c) /^ i) . 0 <> {} ) by FUNCT_1:def 9, FUNCT_1:def 2;
hence ((CantorNF b) /^ i) . 0 <> ((CantorNF c) /^ i) . 0 ; :: thesis: verum
end;
end;
end;
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; :: thesis: verum
end;
end;