let X, Y be set ; :: thesis: for i, j being natural number st X c= Seg i & Y c= Seg j holds
( ( for m, n being Element of NAT st m in X & n in Y holds
m < n ) iff Sgm (X \/ Y) = (Sgm X) ^ (Sgm Y) )
let i, j be natural number ; :: thesis: ( X c= Seg i & Y c= Seg j implies ( ( for m, n being Element of NAT st m in X & n in Y holds
m < n ) iff Sgm (X \/ Y) = (Sgm X) ^ (Sgm Y) ) )
assume that
A1:
X c= Seg i
and
A2:
Y c= Seg j
; :: thesis: ( ( for m, n being Element of NAT st m in X & n in Y holds
m < n ) iff Sgm (X \/ Y) = (Sgm X) ^ (Sgm Y) )
Seg i, Seg j are_c=-comparable
by Th20;
then
( Seg i c= Seg j or Seg j c= Seg i )
by XBOOLE_0:def 9;
then A3:
( X c= Seg j or Y c= Seg i )
by A1, A2, XBOOLE_1:1;
then A4:
( X \/ Y c= Seg i or X \/ Y c= Seg j )
by A1, A2, XBOOLE_1:8;
set p = Sgm X;
set q = Sgm Y;
set r = Sgm (X \/ Y);
thus
( ( for m, n being Element of NAT st m in X & n in Y holds
m < n ) implies Sgm (X \/ Y) = (Sgm X) ^ (Sgm Y) )
:: thesis: ( Sgm (X \/ Y) = (Sgm X) ^ (Sgm Y) implies for m, n being Element of NAT st m in X & n in Y holds
m < n )proof
assume A5:
for
m,
n being
Element of
NAT st
m in X &
n in Y holds
m < n
;
:: thesis: Sgm (X \/ Y) = (Sgm X) ^ (Sgm Y)
X /\ Y = {}
then A7:
X misses Y
by XBOOLE_0:def 7;
reconsider X1 =
X,
Y1 =
Y as
finite set by A1, A2;
A8:
len (Sgm (X \/ Y)) =
card (X1 \/ Y1)
by A1, A2, A3, Th44, XBOOLE_1:8
.=
(card X1) + (card Y1)
by A7, CARD_2:53
.=
(len (Sgm X)) + (card Y1)
by A1, Th44
.=
(len (Sgm X)) + (len (Sgm Y))
by A2, Th44
;
defpred S1[
Element of
NAT ]
means ( $1
in dom (Sgm X) implies
(Sgm (X \/ Y)) . $1
= (Sgm X) . $1 );
A9:
S1[
0 ]
by Th26;
A10:
now let k be
Element of
NAT ;
:: thesis: ( S1[k] implies S1[k + 1] )assume A11:
S1[
k]
;
:: thesis: S1[k + 1]thus
S1[
k + 1]
:: thesis: verumproof
assume A12:
k + 1
in dom (Sgm X)
;
:: thesis: (Sgm (X \/ Y)) . (k + 1) = (Sgm X) . (k + 1)
assume A13:
(Sgm (X \/ Y)) . (k + 1) <> (Sgm X) . (k + 1)
;
:: thesis: contradiction
A14:
(
(Sgm X) . (k + 1) in rng (Sgm X) &
rng (Sgm X) c= NAT )
by A12, FINSEQ_1:def 4, FUNCT_1:def 5;
then reconsider n =
(Sgm X) . (k + 1) as
Element of
NAT ;
len (Sgm X) <= len (Sgm (X \/ Y))
by A8, NAT_1:12;
then
Seg (len (Sgm X)) c= Seg (len (Sgm (X \/ Y)))
by FINSEQ_1:7;
then
dom (Sgm X) c= Seg (len (Sgm (X \/ Y)))
by FINSEQ_1:def 3;
then A15:
dom (Sgm X) c= dom (Sgm (X \/ Y))
by FINSEQ_1:def 3;
then A16:
k + 1
in dom (Sgm (X \/ Y))
by A12;
A17:
(
(Sgm (X \/ Y)) . (k + 1) in rng (Sgm (X \/ Y)) &
rng (Sgm (X \/ Y)) c= NAT )
by A12, A15, FINSEQ_1:def 4, FUNCT_1:def 5;
then reconsider m =
(Sgm (X \/ Y)) . (k + 1) as
Element of
NAT ;
A18:
(
n in X &
m in X \/ Y )
by A1, A4, A14, A17, FINSEQ_1:def 13;
now per cases
( k in dom (Sgm X) or not k in dom (Sgm X) )
;
suppose A19:
k in dom (Sgm X)
;
:: thesis: contradictionthen
(Sgm X) . k in rng (Sgm X)
by FUNCT_1:def 5;
then reconsider n1 =
(Sgm X) . k as
Element of
NAT by A14;
(Sgm (X \/ Y)) . k in rng (Sgm (X \/ Y))
by A15, A19, FUNCT_1:def 5;
then reconsider m1 =
(Sgm (X \/ Y)) . k as
Element of
NAT by A17;
now per cases
( m < n or n < m )
by A13, XXREAL_0:1;
suppose A20:
m < n
;
:: thesis: contradictionthen
not
m in Y
by A5, A18;
then
m in X
by A18, XBOOLE_0:def 3;
then
m in rng (Sgm X)
by A1, FINSEQ_1:def 13;
then consider x being
set such that A21:
x in dom (Sgm X)
and A22:
(Sgm X) . x = m
by FUNCT_1:def 5;
reconsider x =
x as
Element of
NAT by A21;
(
k in Seg (len (Sgm X)) &
k + 1
in Seg (len (Sgm (X \/ Y))) )
by A16, A19, FINSEQ_1:def 3;
then
( 1
<= k &
k < k + 1 &
k + 1
<= len (Sgm (X \/ Y)) )
by FINSEQ_1:3, XREAL_1:31;
then A23:
n1 < m
by A4, A11, A19, FINSEQ_1:def 13;
( 1
<= x &
k <= len (Sgm X) )
by A19, A21, Th27;
then A24:
k < x
by A1, A22, A23, Th46;
( 1
<= k + 1 &
x <= len (Sgm X) )
by A12, A21, Th27;
then
x < k + 1
by A1, A20, A22, Th46;
hence
contradiction
by A24, NAT_1:13;
:: thesis: verum end; suppose A25:
n < m
;
:: thesis: contradiction
n in X \/ Y
by A18, XBOOLE_0:def 3;
then
n in rng (Sgm (X \/ Y))
by A4, FINSEQ_1:def 13;
then consider x being
set such that A26:
x in dom (Sgm (X \/ Y))
and A27:
(Sgm (X \/ Y)) . x = n
by FUNCT_1:def 5;
reconsider x =
x as
Element of
NAT by A26;
( 1
<= k &
k < k + 1 &
k + 1
<= len (Sgm X) )
by A12, A19, Th27, XREAL_1:31;
then A28:
m1 < n
by A1, A11, A19, FINSEQ_1:def 13;
( 1
<= x &
k <= len (Sgm (X \/ Y)) )
by A15, A19, A26, Th27;
then A29:
k < x
by A1, A2, A3, A27, A28, Th46, XBOOLE_1:8;
( 1
<= k + 1 &
x <= len (Sgm (X \/ Y)) )
by A12, A26, Th27;
then
x < k + 1
by A1, A2, A3, A25, A27, Th46, XBOOLE_1:8;
hence
contradiction
by A29, NAT_1:13;
:: thesis: verum end; hence
contradiction
;
:: thesis: verum end; suppose
not
k in dom (Sgm X)
;
:: thesis: contradictionthen
(
k < 1 or
len (Sgm X) < k )
by Th27;
then
( (
k = 0 or
len (Sgm X) < k ) &
k < k + 1 )
by NAT_1:14, XREAL_1:31;
then A30:
(
k = 0 or (
len (Sgm X) < k + 1 &
k + 1
<= len (Sgm X) ) )
by A12, Th27, XXREAL_0:2;
now per cases
( m < n or n < m )
by A13, XXREAL_0:1;
suppose A31:
m < n
;
:: thesis: contradictionthen
not
m in Y
by A5, A18;
then
m in X
by A18, XBOOLE_0:def 3;
then
m in rng (Sgm X)
by A1, FINSEQ_1:def 13;
then consider x being
set such that A32:
x in dom (Sgm X)
and A33:
(Sgm X) . x = m
by FUNCT_1:def 5;
reconsider x =
x as
Element of
NAT by A32;
( 1
<= k + 1 &
x <= len (Sgm X) )
by A12, A32, Th27;
then
x < k + 1
by A1, A31, A33, Th46;
hence
contradiction
by A30, A32, Th26, NAT_1:14;
:: thesis: verum end; suppose A34:
n < m
;
:: thesis: contradiction
n in X \/ Y
by A18, XBOOLE_0:def 3;
then
n in rng (Sgm (X \/ Y))
by A4, FINSEQ_1:def 13;
then consider x being
set such that A35:
x in dom (Sgm (X \/ Y))
and A36:
(Sgm (X \/ Y)) . x = n
by FUNCT_1:def 5;
reconsider x =
x as
Element of
NAT by A35;
( 1
<= k + 1 &
x <= len (Sgm (X \/ Y)) )
by A12, A35, Th27;
then
x < k + 1
by A1, A2, A3, A34, A36, Th46, XBOOLE_1:8;
hence
contradiction
by A30, A35, Th26, NAT_1:14;
:: thesis: verum end; hence
contradiction
;
:: thesis: verum end;
hence
contradiction
;
:: thesis: verum
end; end;
A37:
for
k being
Element of
NAT holds
S1[
k]
from NAT_1:sch 1(A9, A10);
defpred S2[
Element of
NAT ]
means ( $1
in dom (Sgm Y) implies
(Sgm (X \/ Y)) . ((len (Sgm X)) + $1) = (Sgm Y) . $1 );
A38:
S2[
0 ]
by Th26;
A39:
now let k be
Element of
NAT ;
:: thesis: ( S2[k] implies S2[k + 1] )assume A40:
S2[
k]
;
:: thesis: S2[k + 1]thus
S2[
k + 1]
:: thesis: verumproof
assume A41:
k + 1
in dom (Sgm Y)
;
:: thesis: (Sgm (X \/ Y)) . ((len (Sgm X)) + (k + 1)) = (Sgm Y) . (k + 1)
assume A42:
(Sgm (X \/ Y)) . ((len (Sgm X)) + (k + 1)) <> (Sgm Y) . (k + 1)
;
:: thesis: contradiction
set a =
(len (Sgm X)) + (k + 1);
A43:
(
(Sgm Y) . (k + 1) in rng (Sgm Y) &
rng (Sgm Y) c= NAT )
by A41, FINSEQ_1:def 4, FUNCT_1:def 5;
then reconsider n =
(Sgm Y) . (k + 1) as
Element of
NAT ;
(
len (Sgm X) <= len (Sgm X) &
k + 1
<= len (Sgm Y) )
by A41, Th27;
then A44:
(len (Sgm X)) + (k + 1) <= len (Sgm (X \/ Y))
by A8, XREAL_1:9;
A45:
( 1
<= k + 1 &
k + 1
<= (len (Sgm X)) + (k + 1) )
by NAT_1:12;
then
1
<= (len (Sgm X)) + (k + 1)
by XXREAL_0:2;
then A46:
(len (Sgm X)) + (k + 1) in dom (Sgm (X \/ Y))
by A44, Th27;
then A47:
(
(Sgm (X \/ Y)) . ((len (Sgm X)) + (k + 1)) in rng (Sgm (X \/ Y)) &
rng (Sgm (X \/ Y)) c= NAT )
by FINSEQ_1:def 4, FUNCT_1:def 5;
then reconsider m =
(Sgm (X \/ Y)) . ((len (Sgm X)) + (k + 1)) as
Element of
NAT ;
A48:
(
n in Y &
m in X \/ Y )
by A2, A4, A43, A47, FINSEQ_1:def 13;
A49:
now assume
m in X
;
:: thesis: contradictionthen
m in rng (Sgm X)
by A1, FINSEQ_1:def 13;
then consider x being
set such that A50:
x in dom (Sgm X)
and A51:
(Sgm X) . x = m
by FUNCT_1:def 5;
reconsider x =
x as
Element of
NAT by A50;
A52:
(
(Sgm (X \/ Y)) . x = (Sgm (X \/ Y)) . ((len (Sgm X)) + (k + 1)) &
Sgm (X \/ Y) is
one-to-one )
by A4, A37, A50, A51, Lm1;
( 1
<= x &
x <= len (Sgm X) &
len (Sgm X) <= len (Sgm (X \/ Y)) )
by A8, A50, Th27, NAT_1:12;
then
( 1
<= x &
x <= len (Sgm (X \/ Y)) )
by XXREAL_0:2;
then
x in dom (Sgm (X \/ Y))
by Th27;
then
x = (len (Sgm X)) + (k + 1)
by A46, A52, FUNCT_1:def 8;
then
(len (Sgm X)) + (k + 1) <= (len (Sgm X)) + 0
by A50, Th27;
hence
contradiction
by XREAL_1:31;
:: thesis: verum end;
now per cases
( k in dom (Sgm Y) or not k in dom (Sgm Y) )
;
suppose A53:
k in dom (Sgm Y)
;
:: thesis: contradictionthen
(Sgm Y) . k in rng (Sgm Y)
by FUNCT_1:def 5;
then reconsider n1 =
(Sgm Y) . k as
Element of
NAT by A43;
A54:
( 1
<= k &
k <= len (Sgm Y) &
k <= (len (Sgm X)) + k )
by A53, Th27, NAT_1:12;
then A55:
( 1
<= (len (Sgm X)) + k &
(len (Sgm X)) + k <= len (Sgm (X \/ Y)) )
by A8, XREAL_1:9, XXREAL_0:2;
then
(len (Sgm X)) + k in dom (Sgm (X \/ Y))
by Th27;
then
(Sgm (X \/ Y)) . ((len (Sgm X)) + k) in rng (Sgm (X \/ Y))
by FUNCT_1:def 5;
then reconsider m1 =
(Sgm (X \/ Y)) . ((len (Sgm X)) + k) as
Element of
NAT by A47;
now per cases
( m < n or n < m )
by A42, XXREAL_0:1;
suppose A56:
m < n
;
:: thesis: contradiction
m in Y
by A48, A49, XBOOLE_0:def 3;
then
m in rng (Sgm Y)
by A2, FINSEQ_1:def 13;
then consider x being
set such that A57:
x in dom (Sgm Y)
and A58:
(Sgm Y) . x = m
by FUNCT_1:def 5;
reconsider x =
x as
Element of
NAT by A57;
(len (Sgm X)) + k < ((len (Sgm X)) + k) + 1
by XREAL_1:31;
then A59:
n1 < m
by A4, A40, A44, A53, A55, FINSEQ_1:def 13;
( 1
<= x &
k <= len (Sgm Y) )
by A53, A57, Th27;
then A60:
k < x
by A2, A58, A59, Th46;
( 1
<= k + 1 &
x <= len (Sgm Y) )
by A41, A57, Th27;
then
x < k + 1
by A2, A56, A58, Th46;
hence
contradiction
by A60, NAT_1:13;
:: thesis: verum end; suppose A61:
n < m
;
:: thesis: contradiction
n in X \/ Y
by A48, XBOOLE_0:def 3;
then
n in rng (Sgm (X \/ Y))
by A4, FINSEQ_1:def 13;
then consider x being
set such that A62:
x in dom (Sgm (X \/ Y))
and A63:
(Sgm (X \/ Y)) . x = n
by FUNCT_1:def 5;
reconsider x =
x as
Element of
NAT by A62;
( 1
<= k &
k < k + 1 &
k + 1
<= len (Sgm Y) )
by A41, A53, Th27, XREAL_1:31;
then A64:
m1 < n
by A2, A40, A53, FINSEQ_1:def 13;
( 1
<= x &
(len (Sgm X)) + k <= len (Sgm (X \/ Y)) )
by A8, A54, A62, Th27, XREAL_1:9;
then A65:
(len (Sgm X)) + k < x
by A1, A2, A3, A63, A64, Th46, XBOOLE_1:8;
( 1
<= (len (Sgm X)) + (k + 1) &
x <= len (Sgm (X \/ Y)) )
by A45, A62, Th27, XXREAL_0:2;
then
x < ((len (Sgm X)) + k) + 1
by A1, A2, A3, A61, A63, Th46, XBOOLE_1:8;
hence
contradiction
by A65, NAT_1:13;
:: thesis: verum end; hence
contradiction
;
:: thesis: verum end; suppose
not
k in dom (Sgm Y)
;
:: thesis: contradictionthen
(
k < 1 or
len (Sgm Y) < k )
by Th27;
then
( (
k = 0 or
len (Sgm Y) < k ) &
k < k + 1 )
by NAT_1:14, XREAL_1:31;
then A66:
(
k = 0 or (
len (Sgm Y) < k + 1 &
k + 1
<= len (Sgm Y) ) )
by A41, Th27, XXREAL_0:2;
now per cases
( m < n or n < m )
by A42, XXREAL_0:1;
suppose A67:
m < n
;
:: thesis: contradiction
m in Y
by A48, A49, XBOOLE_0:def 3;
then
m in rng (Sgm Y)
by A2, FINSEQ_1:def 13;
then consider x being
set such that A68:
x in dom (Sgm Y)
and A69:
(Sgm Y) . x = m
by FUNCT_1:def 5;
reconsider x =
x as
Element of
NAT by A68;
( 1
<= k + 1 &
x <= len (Sgm Y) )
by A41, A68, Th27;
then
x < k + 1
by A2, A67, A69, Th46;
hence
contradiction
by A66, A68, Th26, NAT_1:14;
:: thesis: verum end; suppose A70:
n < m
;
:: thesis: contradiction
n in X \/ Y
by A48, XBOOLE_0:def 3;
then
n in rng (Sgm (X \/ Y))
by A4, FINSEQ_1:def 13;
then consider x being
set such that A71:
x in dom (Sgm (X \/ Y))
and A72:
(Sgm (X \/ Y)) . x = n
by FUNCT_1:def 5;
reconsider x =
x as
Element of
NAT by A71;
( 1
<= (len (Sgm X)) + 1 &
x <= len (Sgm (X \/ Y)) )
by A71, Th27, NAT_1:12;
then
x < (len (Sgm X)) + 1
by A1, A2, A3, A66, A70, A72, Th46, XBOOLE_1:8;
then
( 1
<= x &
x <= len (Sgm X) )
by A71, Th27, NAT_1:13;
then
x in dom (Sgm X)
by Th27;
then
(
n = (Sgm X) . x &
(Sgm X) . x in rng (Sgm X) )
by A37, A72, FUNCT_1:def 5;
then
n in X
by A1, FINSEQ_1:def 13;
hence
contradiction
by A5, A48;
:: thesis: verum end; hence
contradiction
;
:: thesis: verum end;
hence
contradiction
;
:: thesis: verum
end; end;
for
k being
Element of
NAT holds
S2[
k]
from NAT_1:sch 1(A38, A39);
hence
Sgm (X \/ Y) = (Sgm X) ^ (Sgm Y)
by A8, A37, Th43;
:: thesis: verum
end;
assume A73:
Sgm (X \/ Y) = (Sgm X) ^ (Sgm Y)
; :: thesis: for m, n being Element of NAT st m in X & n in Y holds
m < n
let m, n be Element of NAT ; :: thesis: ( m in X & n in Y implies m < n )
assume that
A74:
m in X
and
A75:
n in Y
; :: thesis: m < n
m in rng (Sgm X)
by A1, A74, FINSEQ_1:def 13;
then consider x being set such that
A76:
x in dom (Sgm X)
and
A77:
(Sgm X) . x = m
by FUNCT_1:def 5;
reconsider x = x as Element of NAT by A76;
n in rng (Sgm Y)
by A2, A75, FINSEQ_1:def 13;
then consider y being set such that
A78:
y in dom (Sgm Y)
and
A79:
(Sgm Y) . y = n
by FUNCT_1:def 5;
reconsider y = y as Element of NAT by A78;
A80:
( m = (Sgm (X \/ Y)) . x & n = (Sgm (X \/ Y)) . ((len (Sgm X)) + y) )
by A73, A76, A77, A78, A79, FINSEQ_1:def 7;
x in Seg (len (Sgm X))
by A76, FINSEQ_1:def 3;
then A81:
( 1 <= x & x <= len (Sgm X) )
by FINSEQ_1:3;
y <> 0
by A78, Th26;
then A82:
x < (len (Sgm X)) + y
by A81, NAT_1:16, XXREAL_0:2;
y <= len (Sgm Y)
by A78, Th27;
then
(len (Sgm X)) + y <= (len (Sgm X)) + (len (Sgm Y))
by XREAL_1:9;
then
(len (Sgm X)) + y <= len (Sgm (X \/ Y))
by A73, FINSEQ_1:35;
hence
m < n
by A4, A80, A81, A82, FINSEQ_1:def 13; :: thesis: verum