set N4 = Necklace 4;
let R be non empty strict RelStr ; :: thesis: ( R in fin_RelStr_sp implies R is N-free )
assume A1:
R in fin_RelStr_sp
; :: thesis: R is N-free
then consider S being strict RelStr such that
A2:
R = S
and
A3:
the carrier of S in FinSETS
by Def4;
assume A4:
R embeds Necklace 4
; :: according to NECKLA_2:def 1 :: thesis: contradiction
defpred S1[ Nat] means ex S being non empty strict RelStr st
( S in fin_RelStr_sp & card the carrier of S = $1 & S embeds Necklace 4 );
reconsider C = the carrier of R as Element of FinSETS by A2, A3;
set k = card C;
A5:
ex i being Nat st S1[i]
A6:
for m being Nat st m <> 0 & S1[m] holds
ex n being Nat st
( n < m & S1[n] )
proof
let m be
Nat;
:: thesis: ( m <> 0 & S1[m] implies ex n being Nat st
( n < m & S1[n] ) )
assume that
m <> 0
and A7:
S1[
m]
;
:: thesis: ex n being Nat st
( n < m & S1[n] )
consider S being non
empty strict RelStr such that A8:
S in fin_RelStr_sp
and A9:
card the
carrier of
S = m
and A10:
S embeds Necklace 4
by A7;
per cases
( S is non empty trivial strict RelStr or ex H1, H2 being strict RelStr st
( the carrier of H1 misses the carrier of H2 & H1 in fin_RelStr_sp & H2 in fin_RelStr_sp & ( S = union_of H1,H2 or S = sum_of H1,H2 ) ) )
by A8, Th6;
suppose A11:
S is non
empty trivial strict RelStr
;
:: thesis: ex n being Nat st
( n < m & S1[n] )consider f being
Function of
(Necklace 4),
S such that A12:
(
f is
one-to-one & ( for
x,
y being
Element of
(Necklace 4) holds
(
[x,y] in the
InternalRel of
(Necklace 4) iff
[(f . x),(f . y)] in the
InternalRel of
S ) ) )
by A10, NECKLACE:def 2;
A13:
the
carrier of
(Necklace 4) = {0 ,1,2,3}
by NECKLACE:2, NECKLACE:21;
then A14:
0 in the
carrier of
(Necklace 4)
by ENUMSET1:def 2;
A15:
1
in the
carrier of
(Necklace 4)
by A13, ENUMSET1:def 2;
(
0 = 0 + 1 or 1
= 0 + 1 )
;
then
[0 ,1] in the
InternalRel of
(Necklace 4)
by A14, A15, NECKLACE:26;
then A16:
[(f . 0 ),(f . 1)] in the
InternalRel of
S
by A12, A14, A15;
then A17:
(
f . 0 in dom the
InternalRel of
S &
f . 1
in rng the
InternalRel of
S )
by RELAT_1:20;
(
dom the
InternalRel of
S c= the
carrier of
S &
rng the
InternalRel of
S c= the
carrier of
S )
by RELSET_1:12;
then
f . 0 = f . 1
by A11, A17, STRUCT_0:def 10;
then
[0 ,0 ] in the
InternalRel of
(Necklace 4)
by A12, A14, A16;
then
(
[0 ,0 ] = [0 ,1] or
[0 ,0 ] = [1,0 ] or
[0 ,0 ] = [1,2] or
[0 ,0 ] = [2,1] or
[0 ,0 ] = [2,3] or
[0 ,0 ] = [3,2] )
by Th2, ENUMSET1:def 4;
hence
ex
n being
Nat st
(
n < m &
S1[
n] )
by ZFMISC_1:33;
:: thesis: verum end; suppose
ex
H1,
H2 being
strict RelStr st
( the
carrier of
H1 misses the
carrier of
H2 &
H1 in fin_RelStr_sp &
H2 in fin_RelStr_sp & (
S = union_of H1,
H2 or
S = sum_of H1,
H2 ) )
;
:: thesis: ex n being Nat st
( n < m & S1[n] )then consider H1,
H2 being
strict RelStr such that A18:
the
carrier of
H1 misses the
carrier of
H2
and A19:
(
H1 in fin_RelStr_sp &
H2 in fin_RelStr_sp )
and A20:
(
S = union_of H1,
H2 or
S = sum_of H1,
H2 )
;
A21:
now assume A22:
S = union_of H1,
H2
;
:: thesis: ex n being Nat st
( n < m & S1[n] )consider f being
Function of
(Necklace 4),
S such that A23:
f is
one-to-one
and A24:
for
x,
y being
Element of
(Necklace 4) holds
(
[x,y] in the
InternalRel of
(Necklace 4) iff
[(f . x),(f . y)] in the
InternalRel of
S )
by A10, NECKLACE:def 2;
the
carrier of
(Necklace 4) = {0 ,1,2,3}
by NECKLACE:2, NECKLACE:21;
then A25:
(
0 in the
carrier of
(Necklace 4) & 1
in the
carrier of
(Necklace 4) & 2
in the
carrier of
(Necklace 4) & 3
in the
carrier of
(Necklace 4) )
by ENUMSET1:def 2;
A26:
[0 ,1] in the
InternalRel of
(Necklace 4)
by Th2, ENUMSET1:def 4;
A27:
[1,0 ] in the
InternalRel of
(Necklace 4)
by Th2, ENUMSET1:def 4;
A28:
[1,2] in the
InternalRel of
(Necklace 4)
by Th2, ENUMSET1:def 4;
A29:
[2,1] in the
InternalRel of
(Necklace 4)
by Th2, ENUMSET1:def 4;
A30:
[2,3] in the
InternalRel of
(Necklace 4)
by Th2, ENUMSET1:def 4;
A31:
[3,2] in the
InternalRel of
(Necklace 4)
by Th2, ENUMSET1:def 4;
A32:
(
dom the
InternalRel of
S c= the
carrier of
S &
rng the
InternalRel of
S c= the
carrier of
S )
by RELSET_1:12;
A33:
[(f . 0 ),(f . 1)] in the
InternalRel of
S
by A24, A25, A26;
A34:
[(f . 1),(f . 0 )] in the
InternalRel of
S
by A24, A25, A27;
(
f . 0 in dom the
InternalRel of
S &
f . 1
in rng the
InternalRel of
S )
by A33, RELAT_1:20;
then A35:
(
f . 0 in the
carrier of
S &
f . 1
in the
carrier of
S )
by A32;
A36:
[(f . 1),(f . 2)] in the
InternalRel of
S
by A24, A25, A28;
A37:
[(f . 2),(f . 1)] in the
InternalRel of
S
by A24, A25, A29;
A38:
[(f . 2),(f . 3)] in the
InternalRel of
S
by A24, A25, A30;
A39:
[(f . 3),(f . 2)] in the
InternalRel of
S
by A24, A25, A31;
A40:
f . 0 in the
carrier of
H1 \/ the
carrier of
H2
by A22, A35, Def2;
per cases
( f . 0 in the carrier of H1 or f . 0 in the carrier of H2 )
by A40, XBOOLE_0:def 3;
suppose A41:
f . 0 in the
carrier of
H1
;
:: thesis: ex n being Nat st
( n < m & S1[n] )A42:
(
dom the
InternalRel of
H1 c= the
carrier of
H1 &
rng the
InternalRel of
H1 c= the
carrier of
H1 )
by RELSET_1:12;
A43:
(
dom the
InternalRel of
H2 c= the
carrier of
H2 &
rng the
InternalRel of
H2 c= the
carrier of
H2 )
by RELSET_1:12;
A44:
[(f . 0 ),(f . 1)] in the
InternalRel of
H1 \/ the
InternalRel of
H2
by A22, A33, Def2;
A45:
[(f . 1),(f . 0 )] in the
InternalRel of
H1 \/ the
InternalRel of
H2
by A22, A34, Def2;
A46:
[(f . 0 ),(f . 1)] in the
InternalRel of
H1
A47:
[(f . 1),(f . 0 )] in the
InternalRel of
H1
A48:
f . 1
in rng the
InternalRel of
H1
by A46, RELAT_1:20;
A49:
[(f . 1),(f . 2)] in the
InternalRel of
H1 \/ the
InternalRel of
H2
by A22, A36, Def2;
A50:
[(f . 2),(f . 1)] in the
InternalRel of
H1 \/ the
InternalRel of
H2
by A22, A37, Def2;
A51:
[(f . 1),(f . 2)] in the
InternalRel of
H1
A52:
[(f . 2),(f . 1)] in the
InternalRel of
H1
A53:
f . 2
in rng the
InternalRel of
H1
by A51, RELAT_1:20;
A54:
[(f . 2),(f . 3)] in the
InternalRel of
H1 \/ the
InternalRel of
H2
by A22, A38, Def2;
A55:
[(f . 3),(f . 2)] in the
InternalRel of
H1 \/ the
InternalRel of
H2
by A22, A39, Def2;
A56:
[(f . 2),(f . 3)] in the
InternalRel of
H1
A57:
[(f . 3),(f . 2)] in the
InternalRel of
H1
A58:
f . 3
in rng the
InternalRel of
H1
by A56, RELAT_1:20;
not
H2 is
empty
by A19, Th4;
then A59:
not the
carrier of
H2 is
empty
;
A60:
dom f = the
carrier of
(Necklace 4)
by FUNCT_2:def 1;
rng f c= the
carrier of
H1
then A62:
f is
Function of the
carrier of
(Necklace 4),the
carrier of
H1
by FUNCT_2:8;
A63:
H1 embeds Necklace 4
proof
for
x,
y being
Element of
(Necklace 4) holds
(
[x,y] in the
InternalRel of
(Necklace 4) iff
[(f . x),(f . y)] in the
InternalRel of
H1 )
proof
let x,
y be
Element of
(Necklace 4);
:: thesis: ( [x,y] in the InternalRel of (Necklace 4) iff [(f . x),(f . y)] in the InternalRel of H1 )
thus
(
[x,y] in the
InternalRel of
(Necklace 4) implies
[(f . x),(f . y)] in the
InternalRel of
H1 )
:: thesis: ( [(f . x),(f . y)] in the InternalRel of H1 implies [x,y] in the InternalRel of (Necklace 4) )proof
assume A64:
[x,y] in the
InternalRel of
(Necklace 4)
;
:: thesis: [(f . x),(f . y)] in the InternalRel of H1
per cases
( [x,y] = [0 ,1] or [x,y] = [1,0 ] or [x,y] = [1,2] or [x,y] = [2,1] or [x,y] = [2,3] or [x,y] = [3,2] )
by A64, Th2, ENUMSET1:def 4;
end;
end;
thus
(
[(f . x),(f . y)] in the
InternalRel of
H1 implies
[x,y] in the
InternalRel of
(Necklace 4) )
:: thesis: verum
end;
hence
H1 embeds Necklace 4
by A23, A62, NECKLACE:def 2;
:: thesis: verum
end; A66:
H1 is non
empty strict RelStr
by A19, Th4;
set cS = the
carrier of
S;
set cH1 = the
carrier of
H1;
set cH2 = the
carrier of
H2;
H1 is
finite
by A19, Th4;
then reconsider cH1 = the
carrier of
H1 as
finite set ;
H2 is
finite
by A19, Th4;
then reconsider cH2 = the
carrier of
H2 as
finite set ;
the
carrier of
S = cH1 \/ cH2
by A22, Def2;
then reconsider cS = the
carrier of
S as
finite set ;
A67:
cH1 <> cS
cS = cH1 \/ cH2
by A22, Def2;
then
cH1 c= cS
by XBOOLE_1:7;
then
cH1 c< cS
by A67, XBOOLE_0:def 8;
then
card cH1 < card cS
by CARD_2:67;
hence
ex
n being
Nat st
(
n < m &
S1[
n] )
by A9, A19, A63, A66;
:: thesis: verum end; suppose A71:
f . 0 in the
carrier of
H2
;
:: thesis: ex n being Nat st
( n < m & S1[n] )A72:
(
dom the
InternalRel of
H2 c= the
carrier of
H2 &
rng the
InternalRel of
H2 c= the
carrier of
H2 )
by RELSET_1:12;
A73:
(
dom the
InternalRel of
H1 c= the
carrier of
H1 &
rng the
InternalRel of
H1 c= the
carrier of
H1 )
by RELSET_1:12;
A74:
[(f . 0 ),(f . 1)] in the
InternalRel of
H1 \/ the
InternalRel of
H2
by A22, A33, Def2;
A75:
[(f . 1),(f . 0 )] in the
InternalRel of
H1 \/ the
InternalRel of
H2
by A22, A34, Def2;
A76:
[(f . 0 ),(f . 1)] in the
InternalRel of
H2
A77:
[(f . 1),(f . 0 )] in the
InternalRel of
H2
A78:
f . 1
in rng the
InternalRel of
H2
by A76, RELAT_1:20;
A79:
[(f . 1),(f . 2)] in the
InternalRel of
H1 \/ the
InternalRel of
H2
by A22, A36, Def2;
A80:
[(f . 2),(f . 1)] in the
InternalRel of
H1 \/ the
InternalRel of
H2
by A22, A37, Def2;
A81:
[(f . 1),(f . 2)] in the
InternalRel of
H2
A82:
[(f . 2),(f . 1)] in the
InternalRel of
H2
A83:
f . 2
in rng the
InternalRel of
H2
by A81, RELAT_1:20;
A84:
[(f . 2),(f . 3)] in the
InternalRel of
H1 \/ the
InternalRel of
H2
by A22, A38, Def2;
A85:
[(f . 3),(f . 2)] in the
InternalRel of
H1 \/ the
InternalRel of
H2
by A22, A39, Def2;
A86:
[(f . 2),(f . 3)] in the
InternalRel of
H2
A87:
[(f . 3),(f . 2)] in the
InternalRel of
H2
A88:
f . 3
in rng the
InternalRel of
H2
by A86, RELAT_1:20;
not
H1 is
empty
by A19, Th4;
then A89:
not the
carrier of
H1 is
empty
;
A90:
dom f = the
carrier of
(Necklace 4)
by FUNCT_2:def 1;
rng f c= the
carrier of
H2
then A92:
f is
Function of the
carrier of
(Necklace 4),the
carrier of
H2
by FUNCT_2:8;
A93:
H2 embeds Necklace 4
proof
for
x,
y being
Element of
(Necklace 4) holds
(
[x,y] in the
InternalRel of
(Necklace 4) iff
[(f . x),(f . y)] in the
InternalRel of
H2 )
proof
let x,
y be
Element of
(Necklace 4);
:: thesis: ( [x,y] in the InternalRel of (Necklace 4) iff [(f . x),(f . y)] in the InternalRel of H2 )
thus
(
[x,y] in the
InternalRel of
(Necklace 4) implies
[(f . x),(f . y)] in the
InternalRel of
H2 )
:: thesis: ( [(f . x),(f . y)] in the InternalRel of H2 implies [x,y] in the InternalRel of (Necklace 4) )proof
assume A94:
[x,y] in the
InternalRel of
(Necklace 4)
;
:: thesis: [(f . x),(f . y)] in the InternalRel of H2
per cases
( [x,y] = [0 ,1] or [x,y] = [1,0 ] or [x,y] = [1,2] or [x,y] = [2,1] or [x,y] = [2,3] or [x,y] = [3,2] )
by A94, Th2, ENUMSET1:def 4;
end;
end;
thus
(
[(f . x),(f . y)] in the
InternalRel of
H2 implies
[x,y] in the
InternalRel of
(Necklace 4) )
:: thesis: verum
end;
hence
H2 embeds Necklace 4
by A23, A92, NECKLACE:def 2;
:: thesis: verum
end; A96:
H2 is non
empty strict RelStr
by A19, Th4;
set cS = the
carrier of
S;
set cH1 = the
carrier of
H1;
set cH2 = the
carrier of
H2;
H1 is
finite
by A19, Th4;
then reconsider cH1 = the
carrier of
H1 as
finite set ;
H2 is
finite
by A19, Th4;
then reconsider cH2 = the
carrier of
H2 as
finite set ;
the
carrier of
S = cH1 \/ cH2
by A22, Def2;
then reconsider cS = the
carrier of
S as
finite set ;
A97:
cH2 <> cS
cS = cH1 \/ cH2
by A22, Def2;
then
cH2 c= cS
by XBOOLE_1:7;
then
cH2 c< cS
by A97, XBOOLE_0:def 8;
then
card cH2 < card cS
by CARD_2:67;
hence
ex
n being
Nat st
(
n < m &
S1[
n] )
by A9, A19, A93, A96;
:: thesis: verum end; end; now assume A101:
S = sum_of H1,
H2
;
:: thesis: ex n being Nat st
( n < m & S1[n] )consider f being
Function of
(Necklace 4),
S such that A102:
f is
one-to-one
and A103:
for
x,
y being
Element of
(Necklace 4) holds
(
[x,y] in the
InternalRel of
(Necklace 4) iff
[(f . x),(f . y)] in the
InternalRel of
S )
by A10, NECKLACE:def 2;
the
carrier of
(Necklace 4) = {0 ,1,2,3}
by NECKLACE:2, NECKLACE:21;
then A104:
(
0 in the
carrier of
(Necklace 4) & 1
in the
carrier of
(Necklace 4) & 2
in the
carrier of
(Necklace 4) & 3
in the
carrier of
(Necklace 4) )
by ENUMSET1:def 2;
set A = the
InternalRel of
H1;
set B = the
InternalRel of
H2;
set C =
[:the carrier of H1,the carrier of H2:];
set D =
[:the carrier of H2,the carrier of H1:];
set cH1 = the
carrier of
H1;
set cH2 = the
carrier of
H2;
set cS = the
carrier of
S;
A105:
[0 ,1] in the
InternalRel of
(Necklace 4)
by Th2, ENUMSET1:def 4;
A106:
[1,0 ] in the
InternalRel of
(Necklace 4)
by Th2, ENUMSET1:def 4;
A107:
[1,2] in the
InternalRel of
(Necklace 4)
by Th2, ENUMSET1:def 4;
A108:
[2,1] in the
InternalRel of
(Necklace 4)
by Th2, ENUMSET1:def 4;
A109:
[2,3] in the
InternalRel of
(Necklace 4)
by Th2, ENUMSET1:def 4;
A110:
[3,2] in the
InternalRel of
(Necklace 4)
by Th2, ENUMSET1:def 4;
A111:
(
dom the
InternalRel of
S c= the
carrier of
S &
rng the
InternalRel of
S c= the
carrier of
S )
by RELSET_1:12;
A112:
[(f . 0 ),(f . 1)] in the
InternalRel of
S
by A103, A104, A105;
A113:
[(f . 1),(f . 0 )] in the
InternalRel of
S
by A103, A104, A106;
(
f . 0 in dom the
InternalRel of
S &
f . 1
in rng the
InternalRel of
S )
by A112, RELAT_1:20;
then A114:
(
f . 0 in the
carrier of
S &
f . 1
in the
carrier of
S )
by A111;
then A115:
f . 1
in the
carrier of
H1 \/ the
carrier of
H2
by A101, Def3;
A116:
[(f . 1),(f . 2)] in the
InternalRel of
S
by A103, A104, A107;
then
(
f . 1
in dom the
InternalRel of
S &
f . 2
in rng the
InternalRel of
S )
by RELAT_1:20;
then
(
f . 1
in the
carrier of
S &
f . 2
in the
carrier of
S )
by A111;
then A117:
f . 2
in the
carrier of
H1 \/ the
carrier of
H2
by A101, Def3;
A118:
[(f . 2),(f . 1)] in the
InternalRel of
S
by A103, A104, A108;
A119:
[(f . 2),(f . 3)] in the
InternalRel of
S
by A103, A104, A109;
then
(
f . 2
in dom the
InternalRel of
S &
f . 3
in rng the
InternalRel of
S )
by RELAT_1:20;
then
f . 3
in the
carrier of
S
by A111;
then A120:
f . 3
in the
carrier of
H1 \/ the
carrier of
H2
by A101, Def3;
A121:
[(f . 3),(f . 2)] in the
InternalRel of
S
by A103, A104, A110;
A122:
f . 0 in the
carrier of
H1 \/ the
carrier of
H2
by A101, A114, Def3;
A123:
(
dom the
InternalRel of
H2 c= the
carrier of
H2 &
rng the
InternalRel of
H2 c= the
carrier of
H2 )
by RELSET_1:12;
A124:
(
dom the
InternalRel of
H1 c= the
carrier of
H1 &
rng the
InternalRel of
H1 c= the
carrier of
H1 )
by RELSET_1:12;
A125:
not
[0 ,2] in the
InternalRel of
(Necklace 4)
proof
assume A126:
[0 ,2] in the
InternalRel of
(Necklace 4)
;
:: thesis: contradiction
per cases
( [0 ,2] = [0 ,1] or [0 ,2] = [1,2] or [0 ,2] = [2,3] or [0 ,2] = [3,2] or [0 ,2] = [2,1] or [0 ,2] = [1,0 ] )
by A126, Th2, ENUMSET1:def 4;
end;
end; A127:
not
[0 ,3] in the
InternalRel of
(Necklace 4)
proof
assume A128:
[0 ,3] in the
InternalRel of
(Necklace 4)
;
:: thesis: contradiction
per cases
( [0 ,3] = [0 ,1] or [0 ,3] = [1,2] or [0 ,3] = [2,3] or [0 ,3] = [3,2] or [0 ,3] = [2,1] or [0 ,3] = [1,0 ] )
by A128, Th2, ENUMSET1:def 4;
end;
end; A129:
not
[1,3] in the
InternalRel of
(Necklace 4)
proof
assume A130:
[1,3] in the
InternalRel of
(Necklace 4)
;
:: thesis: contradiction
per cases
( [1,3] = [0 ,1] or [1,3] = [1,2] or [1,3] = [2,3] or [1,3] = [3,2] or [1,3] = [2,1] or [1,3] = [1,0 ] )
by A130, Th2, ENUMSET1:def 4;
end;
end; A131:
( the
InternalRel of
H1 c= the
InternalRel of
S & the
InternalRel of
H2 c= the
InternalRel of
S &
[:the carrier of H1,the carrier of H2:] c= the
InternalRel of
S &
[:the carrier of H2,the carrier of H1:] c= the
InternalRel of
S )
proof
A132:
the
InternalRel of
H1 c= the
InternalRel of
S
A135:
the
InternalRel of
H2 c= the
InternalRel of
S
A138:
[:the carrier of H1,the carrier of H2:] c= the
InternalRel of
S
[:the carrier of H2,the carrier of H1:] c= the
InternalRel of
S
proof
let x be
set ;
:: according to TARSKI:def 3 :: thesis: ( not x in [:the carrier of H2,the carrier of H1:] or x in the InternalRel of S )
assume
x in [:the carrier of H2,the carrier of H1:]
;
:: thesis: x in the InternalRel of S
then A140:
x in (the InternalRel of H2 \/ [:the carrier of H1,the carrier of H2:]) \/ [:the carrier of H2,the carrier of H1:]
by XBOOLE_0:def 3;
(the InternalRel of H2 \/ [:the carrier of H1,the carrier of H2:]) \/ [:the carrier of H2,the carrier of H1:] c= the
InternalRel of
H1 \/ ((the InternalRel of H2 \/ [:the carrier of H1,the carrier of H2:]) \/ [:the carrier of H2,the carrier of H1:])
by XBOOLE_1:7;
then
(the InternalRel of H2 \/ [:the carrier of H1,the carrier of H2:]) \/ [:the carrier of H2,the carrier of H1:] c= the
InternalRel of
H1 \/ (the InternalRel of H2 \/ ([:the carrier of H1,the carrier of H2:] \/ [:the carrier of H2,the carrier of H1:]))
by XBOOLE_1:4;
then
(the InternalRel of H2 \/ [:the carrier of H1,the carrier of H2:]) \/ [:the carrier of H2,the carrier of H1:] c= (the InternalRel of H1 \/ the InternalRel of H2) \/ ([:the carrier of H1,the carrier of H2:] \/ [:the carrier of H2,the carrier of H1:])
by XBOOLE_1:4;
then
(the InternalRel of H2 \/ [:the carrier of H1,the carrier of H2:]) \/ [:the carrier of H2,the carrier of H1:] c= ((the InternalRel of H1 \/ the InternalRel of H2) \/ [:the carrier of H1,the carrier of H2:]) \/ [:the carrier of H2,the carrier of H1:]
by XBOOLE_1:4;
then
(the InternalRel of H2 \/ [:the carrier of H1,the carrier of H2:]) \/ [:the carrier of H2,the carrier of H1:] c= the
InternalRel of
S
by A101, Def3;
hence
x in the
InternalRel of
S
by A140;
:: thesis: verum
end;
hence
( the
InternalRel of
H1 c= the
InternalRel of
S & the
InternalRel of
H2 c= the
InternalRel of
S &
[:the carrier of H1,the carrier of H2:] c= the
InternalRel of
S &
[:the carrier of H2,the carrier of H1:] c= the
InternalRel of
S )
by A132, A135, A138;
:: thesis: verum
end; per cases
( f . 0 in the carrier of H1 or f . 0 in the carrier of H2 )
by A122, XBOOLE_0:def 3;
suppose A141:
f . 0 in the
carrier of
H1
;
:: thesis: ex n being Nat st
( n < m & S1[n] )A142:
f . 2
in the
carrier of
H1
A143:
f . 3
in the
carrier of
H1
A144:
f . 1
in the
carrier of
H1
set x1 =
[(f . 0 ),(f . 1)];
set x2 =
[(f . 1),(f . 2)];
set x3 =
[(f . 2),(f . 3)];
set x4 =
[(f . 1),(f . 0 )];
set x5 =
[(f . 2),(f . 1)];
set x6 =
[(f . 3),(f . 2)];
[(f . 0 ),(f . 1)] in ((the InternalRel of H1 \/ the InternalRel of H2) \/ [:the carrier of H1,the carrier of H2:]) \/ [:the carrier of H2,the carrier of H1:]
by A101, A112, Def3;
then
(
[(f . 0 ),(f . 1)] in (the InternalRel of H1 \/ the InternalRel of H2) \/ [:the carrier of H1,the carrier of H2:] or
[(f . 0 ),(f . 1)] in [:the carrier of H2,the carrier of H1:] )
by XBOOLE_0:def 3;
then A145:
(
[(f . 0 ),(f . 1)] in the
InternalRel of
H1 \/ the
InternalRel of
H2 or
[(f . 0 ),(f . 1)] in [:the carrier of H1,the carrier of H2:] or
[(f . 0 ),(f . 1)] in [:the carrier of H2,the carrier of H1:] )
by XBOOLE_0:def 3;
A146:
[(f . 0 ),(f . 1)] in the
InternalRel of
H1
[(f . 1),(f . 0 )] in ((the InternalRel of H1 \/ the InternalRel of H2) \/ [:the carrier of H1,the carrier of H2:]) \/ [:the carrier of H2,the carrier of H1:]
by A101, A113, Def3;
then
(
[(f . 1),(f . 0 )] in (the InternalRel of H1 \/ the InternalRel of H2) \/ [:the carrier of H1,the carrier of H2:] or
[(f . 1),(f . 0 )] in [:the carrier of H2,the carrier of H1:] )
by XBOOLE_0:def 3;
then A149:
(
[(f . 1),(f . 0 )] in the
InternalRel of
H1 \/ the
InternalRel of
H2 or
[(f . 1),(f . 0 )] in [:the carrier of H1,the carrier of H2:] or
[(f . 1),(f . 0 )] in [:the carrier of H2,the carrier of H1:] )
by XBOOLE_0:def 3;
A150:
[(f . 1),(f . 0 )] in the
InternalRel of
H1
[(f . 1),(f . 2)] in ((the InternalRel of H1 \/ the InternalRel of H2) \/ [:the carrier of H1,the carrier of H2:]) \/ [:the carrier of H2,the carrier of H1:]
by A101, A116, Def3;
then
(
[(f . 1),(f . 2)] in (the InternalRel of H1 \/ the InternalRel of H2) \/ [:the carrier of H1,the carrier of H2:] or
[(f . 1),(f . 2)] in [:the carrier of H2,the carrier of H1:] )
by XBOOLE_0:def 3;
then A153:
(
[(f . 1),(f . 2)] in the
InternalRel of
H1 \/ the
InternalRel of
H2 or
[(f . 1),(f . 2)] in [:the carrier of H1,the carrier of H2:] or
[(f . 1),(f . 2)] in [:the carrier of H2,the carrier of H1:] )
by XBOOLE_0:def 3;
A154:
[(f . 1),(f . 2)] in the
InternalRel of
H1
[(f . 2),(f . 1)] in ((the InternalRel of H1 \/ the InternalRel of H2) \/ [:the carrier of H1,the carrier of H2:]) \/ [:the carrier of H2,the carrier of H1:]
by A101, A118, Def3;
then
(
[(f . 2),(f . 1)] in (the InternalRel of H1 \/ the InternalRel of H2) \/ [:the carrier of H1,the carrier of H2:] or
[(f . 2),(f . 1)] in [:the carrier of H2,the carrier of H1:] )
by XBOOLE_0:def 3;
then A157:
(
[(f . 2),(f . 1)] in the
InternalRel of
H1 \/ the
InternalRel of
H2 or
[(f . 2),(f . 1)] in [:the carrier of H1,the carrier of H2:] or
[(f . 2),(f . 1)] in [:the carrier of H2,the carrier of H1:] )
by XBOOLE_0:def 3;
A158:
[(f . 2),(f . 1)] in the
InternalRel of
H1
[(f . 2),(f . 3)] in ((the InternalRel of H1 \/ the InternalRel of H2) \/ [:the carrier of H1,the carrier of H2:]) \/ [:the carrier of H2,the carrier of H1:]
by A101, A119, Def3;
then
(
[(f . 2),(f . 3)] in (the InternalRel of H1 \/ the InternalRel of H2) \/ [:the carrier of H1,the carrier of H2:] or
[(f . 2),(f . 3)] in [:the carrier of H2,the carrier of H1:] )
by XBOOLE_0:def 3;
then A161:
(
[(f . 2),(f . 3)] in the
InternalRel of
H1 \/ the
InternalRel of
H2 or
[(f . 2),(f . 3)] in [:the carrier of H1,the carrier of H2:] or
[(f . 2),(f . 3)] in [:the carrier of H2,the carrier of H1:] )
by XBOOLE_0:def 3;
A162:
[(f . 2),(f . 3)] in the
InternalRel of
H1
[(f . 3),(f . 2)] in ((the InternalRel of H1 \/ the InternalRel of H2) \/ [:the carrier of H1,the carrier of H2:]) \/ [:the carrier of H2,the carrier of H1:]
by A101, A121, Def3;
then
(
[(f . 3),(f . 2)] in (the InternalRel of H1 \/ the InternalRel of H2) \/ [:the carrier of H1,the carrier of H2:] or
[(f . 3),(f . 2)] in [:the carrier of H2,the carrier of H1:] )
by XBOOLE_0:def 3;
then A165:
(
[(f . 3),(f . 2)] in the
InternalRel of
H1 \/ the
InternalRel of
H2 or
[(f . 3),(f . 2)] in [:the carrier of H1,the carrier of H2:] or
[(f . 3),(f . 2)] in [:the carrier of H2,the carrier of H1:] )
by XBOOLE_0:def 3;
A166:
[(f . 3),(f . 2)] in the
InternalRel of
H1
not
H2 is
empty
by A19, Th4;
then A169:
not the
carrier of
H2 is
empty
;
A170:
dom f = the
carrier of
(Necklace 4)
by FUNCT_2:def 1;
rng f c= the
carrier of
H1
then A172:
f is
Function of the
carrier of
(Necklace 4),the
carrier of
H1
by FUNCT_2:8;
A173:
H1 embeds Necklace 4
proof
for
x,
y being
Element of
(Necklace 4) holds
(
[x,y] in the
InternalRel of
(Necklace 4) iff
[(f . x),(f . y)] in the
InternalRel of
H1 )
proof
let x,
y be
Element of
(Necklace 4);
:: thesis: ( [x,y] in the InternalRel of (Necklace 4) iff [(f . x),(f . y)] in the InternalRel of H1 )
thus
(
[x,y] in the
InternalRel of
(Necklace 4) implies
[(f . x),(f . y)] in the
InternalRel of
H1 )
:: thesis: ( [(f . x),(f . y)] in the InternalRel of H1 implies [x,y] in the InternalRel of (Necklace 4) )proof
assume A174:
[x,y] in the
InternalRel of
(Necklace 4)
;
:: thesis: [(f . x),(f . y)] in the InternalRel of H1
per cases
( [x,y] = [0 ,1] or [x,y] = [1,0 ] or [x,y] = [1,2] or [x,y] = [2,1] or [x,y] = [2,3] or [x,y] = [3,2] )
by A174, Th2, ENUMSET1:def 4;
end;
end;
thus
(
[(f . x),(f . y)] in the
InternalRel of
H1 implies
[x,y] in the
InternalRel of
(Necklace 4) )
:: thesis: verumproof
assume A175:
[(f . x),(f . y)] in the
InternalRel of
H1
;
:: thesis: [x,y] in the InternalRel of (Necklace 4)
(
[(f . x),(f . y)] in the
InternalRel of
S implies
[x,y] in the
InternalRel of
(Necklace 4) )
by A103;
then
(
[(f . x),(f . y)] in ((the InternalRel of H1 \/ the InternalRel of H2) \/ [:the carrier of H1,the carrier of H2:]) \/ [:the carrier of H2,the carrier of H1:] implies
[x,y] in the
InternalRel of
(Necklace 4) )
by A101, Def3;
then
(
[(f . x),(f . y)] in (the InternalRel of H1 \/ the InternalRel of H2) \/ ([:the carrier of H1,the carrier of H2:] \/ [:the carrier of H2,the carrier of H1:]) implies
[x,y] in the
InternalRel of
(Necklace 4) )
by XBOOLE_1:4;
then
(
[(f . x),(f . y)] in the
InternalRel of
H1 \/ (the InternalRel of H2 \/ ([:the carrier of H1,the carrier of H2:] \/ [:the carrier of H2,the carrier of H1:])) implies
[x,y] in the
InternalRel of
(Necklace 4) )
by XBOOLE_1:4;
hence
[x,y] in the
InternalRel of
(Necklace 4)
by A175, XBOOLE_0:def 3;
:: thesis: verum
end;
end;
hence
H1 embeds Necklace 4
by A102, A172, NECKLACE:def 2;
:: thesis: verum
end; A176:
H1 is non
empty strict RelStr
by A19, Th4;
H1 is
finite
by A19, Th4;
then reconsider cH1 = the
carrier of
H1 as
finite set ;
H2 is
finite
by A19, Th4;
then reconsider cH2 = the
carrier of
H2 as
finite set ;
the
carrier of
S = cH1 \/ cH2
by A101, Def3;
then reconsider cS = the
carrier of
S as
finite set ;
A177:
cH1 <> cS
cS = cH1 \/ cH2
by A101, Def3;
then
cH1 c= cS
by XBOOLE_1:7;
then
cH1 c< cS
by A177, XBOOLE_0:def 8;
then
card cH1 < card cS
by CARD_2:67;
hence
ex
n being
Nat st
(
n < m &
S1[
n] )
by A9, A19, A173, A176;
:: thesis: verum end; suppose A181:
f . 0 in the
carrier of
H2
;
:: thesis: ex n being Nat st
( n < m & S1[n] )A182:
f . 2
in the
carrier of
H2
A183:
f . 3
in the
carrier of
H2
A184:
f . 1
in the
carrier of
H2
set x1 =
[(f . 0 ),(f . 1)];
set x2 =
[(f . 1),(f . 2)];
set x3 =
[(f . 2),(f . 3)];
set x4 =
[(f . 1),(f . 0 )];
set x5 =
[(f . 2),(f . 1)];
set x6 =
[(f . 3),(f . 2)];
[(f . 0 ),(f . 1)] in ((the InternalRel of H1 \/ the InternalRel of H2) \/ [:the carrier of H1,the carrier of H2:]) \/ [:the carrier of H2,the carrier of H1:]
by A101, A112, Def3;
then
(
[(f . 0 ),(f . 1)] in (the InternalRel of H1 \/ the InternalRel of H2) \/ [:the carrier of H1,the carrier of H2:] or
[(f . 0 ),(f . 1)] in [:the carrier of H2,the carrier of H1:] )
by XBOOLE_0:def 3;
then A185:
(
[(f . 0 ),(f . 1)] in the
InternalRel of
H1 \/ the
InternalRel of
H2 or
[(f . 0 ),(f . 1)] in [:the carrier of H1,the carrier of H2:] or
[(f . 0 ),(f . 1)] in [:the carrier of H2,the carrier of H1:] )
by XBOOLE_0:def 3;
A186:
[(f . 0 ),(f . 1)] in the
InternalRel of
H2
[(f . 1),(f . 0 )] in ((the InternalRel of H1 \/ the InternalRel of H2) \/ [:the carrier of H1,the carrier of H2:]) \/ [:the carrier of H2,the carrier of H1:]
by A101, A113, Def3;
then
(
[(f . 1),(f . 0 )] in (the InternalRel of H1 \/ the InternalRel of H2) \/ [:the carrier of H1,the carrier of H2:] or
[(f . 1),(f . 0 )] in [:the carrier of H2,the carrier of H1:] )
by XBOOLE_0:def 3;
then A189:
(
[(f . 1),(f . 0 )] in the
InternalRel of
H1 \/ the
InternalRel of
H2 or
[(f . 1),(f . 0 )] in [:the carrier of H1,the carrier of H2:] or
[(f . 1),(f . 0 )] in [:the carrier of H2,the carrier of H1:] )
by XBOOLE_0:def 3;
A190:
[(f . 1),(f . 0 )] in the
InternalRel of
H2
[(f . 1),(f . 2)] in ((the InternalRel of H1 \/ the InternalRel of H2) \/ [:the carrier of H1,the carrier of H2:]) \/ [:the carrier of H2,the carrier of H1:]
by A101, A116, Def3;
then
(
[(f . 1),(f . 2)] in (the InternalRel of H1 \/ the InternalRel of H2) \/ [:the carrier of H1,the carrier of H2:] or
[(f . 1),(f . 2)] in [:the carrier of H2,the carrier of H1:] )
by XBOOLE_0:def 3;
then A193:
(
[(f . 1),(f . 2)] in the
InternalRel of
H1 \/ the
InternalRel of
H2 or
[(f . 1),(f . 2)] in [:the carrier of H1,the carrier of H2:] or
[(f . 1),(f . 2)] in [:the carrier of H2,the carrier of H1:] )
by XBOOLE_0:def 3;
A194:
[(f . 1),(f . 2)] in the
InternalRel of
H2
[(f . 2),(f . 1)] in ((the InternalRel of H1 \/ the InternalRel of H2) \/ [:the carrier of H1,the carrier of H2:]) \/ [:the carrier of H2,the carrier of H1:]
by A101, A118, Def3;
then
(
[(f . 2),(f . 1)] in (the InternalRel of H1 \/ the InternalRel of H2) \/ [:the carrier of H1,the carrier of H2:] or
[(f . 2),(f . 1)] in [:the carrier of H2,the carrier of H1:] )
by XBOOLE_0:def 3;
then A197:
(
[(f . 2),(f . 1)] in the
InternalRel of
H1 \/ the
InternalRel of
H2 or
[(f . 2),(f . 1)] in [:the carrier of H1,the carrier of H2:] or
[(f . 2),(f . 1)] in [:the carrier of H2,the carrier of H1:] )
by XBOOLE_0:def 3;
A198:
[(f . 2),(f . 1)] in the
InternalRel of
H2
[(f . 2),(f . 3)] in ((the InternalRel of H1 \/ the InternalRel of H2) \/ [:the carrier of H1,the carrier of H2:]) \/ [:the carrier of H2,the carrier of H1:]
by A101, A119, Def3;
then
(
[(f . 2),(f . 3)] in (the InternalRel of H1 \/ the InternalRel of H2) \/ [:the carrier of H1,the carrier of H2:] or
[(f . 2),(f . 3)] in [:the carrier of H2,the carrier of H1:] )
by XBOOLE_0:def 3;
then A201:
(
[(f . 2),(f . 3)] in the
InternalRel of
H1 \/ the
InternalRel of
H2 or
[(f . 2),(f . 3)] in [:the carrier of H1,the carrier of H2:] or
[(f . 2),(f . 3)] in [:the carrier of H2,the carrier of H1:] )
by XBOOLE_0:def 3;
A202:
[(f . 2),(f . 3)] in the
InternalRel of
H2
[(f . 3),(f . 2)] in ((the InternalRel of H1 \/ the InternalRel of H2) \/ [:the carrier of H1,the carrier of H2:]) \/ [:the carrier of H2,the carrier of H1:]
by A101, A121, Def3;
then
(
[(f . 3),(f . 2)] in (the InternalRel of H1 \/ the InternalRel of H2) \/ [:the carrier of H1,the carrier of H2:] or
[(f . 3),(f . 2)] in [:the carrier of H2,the carrier of H1:] )
by XBOOLE_0:def 3;
then A205:
(
[(f . 3),(f . 2)] in the
InternalRel of
H1 \/ the
InternalRel of
H2 or
[(f . 3),(f . 2)] in [:the carrier of H1,the carrier of H2:] or
[(f . 3),(f . 2)] in [:the carrier of H2,the carrier of H1:] )
by XBOOLE_0:def 3;
A206:
[(f . 3),(f . 2)] in the
InternalRel of
H2
not
H1 is
empty
by A19, Th4;
then A209:
not the
carrier of
H1 is
empty
;
A210:
dom f = the
carrier of
(Necklace 4)
by FUNCT_2:def 1;
rng f c= the
carrier of
H2
then A212:
f is
Function of the
carrier of
(Necklace 4),the
carrier of
H2
by FUNCT_2:8;
A213:
H2 embeds Necklace 4
proof
for
x,
y being
Element of
(Necklace 4) holds
(
[x,y] in the
InternalRel of
(Necklace 4) iff
[(f . x),(f . y)] in the
InternalRel of
H2 )
proof
let x,
y be
Element of
(Necklace 4);
:: thesis: ( [x,y] in the InternalRel of (Necklace 4) iff [(f . x),(f . y)] in the InternalRel of H2 )
thus
(
[x,y] in the
InternalRel of
(Necklace 4) implies
[(f . x),(f . y)] in the
InternalRel of
H2 )
:: thesis: ( [(f . x),(f . y)] in the InternalRel of H2 implies [x,y] in the InternalRel of (Necklace 4) )proof
assume A214:
[x,y] in the
InternalRel of
(Necklace 4)
;
:: thesis: [(f . x),(f . y)] in the InternalRel of H2
per cases
( [x,y] = [0 ,1] or [x,y] = [1,0 ] or [x,y] = [1,2] or [x,y] = [2,1] or [x,y] = [2,3] or [x,y] = [3,2] )
by A214, Th2, ENUMSET1:def 4;
end;
end;
thus
(
[(f . x),(f . y)] in the
InternalRel of
H2 implies
[x,y] in the
InternalRel of
(Necklace 4) )
:: thesis: verumproof
assume A215:
[(f . x),(f . y)] in the
InternalRel of
H2
;
:: thesis: [x,y] in the InternalRel of (Necklace 4)
(
[(f . x),(f . y)] in the
InternalRel of
S implies
[x,y] in the
InternalRel of
(Necklace 4) )
by A103;
then
(
[(f . x),(f . y)] in ((the InternalRel of H1 \/ the InternalRel of H2) \/ [:the carrier of H1,the carrier of H2:]) \/ [:the carrier of H2,the carrier of H1:] implies
[x,y] in the
InternalRel of
(Necklace 4) )
by A101, Def3;
then
(
[(f . x),(f . y)] in (the InternalRel of H1 \/ the InternalRel of H2) \/ ([:the carrier of H1,the carrier of H2:] \/ [:the carrier of H2,the carrier of H1:]) implies
[x,y] in the
InternalRel of
(Necklace 4) )
by XBOOLE_1:4;
then
(
[(f . x),(f . y)] in the
InternalRel of
H2 \/ (the InternalRel of H1 \/ ([:the carrier of H1,the carrier of H2:] \/ [:the carrier of H2,the carrier of H1:])) implies
[x,y] in the
InternalRel of
(Necklace 4) )
by XBOOLE_1:4;
hence
[x,y] in the
InternalRel of
(Necklace 4)
by A215, XBOOLE_0:def 3;
:: thesis: verum
end;
end;
hence
H2 embeds Necklace 4
by A102, A212, NECKLACE:def 2;
:: thesis: verum
end; A216:
H2 is non
empty strict RelStr
by A19, Th4;
H1 is
finite
by A19, Th4;
then reconsider cH1 = the
carrier of
H1 as
finite set ;
H2 is
finite
by A19, Th4;
then reconsider cH2 = the
carrier of
H2 as
finite set ;
the
carrier of
S = cH1 \/ cH2
by A101, Def3;
then reconsider cS = the
carrier of
S as
finite set ;
A217:
cH2 <> cS
cS = cH1 \/ cH2
by A101, Def3;
then
cH2 c= cS
by XBOOLE_1:7;
then
cH2 c< cS
by A217, XBOOLE_0:def 8;
then
card cH2 < card cS
by CARD_2:67;
hence
ex
n being
Nat st
(
n < m &
S1[
n] )
by A9, A19, A213, A216;
:: thesis: verum end; end; hence
ex
n being
Nat st
(
n < m &
S1[
n] )
by A20, A21;
:: thesis: verum end;
end;
S1[ 0 ]
from NAT_1:sch 7(A5, A6);
hence
contradiction
; :: thesis: verum