let X, Y be finite natural-membered set ; :: thesis: ( 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) )
:: thesis: ( Sgm0 (X \/ Y) = (Sgm0 X) ^ (Sgm0 Y) implies X <N< Y )proof
assume A40:
X <N< Y
;
:: thesis: Sgm0 (X \/ Y) = (Sgm0 X) ^ (Sgm0 Y)
X /\ Y = {}
then A7:
X misses Y
by XBOOLE_0:def 7;
reconsider X1 =
X,
Y1 =
Y as
finite set ;
A51:
(
0 < len (Sgm0 X) implies
X1 <> {} )
by Th44, CARD_1:47;
A8:
len (Sgm0 (X \/ Y)) =
card (X1 \/ Y1)
by Th44
.=
(card X1) + (card Y1)
by A7, CARD_2:53
.=
(len (Sgm0 X)) + (card Y1)
by Th44
.=
(len (Sgm0 X)) + (len (Sgm0 Y))
by Th44
;
defpred S1[
Element of
NAT ]
means ( $1
in dom (Sgm0 X) implies
(Sgm0 (X \/ Y)) . $1
= (Sgm0 X) . $1 );
A9:
S1[
0 ]
by A40, A51, AE220;
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 (Sgm0 X)
;
:: thesis: (Sgm0 (X \/ Y)) . (k + 1) = (Sgm0 X) . (k + 1)
assume A13:
(Sgm0 (X \/ Y)) . (k + 1) <> (Sgm0 X) . (k + 1)
;
:: thesis: contradiction
A14:
(
(Sgm0 X) . (k + 1) in rng (Sgm0 X) &
rng (Sgm0 X) c= NAT )
by A12, FUNCT_1:def 5, RELAT_1:def 19;
reconsider n =
(Sgm0 X) . (k + 1) as
Element of
NAT by ORDINAL1:def 13;
len (Sgm0 X) <= len (Sgm0 (X \/ Y))
by A8, NAT_1:12;
then A15:
len (Sgm0 X) c= len (Sgm0 (X \/ Y))
by NAT_1:40;
then A17:
(
(Sgm0 (X \/ Y)) . (k + 1) in rng (Sgm0 (X \/ Y)) &
rng (Sgm0 (X \/ Y)) c= NAT )
by A12, FUNCT_1:def 5, RELAT_1:def 19;
reconsider m =
(Sgm0 (X \/ Y)) . (k + 1) as
Element of
NAT by ORDINAL1:def 13;
A18:
(
n in X &
m in X \/ Y )
by A14, A17, AC113;
now per cases
( k in dom (Sgm0 X) or not k in dom (Sgm0 X) )
;
suppose A19:
k in dom (Sgm0 X)
;
:: thesis: contradictionreconsider n1 =
(Sgm0 X) . k as
Element of
NAT by ORDINAL1:def 13;
reconsider m1 =
(Sgm0 (X \/ Y)) . k as
Element of
NAT by ORDINAL1:def 13;
now per cases
( m < n or n < m )
by A13, XXREAL_0:1;
suppose A20:
m < n
;
:: thesis: contradictionthen
not
m in Y
by AE100, A40, A18;
then
m in X
by A18, XBOOLE_0:def 3;
then
m in rng (Sgm0 X)
by AC113;
then consider x being
set such that A21:
x in dom (Sgm0 X)
and A22:
(Sgm0 X) . x = m
by FUNCT_1:def 5;
reconsider x =
x as
Element of
NAT by A21;
(
k < k + 1 &
k + 1
< len (Sgm0 (X \/ Y)) )
by A15, A12, NAT_1:45, XREAL_1:31;
then A23:
n1 < m
by A11, A19, AC113;
k < len (Sgm0 X)
by A19, NAT_1:45;
then A24:
k < x
by A22, A23, Th46;
x < len (Sgm0 X)
by A21, NAT_1:45;
then
x < k + 1
by 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 (Sgm0 (X \/ Y))
by AC113;
then consider x being
set such that A26:
x in dom (Sgm0 (X \/ Y))
and A27:
(Sgm0 (X \/ Y)) . x = n
by FUNCT_1:def 5;
reconsider x =
x as
Element of
NAT by A26;
(
k < k + 1 &
k + 1
< len (Sgm0 X) )
by A12, NAT_1:45, XREAL_1:31;
then A28:
m1 < n
by A11, A19, AC113;
k < len (Sgm0 (X \/ Y))
by A15, A19, NAT_1:45;
then A29:
k < x
by A27, A28, Th46;
x < len (Sgm0 (X \/ Y))
by A26, NAT_1:45;
then
x < k + 1
by A25, A27, Th46;
hence
contradiction
by A29, NAT_1:13;
:: 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 (Sgm0 Y) implies
(Sgm0 (X \/ Y)) . ((len (Sgm0 X)) + $1) = (Sgm0 Y) . $1 );
(
len (Sgm0 Y) > 0 implies
Y <> {} )
by Th44, CARD_1:47;
then A38:
S2[
0 ]
by A40, AE222;
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 (Sgm0 Y)
;
:: thesis: (Sgm0 (X \/ Y)) . ((len (Sgm0 X)) + (k + 1)) = (Sgm0 Y) . (k + 1)
assume A42:
(Sgm0 (X \/ Y)) . ((len (Sgm0 X)) + (k + 1)) <> (Sgm0 Y) . (k + 1)
;
:: thesis: contradiction
set a =
(len (Sgm0 X)) + (k + 1);
A43:
(
(Sgm0 Y) . (k + 1) in rng (Sgm0 Y) &
rng (Sgm0 Y) c= NAT )
by A41, FUNCT_1:def 5, RELAT_1:def 19;
reconsider n =
(Sgm0 Y) . (k + 1) as
Element of
NAT by ORDINAL1:def 13;
k + 1
< len (Sgm0 Y)
by A41, NAT_1:45;
then A44:
(len (Sgm0 X)) + (k + 1) < len (Sgm0 (X \/ Y))
by A8, XREAL_1:8;
A46:
(len (Sgm0 X)) + (k + 1) in dom (Sgm0 (X \/ Y))
by A44, NAT_1:45;
then A47:
(
(Sgm0 (X \/ Y)) . ((len (Sgm0 X)) + (k + 1)) in rng (Sgm0 (X \/ Y)) &
rng (Sgm0 (X \/ Y)) c= NAT )
by FUNCT_1:def 5, RELAT_1:def 19;
reconsider m =
(Sgm0 (X \/ Y)) . ((len (Sgm0 X)) + (k + 1)) as
Element of
NAT by ORDINAL1:def 13;
A48:
(
n in Y &
m in X \/ Y )
by A43, A47, AC113;
now per cases
( k in dom (Sgm0 Y) or not k in dom (Sgm0 Y) )
;
suppose A53:
k in dom (Sgm0 Y)
;
:: thesis: contradictionreconsider n1 =
(Sgm0 Y) . k as
Element of
NAT by ORDINAL1:def 13;
A54:
(
k < len (Sgm0 Y) &
k <= (len (Sgm0 X)) + k )
by A53, NAT_1:12, NAT_1:45;
reconsider m1 =
(Sgm0 (X \/ Y)) . ((len (Sgm0 X)) + k) as
Element of
NAT by ORDINAL1:def 13;
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 (Sgm0 Y)
by AC113;
then consider x being
set such that A57:
x in dom (Sgm0 Y)
and A58:
(Sgm0 Y) . x = m
by FUNCT_1:def 5;
reconsider x =
x as
Element of
NAT by A57;
(len (Sgm0 X)) + k < ((len (Sgm0 X)) + k) + 1
by XREAL_1:31;
then A59:
n1 < m
by A40, A44, A53, AC113;
k < len (Sgm0 Y)
by A53, NAT_1:45;
then A60:
k < x
by A58, A59, Th46;
x < len (Sgm0 Y)
by A57, NAT_1:45;
then
x < k + 1
by 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 (Sgm0 (X \/ Y))
by AC113;
then consider x being
set such that A62:
x in dom (Sgm0 (X \/ Y))
and A63:
(Sgm0 (X \/ Y)) . x = n
by FUNCT_1:def 5;
reconsider x =
x as
Element of
NAT by A62;
(
k < k + 1 &
k + 1
< len (Sgm0 Y) )
by A41, NAT_1:45, XREAL_1:31;
then A64:
m1 < n
by A40, A53, AC113;
(len (Sgm0 X)) + k < len (Sgm0 (X \/ Y))
by A8, A54, XREAL_1:8;
then A65:
(len (Sgm0 X)) + k < x
by A63, A64, Th46;
x < len (Sgm0 (X \/ Y))
by A62, NAT_1:45;
then
x < ((len (Sgm0 X)) + k) + 1
by A61, A63, Th46;
hence
contradiction
by A65, NAT_1:13;
:: 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
Sgm0 (X \/ Y) = (Sgm0 X) ^ (Sgm0 Y)
by A8, A37, AFINSQ_1:def 4;
:: thesis: verum
end;
assume A73:
Sgm0 (X \/ Y) = (Sgm0 X) ^ (Sgm0 Y)
; :: thesis: X <N< Y
let m, n be Nat; :: according to AFINSQ_2:def 6 :: 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 (Sgm0 X)
by A74, AC113;
then consider x being set such that
A76:
x in dom (Sgm0 X)
and
A77:
(Sgm0 X) . x = m
by FUNCT_1:def 5;
reconsider x = x as Element of NAT by A76;
n in rng (Sgm0 Y)
by A75, AC113;
then consider y being set such that
A78:
y in dom (Sgm0 Y)
and
A79:
(Sgm0 Y) . y = n
by FUNCT_1:def 5;
reconsider y = y as Element of NAT by A78;
A80:
( m = (Sgm0 (X \/ Y)) . x & n = (Sgm0 (X \/ Y)) . ((len (Sgm0 X)) + y) )
by A73, A76, A77, A78, A79, AFINSQ_1:def 4;
A81:
x < len (Sgm0 X)
by A76, NAT_1:45;
len (Sgm0 X) <= (len (Sgm0 X)) + y
by NAT_1:12;
then A82:
x < (len (Sgm0 X)) + y
by A81, XXREAL_0:2;
y < len (Sgm0 Y)
by A78, NAT_1:45;
then
(len (Sgm0 X)) + y < (len (Sgm0 X)) + (len (Sgm0 Y))
by XREAL_1:8;
then
(len (Sgm0 X)) + y < len (Sgm0 (X \/ Y))
by A73, AFINSQ_1:20;
hence
m < n
by A80, A82, AC113; :: thesis: verum