let X, Y be finite natural-membered set ; ( X <N< Y iff Sgm0 (X \/ Y) = (Sgm0 X) ^ (Sgm0 Y) )
set p = Sgm0 X;
set q = Sgm0 Y;
set r = Sgm0 (X \/ Y);
thus
( X <N< Y implies Sgm0 (X \/ Y) = (Sgm0 X) ^ (Sgm0 Y) )
( Sgm0 (X \/ Y) = (Sgm0 X) ^ (Sgm0 Y) implies X <N< Y )proof
defpred S1[
Nat]
means ( $1
in dom (Sgm0 X) implies
(Sgm0 (X \/ Y)) . $1
= (Sgm0 X) . $1 );
reconsider X1 =
X,
Y1 =
Y as
finite set ;
assume A1:
X <N< Y
;
Sgm0 (X \/ Y) = (Sgm0 X) ^ (Sgm0 Y)
X /\ Y = {}
then A5:
X misses Y
;
A6:
len (Sgm0 (X \/ Y)) =
card (X1 \/ Y1)
by Th20
.=
(card X1) + (card Y1)
by A5, CARD_2:40
.=
(len (Sgm0 X)) + (card Y1)
by Th20
.=
(len (Sgm0 X)) + (len (Sgm0 Y))
by Th20
;
A7:
now for k being Nat st S1[k] holds
S1[k + 1]let k be
Nat;
( S1[k] implies S1[k + 1] )assume A8:
S1[
k]
;
S1[k + 1]thus
S1[
k + 1]
verumproof
set m =
(Sgm0 (X \/ Y)) . (k + 1);
set n =
(Sgm0 X) . (k + 1);
assume A9:
k + 1
in dom (Sgm0 X)
;
(Sgm0 (X \/ Y)) . (k + 1) = (Sgm0 X) . (k + 1)
then
(Sgm0 X) . (k + 1) in rng (Sgm0 X)
by FUNCT_1:def 3;
then A10:
(Sgm0 X) . (k + 1) in X
by Def4;
len (Sgm0 X) <= len (Sgm0 (X \/ Y))
by A6, NAT_1:12;
then A11:
Segm (len (Sgm0 X)) c= Segm (len (Sgm0 (X \/ Y)))
by NAT_1:39;
then
(Sgm0 (X \/ Y)) . (k + 1) in rng (Sgm0 (X \/ Y))
by A9, FUNCT_1:def 3;
then A12:
(Sgm0 (X \/ Y)) . (k + 1) in X \/ Y
by Def4;
assume A13:
(Sgm0 (X \/ Y)) . (k + 1) <> (Sgm0 X) . (k + 1)
;
contradiction
now contradictionper cases
( k in dom (Sgm0 X) or not k in dom (Sgm0 X) )
;
suppose A14:
k in dom (Sgm0 X)
;
contradictionset m1 =
(Sgm0 (X \/ Y)) . k;
set n1 =
(Sgm0 X) . k;
now contradictionper cases
( (Sgm0 (X \/ Y)) . (k + 1) < (Sgm0 X) . (k + 1) or (Sgm0 X) . (k + 1) < (Sgm0 (X \/ Y)) . (k + 1) )
by A13, XXREAL_0:1;
suppose A15:
(Sgm0 (X \/ Y)) . (k + 1) < (Sgm0 X) . (k + 1)
;
contradictionthen
not
(Sgm0 (X \/ Y)) . (k + 1) in Y
by A1, A10;
then
(Sgm0 (X \/ Y)) . (k + 1) in X
by A12, XBOOLE_0:def 3;
then
(Sgm0 (X \/ Y)) . (k + 1) in rng (Sgm0 X)
by Def4;
then consider x being
object such that A16:
x in dom (Sgm0 X)
and A17:
(Sgm0 X) . x = (Sgm0 (X \/ Y)) . (k + 1)
by FUNCT_1:def 3;
reconsider x =
x as
Element of
NAT by A16;
x < len (Sgm0 X)
by A16, AFINSQ_1:86;
then A18:
x < k + 1
by A15, A17, Th33;
A19:
k < k + 1
by XREAL_1:29;
k + 1
< len (Sgm0 (X \/ Y))
by A9, A11, AFINSQ_1:86;
then A20:
(Sgm0 X) . k < (Sgm0 (X \/ Y)) . (k + 1)
by A8, A14, A19, Def4;
k < len (Sgm0 X)
by A14, AFINSQ_1:86;
then
k < x
by A17, A20, Th33;
hence
contradiction
by A18, NAT_1:13;
verum end; suppose A21:
(Sgm0 X) . (k + 1) < (Sgm0 (X \/ Y)) . (k + 1)
;
contradiction
(Sgm0 X) . (k + 1) in X \/ Y
by A10, XBOOLE_0:def 3;
then
(Sgm0 X) . (k + 1) in rng (Sgm0 (X \/ Y))
by Def4;
then consider x being
object such that A22:
x in dom (Sgm0 (X \/ Y))
and A23:
(Sgm0 (X \/ Y)) . x = (Sgm0 X) . (k + 1)
by FUNCT_1:def 3;
reconsider x =
x as
Element of
NAT by A22;
x < len (Sgm0 (X \/ Y))
by A22, AFINSQ_1:86;
then A24:
x < k + 1
by A21, A23, Th33;
A25:
k < k + 1
by XREAL_1:29;
k + 1
< len (Sgm0 X)
by A9, AFINSQ_1:86;
then A26:
(Sgm0 (X \/ Y)) . k < (Sgm0 X) . (k + 1)
by A8, A14, A25, Def4;
k < len (Sgm0 (X \/ Y))
by A11, A14, AFINSQ_1:86;
then
k < x
by A23, A26, Th33;
hence
contradiction
by A24, NAT_1:13;
verum end; end; end; hence
contradiction
;
verum end; end; end;
hence
contradiction
;
verum
end; end;
(
0 < len (Sgm0 X) implies
X1 <> {} )
by Th20, CARD_1:27;
then A29:
S1[
0 ]
by A1, Th34;
A30:
for
k being
Nat holds
S1[
k]
from NAT_1:sch 2(A29, A7);
defpred S2[
Nat]
means ( $1
in dom (Sgm0 Y) implies
(Sgm0 (X \/ Y)) . ((len (Sgm0 X)) + $1) = (Sgm0 Y) . $1 );
A31:
now for k being Nat st S2[k] holds
S2[k + 1]let k be
Nat;
( S2[k] implies S2[k + 1] )assume A32:
S2[
k]
;
S2[k + 1]thus
S2[
k + 1]
verumproof
set n =
(Sgm0 Y) . (k + 1);
set a =
(len (Sgm0 X)) + (k + 1);
set m =
(Sgm0 (X \/ Y)) . ((len (Sgm0 X)) + (k + 1));
assume A33:
k + 1
in dom (Sgm0 Y)
;
(Sgm0 (X \/ Y)) . ((len (Sgm0 X)) + (k + 1)) = (Sgm0 Y) . (k + 1)
then
(Sgm0 Y) . (k + 1) in rng (Sgm0 Y)
by FUNCT_1:def 3;
then A34:
(Sgm0 Y) . (k + 1) in Y
by Def4;
k + 1
< len (Sgm0 Y)
by A33, AFINSQ_1:86;
then A35:
(len (Sgm0 X)) + (k + 1) < len (Sgm0 (X \/ Y))
by A6, XREAL_1:6;
then A36:
(len (Sgm0 X)) + (k + 1) in dom (Sgm0 (X \/ Y))
by AFINSQ_1:86;
then
(Sgm0 (X \/ Y)) . ((len (Sgm0 X)) + (k + 1)) in rng (Sgm0 (X \/ Y))
by FUNCT_1:def 3;
then A37:
(Sgm0 (X \/ Y)) . ((len (Sgm0 X)) + (k + 1)) in X \/ Y
by Def4;
assume A43:
(Sgm0 (X \/ Y)) . ((len (Sgm0 X)) + (k + 1)) <> (Sgm0 Y) . (k + 1)
;
contradiction
now contradictionper cases
( k in dom (Sgm0 Y) or not k in dom (Sgm0 Y) )
;
suppose A44:
k in dom (Sgm0 Y)
;
contradictionset m1 =
(Sgm0 (X \/ Y)) . ((len (Sgm0 X)) + k);
set n1 =
(Sgm0 Y) . k;
A45:
k < len (Sgm0 Y)
by A44, AFINSQ_1:86;
now contradictionper cases
( (Sgm0 (X \/ Y)) . ((len (Sgm0 X)) + (k + 1)) < (Sgm0 Y) . (k + 1) or (Sgm0 Y) . (k + 1) < (Sgm0 (X \/ Y)) . ((len (Sgm0 X)) + (k + 1)) )
by A43, XXREAL_0:1;
suppose A46:
(Sgm0 (X \/ Y)) . ((len (Sgm0 X)) + (k + 1)) < (Sgm0 Y) . (k + 1)
;
contradiction
(Sgm0 (X \/ Y)) . ((len (Sgm0 X)) + (k + 1)) in Y
by A37, A38, XBOOLE_0:def 3;
then
(Sgm0 (X \/ Y)) . ((len (Sgm0 X)) + (k + 1)) in rng (Sgm0 Y)
by Def4;
then consider x being
object such that A47:
x in dom (Sgm0 Y)
and A48:
(Sgm0 Y) . x = (Sgm0 (X \/ Y)) . ((len (Sgm0 X)) + (k + 1))
by FUNCT_1:def 3;
reconsider x =
x as
Element of
NAT by A47;
x < len (Sgm0 Y)
by A47, AFINSQ_1:86;
then A49:
x < k + 1
by A46, A48, Th33;
(len (Sgm0 X)) + k < ((len (Sgm0 X)) + k) + 1
by XREAL_1:29;
then A50:
(Sgm0 Y) . k < (Sgm0 (X \/ Y)) . ((len (Sgm0 X)) + (k + 1))
by A32, A35, A44, Def4;
k < len (Sgm0 Y)
by A44, AFINSQ_1:86;
then
k < x
by A48, A50, Th33;
hence
contradiction
by A49, NAT_1:13;
verum end; suppose A51:
(Sgm0 Y) . (k + 1) < (Sgm0 (X \/ Y)) . ((len (Sgm0 X)) + (k + 1))
;
contradiction
(Sgm0 Y) . (k + 1) in X \/ Y
by A34, XBOOLE_0:def 3;
then
(Sgm0 Y) . (k + 1) in rng (Sgm0 (X \/ Y))
by Def4;
then consider x being
object such that A52:
x in dom (Sgm0 (X \/ Y))
and A53:
(Sgm0 (X \/ Y)) . x = (Sgm0 Y) . (k + 1)
by FUNCT_1:def 3;
reconsider x =
x as
Element of
NAT by A52;
x < len (Sgm0 (X \/ Y))
by A52, AFINSQ_1:86;
then A54:
x < ((len (Sgm0 X)) + k) + 1
by A51, A53, Th33;
A55:
k < k + 1
by XREAL_1:29;
k + 1
< len (Sgm0 Y)
by A33, AFINSQ_1:86;
then A56:
(Sgm0 (X \/ Y)) . ((len (Sgm0 X)) + k) < (Sgm0 Y) . (k + 1)
by A32, A44, A55, Def4;
(len (Sgm0 X)) + k < len (Sgm0 (X \/ Y))
by A6, A45, XREAL_1:6;
then
(len (Sgm0 X)) + k < x
by A53, A56, Th33;
hence
contradiction
by A54, NAT_1:13;
verum end; end; end; hence
contradiction
;
verum end; end; end;
hence
contradiction
;
verum
end; end;
(
len (Sgm0 Y) > 0 implies
Y <> {} )
by Th20, CARD_1:27;
then A59:
S2[
0 ]
by A1, Th32;
for
k being
Nat holds
S2[
k]
from NAT_1:sch 2(A59, A31);
hence
Sgm0 (X \/ Y) = (Sgm0 X) ^ (Sgm0 Y)
by A6, A30, AFINSQ_1:def 3;
verum
end;
assume A60:
Sgm0 (X \/ Y) = (Sgm0 X) ^ (Sgm0 Y)
; X <N< Y
let m, n be Nat; AFINSQ_2:def 5 ( m in X & n in Y implies m < n )
assume that
A61:
m in X
and
A62:
n in Y
; m < n
n in rng (Sgm0 Y)
by A62, Def4;
then consider y being object such that
A63:
y in dom (Sgm0 Y)
and
A64:
(Sgm0 Y) . y = n
by FUNCT_1:def 3;
reconsider y = y as Element of NAT by A63;
A65:
n = (Sgm0 (X \/ Y)) . ((len (Sgm0 X)) + y)
by A60, A63, A64, AFINSQ_1:def 3;
y < len (Sgm0 Y)
by A63, AFINSQ_1:86;
then
(len (Sgm0 X)) + y < (len (Sgm0 X)) + (len (Sgm0 Y))
by XREAL_1:6;
then A66:
(len (Sgm0 X)) + y < len (Sgm0 (X \/ Y))
by A60, AFINSQ_1:17;
A67:
len (Sgm0 X) <= (len (Sgm0 X)) + y
by NAT_1:12;
m in rng (Sgm0 X)
by A61, Def4;
then consider x being object such that
A68:
x in dom (Sgm0 X)
and
A69:
(Sgm0 X) . x = m
by FUNCT_1:def 3;
reconsider x = x as Element of NAT by A68;
x < len (Sgm0 X)
by A68, AFINSQ_1:86;
then A70:
x < (len (Sgm0 X)) + y
by A67, XXREAL_0:2;
m = (Sgm0 (X \/ Y)) . x
by A60, A68, A69, AFINSQ_1:def 3;
hence
m < n
by A65, A70, A66, Def4; verum