let R be non empty strict RelStr ; :: thesis: ( R in fin_RelStr_sp implies R is N-free )
set N4 = Necklace 4;
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 );
assume A1: R in fin_RelStr_sp ; :: thesis: R is N-free
then ex S being strict RelStr st
( R = S & the carrier of S in FinSETS ) by Def4;
then reconsider C = the carrier of R as Element of FinSETS ;
set k = card C;
A2: 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
A3: S1[m] ; :: thesis: ex n being Nat st
( n < m & S1[n] )
consider S being non empty strict RelStr such that
A4: S in fin_RelStr_sp and
A5: card the carrier of S = m and
A6: S embeds Necklace 4 by A3;
per cases ( S is 1 -element 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 A4, Th6;
suppose A7: S is 1 -element strict RelStr ; :: thesis: ex n being Nat st
( n < m & S1[n] )
A8: dom the InternalRel of S c= the carrier of S by RELAT_1:def 18;
A9: rng the InternalRel of S c= the carrier of S by RELAT_1:def 19;
consider f being Function of (Necklace 4),S such that
f is one-to-one and
A10: 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 A6, NECKLACE:def 1;
A11: the carrier of (Necklace 4) = {0,1,2,3} by NECKLACE:1, NECKLACE:20;
then A12: 0 in the carrier of (Necklace 4) by ENUMSET1:def 2;
A13: 1 in the carrier of (Necklace 4) by A11, ENUMSET1:def 2;
( 0 = 0 + 1 or 1 = 0 + 1 ) ;
then [0,1] in the InternalRel of (Necklace 4) by A12, A13, NECKLACE:25;
then A14: [(f . 0),(f . 1)] in the InternalRel of S by A10, A12, A13;
then A15: f . 1 in rng the InternalRel of S by XTUPLE_0:def 13;
f . 0 in dom the InternalRel of S by A14, XTUPLE_0:def 12;
then f . 0 = f . 1 by A7, A15, A8, A9, STRUCT_0:def 10;
then [0,0] in the InternalRel of (Necklace 4) by A10, A12, A14;
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 XTUPLE_0:1; :: 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
A16: the carrier of H1 misses the carrier of H2 and
A17: H1 in fin_RelStr_sp and
A18: H2 in fin_RelStr_sp and
A19: ( S = union_of (H1,H2) or S = sum_of (H1,H2) ) ;
A20: now :: thesis: ( S = sum_of (H1,H2) implies ex n being Nat st
( n < m & S1[n] ) )
A21: not [1,3] in the InternalRel of (Necklace 4)
proof
assume A22: [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 A22, Th2, ENUMSET1:def 4;
end;
end;
A23: not [0,2] in the InternalRel of (Necklace 4)
proof
assume A24: [0,2] in the InternalRel of (Necklace 4) ; :: thesis: contradiction
end;
A25: the carrier of (Necklace 4) = {0,1,2,3} by NECKLACE:1, NECKLACE:20;
then A26: 0 in the carrier of (Necklace 4) by ENUMSET1:def 2;
A27: not [0,3] in the InternalRel of (Necklace 4)
proof
assume A28: [0,3] in the InternalRel of (Necklace 4) ; :: thesis: contradiction
end;
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;
A29: dom the InternalRel of S c= the carrier of S by RELAT_1:def 18;
assume A30: S = sum_of (H1,H2) ; :: thesis: ex n being Nat st
( n < m & S1[n] )
A31: [: the carrier of H1, the carrier of H2:] c= the InternalRel of S
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in [: the carrier of H1, the carrier of H2:] or x in the InternalRel of S )
assume x in [: the carrier of H1, the carrier of H2:] ; :: thesis: x in the InternalRel of S
then A32: x in ( the InternalRel of H1 \/ the InternalRel of H2) \/ [: the carrier of H1, the carrier of H2:] by XBOOLE_0:def 3;
( the InternalRel of H1 \/ the InternalRel of H2) \/ [: the carrier of H1, the carrier of H2:] 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 H1 \/ the InternalRel of H2) \/ [: the carrier of H1, the carrier of H2:] c= the InternalRel of S by A30, Def3;
hence x in the InternalRel of S by A32; :: thesis: verum
end;
A33: rng the InternalRel of S c= the carrier of S by RELAT_1:def 19;
A34: 3 in the carrier of (Necklace 4) by A25, ENUMSET1:def 2;
A35: [: the carrier of H2, the carrier of H1:] c= the InternalRel of S
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in [: the carrier of H2, the carrier of H1:] or x in the InternalRel of S )
( 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 A36: ( 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 A30, Def3;
assume x in [: the carrier of H2, the carrier of H1:] ; :: thesis: x in the InternalRel of S
then 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;
hence x in the InternalRel of S by A36; :: thesis: verum
end;
A37: rng the InternalRel of H1 c= the carrier of H1 by RELAT_1:def 19;
A38: 1 in the carrier of (Necklace 4) by A25, ENUMSET1:def 2;
consider f being Function of (Necklace 4),S such that
A39: f is one-to-one and
A40: 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 A6, NECKLACE:def 1;
[1,0] in the InternalRel of (Necklace 4) by Th2, ENUMSET1:def 4;
then A41: [(f . 1),(f . 0)] in the InternalRel of S by A40, A26, A38;
A42: 2 in the carrier of (Necklace 4) by A25, ENUMSET1:def 2;
[3,2] in the InternalRel of (Necklace 4) by Th2, ENUMSET1:def 4;
then A43: [(f . 3),(f . 2)] in the InternalRel of S by A40, A42, A34;
[2,1] in the InternalRel of (Necklace 4) by Th2, ENUMSET1:def 4;
then A44: [(f . 2),(f . 1)] in the InternalRel of S by A40, A38, A42;
A45: rng the InternalRel of H2 c= the carrier of H2 by RELAT_1:def 19;
[2,3] in the InternalRel of (Necklace 4) by Th2, ENUMSET1:def 4;
then A46: [(f . 2),(f . 3)] in the InternalRel of S by A40, A42, A34;
then f . 3 in rng the InternalRel of S by XTUPLE_0:def 13;
then f . 3 in the carrier of S by A33;
then A47: f . 3 in the carrier of H1 \/ the carrier of H2 by A30, Def3;
[0,1] in the InternalRel of (Necklace 4) by Th2, ENUMSET1:def 4;
then A48: [(f . 0),(f . 1)] in the InternalRel of S by A40, A26, A38;
then f . 0 in dom the InternalRel of S by XTUPLE_0:def 12;
then f . 0 in the carrier of S by A29;
then A49: f . 0 in the carrier of H1 \/ the carrier of H2 by A30, Def3;
f . 1 in rng the InternalRel of S by A48, XTUPLE_0:def 13;
then f . 1 in the carrier of S by A33;
then A50: f . 1 in the carrier of H1 \/ the carrier of H2 by A30, Def3;
A51: dom the InternalRel of H1 c= the carrier of H1 by RELAT_1:def 18;
[1,2] in the InternalRel of (Necklace 4) by Th2, ENUMSET1:def 4;
then A52: [(f . 1),(f . 2)] in the InternalRel of S by A40, A38, A42;
then f . 2 in rng the InternalRel of S by XTUPLE_0:def 13;
then f . 2 in the carrier of S by A33;
then A53: f . 2 in the carrier of H1 \/ the carrier of H2 by A30, Def3;
A54: dom the InternalRel of H2 c= the carrier of H2 by RELAT_1:def 18;
per cases ( f . 0 in the carrier of H1 or f . 0 in the carrier of H2 ) by A49, XBOOLE_0:def 3;
suppose A55: f . 0 in the carrier of H1 ; :: thesis: ex n being Nat st
( n < m & S1[n] )
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)];
A56: now :: thesis: not [(f . 0),(f . 1)] in [: the carrier of H2, the carrier of H1:]
assume [(f . 0),(f . 1)] in [: the carrier of H2, the carrier of H1:] ; :: thesis: contradiction
then f . 0 in the carrier of H2 by ZFMISC_1:87;
hence contradiction by A16, A55, XBOOLE_0:3; :: thesis: verum
end;
A57: now :: thesis: not f . 2 in the carrier of H2
assume f . 2 in the carrier of H2 ; :: thesis: contradiction
then [(f . 0),(f . 2)] in [: the carrier of H1, the carrier of H2:] by A55, ZFMISC_1:87;
hence contradiction by A40, A26, A42, A23, A31; :: thesis: verum
end;
A58: now :: thesis: not [(f . 1),(f . 0)] in the InternalRel of H2
assume [(f . 1),(f . 0)] in the InternalRel of H2 ; :: thesis: contradiction
then f . 0 in rng the InternalRel of H2 by XTUPLE_0:def 13;
hence contradiction by A16, A45, A55, XBOOLE_0:3; :: thesis: verum
end;
A59: now :: thesis: not [(f . 1),(f . 0)] in [: the carrier of H1, the carrier of H2:]
assume [(f . 1),(f . 0)] in [: the carrier of H1, the carrier of H2:] ; :: thesis: contradiction
then f . 0 in the carrier of H2 by ZFMISC_1:87;
hence contradiction by A16, A55, XBOOLE_0:3; :: thesis: verum
end;
A60: now :: thesis: not [(f . 0),(f . 1)] in the InternalRel of H2
assume [(f . 0),(f . 1)] in the InternalRel of H2 ; :: thesis: contradiction
then f . 0 in dom the InternalRel of H2 by XTUPLE_0:def 12;
hence contradiction by A16, A54, A55, XBOOLE_0:3; :: thesis: verum
end;
A61: now :: thesis: not f . 3 in the carrier of H2
assume f . 3 in the carrier of H2 ; :: thesis: contradiction
then [(f . 0),(f . 3)] in [: the carrier of H1, the carrier of H2:] by A55, ZFMISC_1:87;
hence contradiction by A40, A26, A34, A27, A31; :: thesis: verum
end;
then A62: f . 3 in the carrier of H1 by A47, XBOOLE_0:def 3;
A63: now :: thesis: not f . 1 in the carrier of H2
assume f . 1 in the carrier of H2 ; :: thesis: contradiction
then [(f . 1),(f . 3)] in [: the carrier of H2, the carrier of H1:] by A62, ZFMISC_1:87;
hence contradiction by A40, A38, A34, A21, A35; :: thesis: verum
end;
A64: dom f = the carrier of (Necklace 4) by FUNCT_2:def 1;
rng f c= the carrier of H1
proof
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng f or y in the carrier of H1 )
assume y in rng f ; :: thesis: y in the carrier of H1
then consider x being object such that
A65: x in dom f and
A66: y = f . x by FUNCT_1:def 3;
per cases ( x = 0 or x = 1 or x = 2 or x = 3 ) by A64, A65, Lm1, ENUMSET1:def 2;
suppose x = 0 ; :: thesis: y in the carrier of H1
hence y in the carrier of H1 by A55, A66; :: thesis: verum
end;
suppose x = 1 ; :: thesis: y in the carrier of H1
hence y in the carrier of H1 by A50, A63, A66, XBOOLE_0:def 3; :: thesis: verum
end;
suppose x = 2 ; :: thesis: y in the carrier of H1
hence y in the carrier of H1 by A53, A57, A66, XBOOLE_0:def 3; :: thesis: verum
end;
suppose x = 3 ; :: thesis: y in the carrier of H1
hence y in the carrier of H1 by A47, A61, A66, XBOOLE_0:def 3; :: thesis: verum
end;
end;
end;
then A67: f is Function of the carrier of (Necklace 4), the carrier of H1 by FUNCT_2:6;
H1 is finite by A17, Th4;
then reconsider cH1 = the carrier of H1 as finite set ;
A68: H1 is non empty strict RelStr by A17, Th4;
A69: now :: thesis: not [(f . 3),(f . 2)] in the InternalRel of H2
assume [(f . 3),(f . 2)] in the InternalRel of H2 ; :: thesis: contradiction
then f . 2 in rng the InternalRel of H2 by XTUPLE_0:def 13;
hence contradiction by A45, A57; :: thesis: verum
end;
A70: now :: thesis: not [(f . 2),(f . 3)] in the InternalRel of H2
assume [(f . 2),(f . 3)] in the InternalRel of H2 ; :: thesis: contradiction
then f . 2 in dom the InternalRel of H2 by XTUPLE_0:def 12;
hence contradiction by A54, A57; :: thesis: verum
end;
[(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 A30, A41, 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 ( [(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;
then A71: [(f . 1),(f . 0)] in the InternalRel of H1 by A58, A59, A63, XBOOLE_0:def 3, ZFMISC_1:87;
A72: now :: thesis: not [(f . 1),(f . 2)] in the InternalRel of H2
assume [(f . 1),(f . 2)] in the InternalRel of H2 ; :: thesis: contradiction
then f . 1 in dom the InternalRel of H2 by XTUPLE_0:def 12;
hence contradiction by A54, A63; :: thesis: verum
end;
[(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 A30, A52, 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 ( [(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;
then A73: [(f . 1),(f . 2)] in the InternalRel of H1 by A72, A57, A63, XBOOLE_0:def 3, ZFMISC_1:87;
[(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 A30, A43, 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 ( [(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;
then A74: [(f . 3),(f . 2)] in the InternalRel of H1 by A69, A57, A61, XBOOLE_0:def 3, ZFMISC_1:87;
[(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 A30, A46, 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 ( [(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;
then A75: [(f . 2),(f . 3)] in the InternalRel of H1 by A70, A61, A57, XBOOLE_0:def 3, ZFMISC_1:87;
A76: now :: thesis: not [(f . 2),(f . 1)] in the InternalRel of H2
assume [(f . 2),(f . 1)] in the InternalRel of H2 ; :: thesis: contradiction
then f . 1 in rng the InternalRel of H2 by XTUPLE_0:def 13;
hence contradiction by A45, A63; :: thesis: verum
end;
H2 is finite by A18, Th4;
then reconsider cH2 = the carrier of H2 as finite set ;
the carrier of S = cH1 \/ cH2 by A30, Def3;
then reconsider cS = the carrier of S as finite set ;
A77: not H2 is empty by A18, Th4;
A78: cH1 <> cS
proof
A79: cS = cH1 \/ cH2 by A30, Def3;
assume A80: cH1 = cS ; :: thesis: contradiction
consider x being object such that
A81: x in cH2 by A77, XBOOLE_0:def 1;
cH1 /\ cH2 = {} by A16, XBOOLE_0:def 7;
then not x in cH1 by A81, XBOOLE_0:def 4;
hence contradiction by A80, A79, A81, XBOOLE_0:def 3; :: thesis: verum
end;
cS = cH1 \/ cH2 by A30, Def3;
then cH1 c= cS by XBOOLE_1:7;
then cH1 c< cS by A78, XBOOLE_0:def 8;
then A82: card cH1 < card cS by CARD_2:48;
[(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 A30, A44, 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 ( [(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;
then A83: [(f . 2),(f . 1)] in the InternalRel of H1 by A76, A63, A57, XBOOLE_0:def 3, ZFMISC_1:87;
[(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 A30, A48, 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 ( [(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;
then A84: [(f . 0),(f . 1)] in the InternalRel of H1 by A60, A63, A56, XBOOLE_0:def 3, ZFMISC_1:87;
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 A85: [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 A85, Th2, ENUMSET1:def 4;
suppose A86: [x,y] = [0,1] ; :: thesis: [(f . x),(f . y)] in the InternalRel of H1
then x = 0 by XTUPLE_0:1;
hence [(f . x),(f . y)] in the InternalRel of H1 by A84, A86, XTUPLE_0:1; :: thesis: verum
end;
suppose A87: [x,y] = [1,0] ; :: thesis: [(f . x),(f . y)] in the InternalRel of H1
then x = 1 by XTUPLE_0:1;
hence [(f . x),(f . y)] in the InternalRel of H1 by A71, A87, XTUPLE_0:1; :: thesis: verum
end;
suppose A88: [x,y] = [1,2] ; :: thesis: [(f . x),(f . y)] in the InternalRel of H1
then x = 1 by XTUPLE_0:1;
hence [(f . x),(f . y)] in the InternalRel of H1 by A73, A88, XTUPLE_0:1; :: thesis: verum
end;
suppose A89: [x,y] = [2,1] ; :: thesis: [(f . x),(f . y)] in the InternalRel of H1
then x = 2 by XTUPLE_0:1;
hence [(f . x),(f . y)] in the InternalRel of H1 by A83, A89, XTUPLE_0:1; :: thesis: verum
end;
suppose A90: [x,y] = [2,3] ; :: thesis: [(f . x),(f . y)] in the InternalRel of H1
then x = 2 by XTUPLE_0:1;
hence [(f . x),(f . y)] in the InternalRel of H1 by A75, A90, XTUPLE_0:1; :: thesis: verum
end;
suppose A91: [x,y] = [3,2] ; :: thesis: [(f . x),(f . y)] in the InternalRel of H1
then x = 3 by XTUPLE_0:1;
hence [(f . x),(f . y)] in the InternalRel of H1 by A74, A91, XTUPLE_0:1; :: thesis: verum
end;
end;
end;
thus ( [(f . x),(f . y)] in the InternalRel of H1 implies [x,y] in the InternalRel of (Necklace 4) ) :: thesis: verum
proof
( [(f . x),(f . y)] in the InternalRel of S implies [x,y] in the InternalRel of (Necklace 4) ) by A40;
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 A30, 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 A92: ( [(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;
assume [(f . x),(f . y)] in the InternalRel of H1 ; :: thesis: [x,y] in the InternalRel of (Necklace 4)
hence [x,y] in the InternalRel of (Necklace 4) by A92, XBOOLE_0:def 3; :: thesis: verum
end;
end;
then H1 embeds Necklace 4 by A39, A67, NECKLACE:def 1;
hence ex n being Nat st
( n < m & S1[n] ) by A5, A17, A68, A82; :: thesis: verum
end;
suppose A93: f . 0 in the carrier of H2 ; :: thesis: ex n being Nat st
( n < m & S1[n] )
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)];
A94: now :: thesis: not [(f . 0),(f . 1)] in [: the carrier of H1, the carrier of H2:]
assume [(f . 0),(f . 1)] in [: the carrier of H1, the carrier of H2:] ; :: thesis: contradiction
then f . 0 in the carrier of H1 by ZFMISC_1:87;
hence contradiction by A16, A93, XBOOLE_0:3; :: thesis: verum
end;
A95: now :: thesis: not [(f . 1),(f . 0)] in [: the carrier of H2, the carrier of H1:]
assume [(f . 1),(f . 0)] in [: the carrier of H2, the carrier of H1:] ; :: thesis: contradiction
then f . 0 in the carrier of H1 by ZFMISC_1:87;
hence contradiction by A16, A93, XBOOLE_0:3; :: thesis: verum
end;
A96: now :: thesis: not f . 3 in the carrier of H1
assume f . 3 in the carrier of H1 ; :: thesis: contradiction
then [(f . 0),(f . 3)] in [: the carrier of H2, the carrier of H1:] by A93, ZFMISC_1:87;
hence contradiction by A40, A26, A34, A27, A35; :: thesis: verum
end;
then A97: f . 3 in the carrier of H2 by A47, XBOOLE_0:def 3;
A98: now :: thesis: not f . 1 in the carrier of H1
assume f . 1 in the carrier of H1 ; :: thesis: contradiction
then [(f . 1),(f . 3)] in [: the carrier of H1, the carrier of H2:] by A97, ZFMISC_1:87;
hence contradiction by A40, A38, A34, A21, A31; :: thesis: verum
end;
A99: now :: thesis: not [(f . 1),(f . 0)] in the InternalRel of H1
assume [(f . 1),(f . 0)] in the InternalRel of H1 ; :: thesis: contradiction
then f . 1 in dom the InternalRel of H1 by XTUPLE_0:def 12;
hence contradiction by A51, A98; :: thesis: verum
end;
[(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 A30, A41, 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 ( [(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;
then A100: [(f . 1),(f . 0)] in the InternalRel of H2 by A99, A98, A95, XBOOLE_0:def 3, ZFMISC_1:87;
A101: now :: thesis: not [(f . 2),(f . 1)] in the InternalRel of H1
assume [(f . 2),(f . 1)] in the InternalRel of H1 ; :: thesis: contradiction
then f . 1 in rng the InternalRel of H1 by XTUPLE_0:def 13;
hence contradiction by A37, A98; :: thesis: verum
end;
A102: now :: thesis: not f . 2 in the carrier of H1
assume f . 2 in the carrier of H1 ; :: thesis: contradiction
then [(f . 0),(f . 2)] in [: the carrier of H2, the carrier of H1:] by A93, ZFMISC_1:87;
hence contradiction by A40, A26, A42, A23, A35; :: thesis: verum
end;
A103: dom f = the carrier of (Necklace 4) by FUNCT_2:def 1;
rng f c= the carrier of H2
proof
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng f or y in the carrier of H2 )
assume y in rng f ; :: thesis: y in the carrier of H2
then consider x being object such that
A104: x in dom f and
A105: y = f . x by FUNCT_1:def 3;
per cases ( x = 0 or x = 1 or x = 2 or x = 3 ) by A103, A104, Lm1, ENUMSET1:def 2;
suppose x = 0 ; :: thesis: y in the carrier of H2
hence y in the carrier of H2 by A93, A105; :: thesis: verum
end;
suppose x = 1 ; :: thesis: y in the carrier of H2
hence y in the carrier of H2 by A50, A98, A105, XBOOLE_0:def 3; :: thesis: verum
end;
suppose x = 2 ; :: thesis: y in the carrier of H2
hence y in the carrier of H2 by A53, A102, A105, XBOOLE_0:def 3; :: thesis: verum
end;
suppose x = 3 ; :: thesis: y in the carrier of H2
hence y in the carrier of H2 by A47, A96, A105, XBOOLE_0:def 3; :: thesis: verum
end;
end;
end;
then A106: f is Function of the carrier of (Necklace 4), the carrier of H2 by FUNCT_2:6;
H1 is finite by A17, Th4;
then reconsider cH1 = the carrier of H1 as finite set ;
A107: H2 is non empty strict RelStr by A18, Th4;
A108: now :: thesis: not [(f . 0),(f . 1)] in the InternalRel of H1
assume [(f . 0),(f . 1)] in the InternalRel of H1 ; :: thesis: contradiction
then f . 0 in dom the InternalRel of H1 by XTUPLE_0:def 12;
hence contradiction by A16, A51, A93, XBOOLE_0:3; :: thesis: verum
end;
A109: now :: thesis: not [(f . 3),(f . 2)] in the InternalRel of H1
assume [(f . 3),(f . 2)] in the InternalRel of H1 ; :: thesis: contradiction
then f . 2 in rng the InternalRel of H1 by XTUPLE_0:def 13;
hence contradiction by A37, A102; :: thesis: verum
end;
A110: now :: thesis: not [(f . 2),(f . 3)] in the InternalRel of H1
assume [(f . 2),(f . 3)] in the InternalRel of H1 ; :: thesis: contradiction
then f . 2 in dom the InternalRel of H1 by XTUPLE_0:def 12;
hence contradiction by A51, A102; :: thesis: verum
end;
[(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 A30, A43, 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 ( [(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;
then A111: [(f . 3),(f . 2)] in the InternalRel of H2 by A109, A96, A102, XBOOLE_0:def 3, ZFMISC_1:87;
A112: now :: thesis: not [(f . 1),(f . 2)] in the InternalRel of H1
assume [(f . 1),(f . 2)] in the InternalRel of H1 ; :: thesis: contradiction
then f . 2 in rng the InternalRel of H1 by XTUPLE_0:def 13;
hence contradiction by A37, A102; :: thesis: verum
end;
[(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 A30, A52, 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 ( [(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;
then A113: [(f . 1),(f . 2)] in the InternalRel of H2 by A112, A98, A102, XBOOLE_0:def 3, ZFMISC_1:87;
[(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 A30, A46, 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 ( [(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;
then A114: [(f . 2),(f . 3)] in the InternalRel of H2 by A110, A102, A96, XBOOLE_0:def 3, ZFMISC_1:87;
[(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 A30, A44, 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 ( [(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;
then A115: [(f . 2),(f . 1)] in the InternalRel of H2 by A101, A102, A98, XBOOLE_0:def 3, ZFMISC_1:87;
H2 is finite by A18, Th4;
then reconsider cH2 = the carrier of H2 as finite set ;
the carrier of S = cH1 \/ cH2 by A30, Def3;
then reconsider cS = the carrier of S as finite set ;
A116: not H1 is empty by A17, Th4;
A117: cH2 <> cS
proof
A118: cS = cH1 \/ cH2 by A30, Def3;
assume A119: cH2 = cS ; :: thesis: contradiction
consider x being object such that
A120: x in cH1 by A116, XBOOLE_0:def 1;
cH1 /\ cH2 = {} by A16, XBOOLE_0:def 7;
then not x in cH2 by A120, XBOOLE_0:def 4;
hence contradiction by A119, A118, A120, XBOOLE_0:def 3; :: thesis: verum
end;
cS = cH1 \/ cH2 by A30, Def3;
then cH2 c= cS by XBOOLE_1:7;
then cH2 c< cS by A117, XBOOLE_0:def 8;
then A121: card cH2 < card cS by CARD_2:48;
[(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 A30, A48, 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 ( [(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;
then A122: [(f . 0),(f . 1)] in the InternalRel of H2 by A108, A94, A98, XBOOLE_0:def 3, ZFMISC_1:87;
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 A123: [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 A123, Th2, ENUMSET1:def 4;
suppose A124: [x,y] = [0,1] ; :: thesis: [(f . x),(f . y)] in the InternalRel of H2
then x = 0 by XTUPLE_0:1;
hence [(f . x),(f . y)] in the InternalRel of H2 by A122, A124, XTUPLE_0:1; :: thesis: verum
end;
suppose A125: [x,y] = [1,0] ; :: thesis: [(f . x),(f . y)] in the InternalRel of H2
then x = 1 by XTUPLE_0:1;
hence [(f . x),(f . y)] in the InternalRel of H2 by A100, A125, XTUPLE_0:1; :: thesis: verum
end;
suppose A126: [x,y] = [1,2] ; :: thesis: [(f . x),(f . y)] in the InternalRel of H2
then x = 1 by XTUPLE_0:1;
hence [(f . x),(f . y)] in the InternalRel of H2 by A113, A126, XTUPLE_0:1; :: thesis: verum
end;
suppose A127: [x,y] = [2,1] ; :: thesis: [(f . x),(f . y)] in the InternalRel of H2
then x = 2 by XTUPLE_0:1;
hence [(f . x),(f . y)] in the InternalRel of H2 by A115, A127, XTUPLE_0:1; :: thesis: verum
end;
suppose A128: [x,y] = [2,3] ; :: thesis: [(f . x),(f . y)] in the InternalRel of H2
then x = 2 by XTUPLE_0:1;
hence [(f . x),(f . y)] in the InternalRel of H2 by A114, A128, XTUPLE_0:1; :: thesis: verum
end;
suppose A129: [x,y] = [3,2] ; :: thesis: [(f . x),(f . y)] in the InternalRel of H2
then x = 3 by XTUPLE_0:1;
hence [(f . x),(f . y)] in the InternalRel of H2 by A111, A129, XTUPLE_0:1; :: thesis: verum
end;
end;
end;
thus ( [(f . x),(f . y)] in the InternalRel of H2 implies [x,y] in the InternalRel of (Necklace 4) ) :: thesis: verum
proof
( [(f . x),(f . y)] in the InternalRel of S implies [x,y] in the InternalRel of (Necklace 4) ) by A40;
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 A30, 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 A130: ( [(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;
assume [(f . x),(f . y)] in the InternalRel of H2 ; :: thesis: [x,y] in the InternalRel of (Necklace 4)
hence [x,y] in the InternalRel of (Necklace 4) by A130, XBOOLE_0:def 3; :: thesis: verum
end;
end;
then H2 embeds Necklace 4 by A39, A106, NECKLACE:def 1;
hence ex n being Nat st
( n < m & S1[n] ) by A5, A18, A107, A121; :: thesis: verum
end;
end;
end;
now :: thesis: ( S = union_of (H1,H2) implies ex n being Nat st
( n < m & S1[n] ) )
A131: the carrier of (Necklace 4) = {0,1,2,3} by NECKLACE:1, NECKLACE:20;
then A132: 0 in the carrier of (Necklace 4) by ENUMSET1:def 2;
A133: 3 in the carrier of (Necklace 4) by A131, ENUMSET1:def 2;
A134: 1 in the carrier of (Necklace 4) by A131, ENUMSET1:def 2;
A135: dom the InternalRel of S c= the carrier of S by RELAT_1:def 18;
consider f being Function of (Necklace 4),S such that
A136: f is one-to-one and
A137: 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 A6, NECKLACE:def 1;
assume A138: S = union_of (H1,H2) ; :: thesis: ex n being Nat st
( n < m & S1[n] )
[0,1] in the InternalRel of (Necklace 4) by Th2, ENUMSET1:def 4;
then A139: [(f . 0),(f . 1)] in the InternalRel of S by A137, A132, A134;
then f . 0 in dom the InternalRel of S by XTUPLE_0:def 12;
then f . 0 in the carrier of S by A135;
then A140: f . 0 in the carrier of H1 \/ the carrier of H2 by A138, Def2;
A141: 2 in the carrier of (Necklace 4) by A131, ENUMSET1:def 2;
[3,2] in the InternalRel of (Necklace 4) by Th2, ENUMSET1:def 4;
then A142: [(f . 3),(f . 2)] in the InternalRel of S by A137, A141, A133;
[2,3] in the InternalRel of (Necklace 4) by Th2, ENUMSET1:def 4;
then A143: [(f . 2),(f . 3)] in the InternalRel of S by A137, A141, A133;
[2,1] in the InternalRel of (Necklace 4) by Th2, ENUMSET1:def 4;
then A144: [(f . 2),(f . 1)] in the InternalRel of S by A137, A134, A141;
[1,2] in the InternalRel of (Necklace 4) by Th2, ENUMSET1:def 4;
then A145: [(f . 1),(f . 2)] in the InternalRel of S by A137, A134, A141;
[1,0] in the InternalRel of (Necklace 4) by Th2, ENUMSET1:def 4;
then A146: [(f . 1),(f . 0)] in the InternalRel of S by A137, A132, A134;
per cases ( f . 0 in the carrier of H1 or f . 0 in the carrier of H2 ) by A140, XBOOLE_0:def 3;
suppose A147: f . 0 in the carrier of H1 ; :: thesis: ex n being Nat st
( n < m & S1[n] )
set cS = the carrier of S;
set cH1 = the carrier of H1;
set cH2 = the carrier of H2;
A148: dom f = the carrier of (Necklace 4) by FUNCT_2:def 1;
H2 is finite by A18, Th4;
then reconsider cH2 = the carrier of H2 as finite set ;
H1 is finite by A17, Th4;
then reconsider cH1 = the carrier of H1 as finite set ;
A149: the carrier of S = cH1 \/ cH2 by A138, Def2;
A150: dom the InternalRel of H2 c= the carrier of H2 by RELAT_1:def 18;
A151: now :: thesis: not [(f . 0),(f . 1)] in the InternalRel of H2
assume [(f . 0),(f . 1)] in the InternalRel of H2 ; :: thesis: contradiction
then f . 0 in dom the InternalRel of H2 by XTUPLE_0:def 12;
hence contradiction by A16, A147, A150, XBOOLE_0:3; :: thesis: verum
end;
A152: rng the InternalRel of H2 c= the carrier of H2 by RELAT_1:def 19;
A153: now :: thesis: not [(f . 1),(f . 0)] in the InternalRel of H2
assume [(f . 1),(f . 0)] in the InternalRel of H2 ; :: thesis: contradiction
then f . 0 in rng the InternalRel of H2 by XTUPLE_0:def 13;
hence contradiction by A16, A147, A152, XBOOLE_0:3; :: thesis: verum
end;
[(f . 1),(f . 0)] in the InternalRel of H1 \/ the InternalRel of H2 by A138, A146, Def2;
then A154: [(f . 1),(f . 0)] in the InternalRel of H1 by A153, XBOOLE_0:def 3;
A155: H1 is non empty strict RelStr by A17, Th4;
reconsider cS = the carrier of S as finite set by A149;
A156: rng the InternalRel of H1 c= the carrier of H1 by RELAT_1:def 19;
[(f . 0),(f . 1)] in the InternalRel of H1 \/ the InternalRel of H2 by A138, A139, Def2;
then A157: [(f . 0),(f . 1)] in the InternalRel of H1 by A151, XBOOLE_0:def 3;
then A158: f . 1 in rng the InternalRel of H1 by XTUPLE_0:def 13;
A159: now :: thesis: not [(f . 2),(f . 1)] in the InternalRel of H2
assume [(f . 2),(f . 1)] in the InternalRel of H2 ; :: thesis: contradiction
then f . 1 in rng the InternalRel of H2 by XTUPLE_0:def 13;
hence contradiction by A16, A156, A152, A158, XBOOLE_0:3; :: thesis: verum
end;
A160: not H2 is empty by A18, Th4;
A161: cH1 <> cS
proof
A162: cS = cH1 \/ cH2 by A138, Def2;
assume A163: cH1 = cS ; :: thesis: contradiction
consider x being object such that
A164: x in cH2 by A160, XBOOLE_0:def 1;
cH1 /\ cH2 = {} by A16, XBOOLE_0:def 7;
then not x in cH1 by A164, XBOOLE_0:def 4;
hence contradiction by A163, A162, A164, XBOOLE_0:def 3; :: thesis: verum
end;
cS = cH1 \/ cH2 by A138, Def2;
then cH1 c= cS by XBOOLE_1:7;
then cH1 c< cS by A161, XBOOLE_0:def 8;
then A165: card cH1 < card cS by CARD_2:48;
A166: [(f . 2),(f . 3)] in the InternalRel of H1 \/ the InternalRel of H2 by A138, A143, Def2;
A167: [(f . 1),(f . 2)] in the InternalRel of H1 \/ the InternalRel of H2 by A138, A145, Def2;
now :: thesis: not [(f . 1),(f . 2)] in the InternalRel of H2
assume [(f . 1),(f . 2)] in the InternalRel of H2 ; :: thesis: contradiction
then f . 1 in dom the InternalRel of H2 by XTUPLE_0:def 12;
hence contradiction by A16, A156, A150, A158, XBOOLE_0:3; :: thesis: verum
end;
then A168: [(f . 1),(f . 2)] in the InternalRel of H1 by A167, XBOOLE_0:def 3;
then A169: f . 2 in rng the InternalRel of H1 by XTUPLE_0:def 13;
now :: thesis: not [(f . 2),(f . 3)] in the InternalRel of H2
assume [(f . 2),(f . 3)] in the InternalRel of H2 ; :: thesis: contradiction
then f . 2 in dom the InternalRel of H2 by XTUPLE_0:def 12;
hence contradiction by A16, A156, A150, A169, XBOOLE_0:3; :: thesis: verum
end;
then A170: [(f . 2),(f . 3)] in the InternalRel of H1 by A166, XBOOLE_0:def 3;
[(f . 2),(f . 1)] in the InternalRel of H1 \/ the InternalRel of H2 by A138, A144, Def2;
then A171: [(f . 2),(f . 1)] in the InternalRel of H1 by A159, XBOOLE_0:def 3;
A172: now :: thesis: not [(f . 3),(f . 2)] in the InternalRel of H2
assume [(f . 3),(f . 2)] in the InternalRel of H2 ; :: thesis: contradiction
then f . 2 in rng the InternalRel of H2 by XTUPLE_0:def 13;
hence contradiction by A16, A156, A152, A169, XBOOLE_0:3; :: thesis: verum
end;
[(f . 3),(f . 2)] in the InternalRel of H1 \/ the InternalRel of H2 by A138, A142, Def2;
then A173: [(f . 3),(f . 2)] in the InternalRel of H1 by A172, XBOOLE_0:def 3;
A174: 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 A175: [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 A175, Th2, ENUMSET1:def 4;
suppose A176: [x,y] = [0,1] ; :: thesis: [(f . x),(f . y)] in the InternalRel of H1
then x = 0 by XTUPLE_0:1;
hence [(f . x),(f . y)] in the InternalRel of H1 by A157, A176, XTUPLE_0:1; :: thesis: verum
end;
suppose A177: [x,y] = [1,0] ; :: thesis: [(f . x),(f . y)] in the InternalRel of H1
then x = 1 by XTUPLE_0:1;
hence [(f . x),(f . y)] in the InternalRel of H1 by A154, A177, XTUPLE_0:1; :: thesis: verum
end;
suppose A178: [x,y] = [1,2] ; :: thesis: [(f . x),(f . y)] in the InternalRel of H1
then x = 1 by XTUPLE_0:1;
hence [(f . x),(f . y)] in the InternalRel of H1 by A168, A178, XTUPLE_0:1; :: thesis: verum
end;
suppose A179: [x,y] = [2,1] ; :: thesis: [(f . x),(f . y)] in the InternalRel of H1
then x = 2 by XTUPLE_0:1;
hence [(f . x),(f . y)] in the InternalRel of H1 by A171, A179, XTUPLE_0:1; :: thesis: verum
end;
suppose A180: [x,y] = [2,3] ; :: thesis: [(f . x),(f . y)] in the InternalRel of H1
then x = 2 by XTUPLE_0:1;
hence [(f . x),(f . y)] in the InternalRel of H1 by A170, A180, XTUPLE_0:1; :: thesis: verum
end;
suppose A181: [x,y] = [3,2] ; :: thesis: [(f . x),(f . y)] in the InternalRel of H1
then x = 3 by XTUPLE_0:1;
hence [(f . x),(f . y)] in the InternalRel of H1 by A173, A181, XTUPLE_0:1; :: thesis: verum
end;
end;
end;
thus ( [(f . x),(f . y)] in the InternalRel of H1 implies [x,y] in the InternalRel of (Necklace 4) ) :: thesis: verum
proof
( [(f . x),(f . y)] in the InternalRel of S implies [x,y] in the InternalRel of (Necklace 4) ) by A137;
then A182: ( [(f . x),(f . y)] in the InternalRel of H1 \/ the InternalRel of H2 implies [x,y] in the InternalRel of (Necklace 4) ) by A138, Def2;
assume [(f . x),(f . y)] in the InternalRel of H1 ; :: thesis: [x,y] in the InternalRel of (Necklace 4)
hence [x,y] in the InternalRel of (Necklace 4) by A182, XBOOLE_0:def 3; :: thesis: verum
end;
end;
A183: f . 3 in rng the InternalRel of H1 by A170, XTUPLE_0:def 13;
rng f c= the carrier of H1
proof
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng f or y in the carrier of H1 )
assume y in rng f ; :: thesis: y in the carrier of H1
then consider x being object such that
A184: x in dom f and
A185: y = f . x by FUNCT_1:def 3;
per cases ( x = 0 or x = 1 or x = 2 or x = 3 ) by A148, A184, Lm1, ENUMSET1:def 2;
suppose x = 0 ; :: thesis: y in the carrier of H1
hence y in the carrier of H1 by A147, A185; :: thesis: verum
end;
suppose x = 1 ; :: thesis: y in the carrier of H1
hence y in the carrier of H1 by A156, A158, A185; :: thesis: verum
end;
suppose x = 2 ; :: thesis: y in the carrier of H1
hence y in the carrier of H1 by A156, A169, A185; :: thesis: verum
end;
suppose x = 3 ; :: thesis: y in the carrier of H1
hence y in the carrier of H1 by A156, A183, A185; :: thesis: verum
end;
end;
end;
then f is Function of the carrier of (Necklace 4), the carrier of H1 by FUNCT_2:6;
then H1 embeds Necklace 4 by A136, A174, NECKLACE:def 1;
hence ex n being Nat st
( n < m & S1[n] ) by A5, A17, A155, A165; :: thesis: verum
end;
suppose A186: f . 0 in the carrier of H2 ; :: thesis: ex n being Nat st
( n < m & S1[n] )
set cS = the carrier of S;
set cH1 = the carrier of H1;
set cH2 = the carrier of H2;
A187: dom f = the carrier of (Necklace 4) by FUNCT_2:def 1;
H2 is finite by A18, Th4;
then reconsider cH2 = the carrier of H2 as finite set ;
H1 is finite by A17, Th4;
then reconsider cH1 = the carrier of H1 as finite set ;
A188: the carrier of S = cH1 \/ cH2 by A138, Def2;
A189: dom the InternalRel of H1 c= the carrier of H1 by RELAT_1:def 18;
A190: now :: thesis: not [(f . 0),(f . 1)] in the InternalRel of H1
assume [(f . 0),(f . 1)] in the InternalRel of H1 ; :: thesis: contradiction
then f . 0 in dom the InternalRel of H1 by XTUPLE_0:def 12;
hence contradiction by A16, A186, A189, XBOOLE_0:3; :: thesis: verum
end;
A191: rng the InternalRel of H1 c= the carrier of H1 by RELAT_1:def 19;
A192: now :: thesis: not [(f . 1),(f . 0)] in the InternalRel of H1
assume [(f . 1),(f . 0)] in the InternalRel of H1 ; :: thesis: contradiction
then f . 0 in rng the InternalRel of H1 by XTUPLE_0:def 13;
hence contradiction by A16, A186, A191, XBOOLE_0:3; :: thesis: verum
end;
[(f . 1),(f . 0)] in the InternalRel of H1 \/ the InternalRel of H2 by A138, A146, Def2;
then A193: [(f . 1),(f . 0)] in the InternalRel of H2 by A192, XBOOLE_0:def 3;
A194: H2 is non empty strict RelStr by A18, Th4;
reconsider cS = the carrier of S as finite set by A188;
A195: rng the InternalRel of H2 c= the carrier of H2 by RELAT_1:def 19;
[(f . 0),(f . 1)] in the InternalRel of H1 \/ the InternalRel of H2 by A138, A139, Def2;
then A196: [(f . 0),(f . 1)] in the InternalRel of H2 by A190, XBOOLE_0:def 3;
then A197: f . 1 in rng the InternalRel of H2 by XTUPLE_0:def 13;
A198: now :: thesis: not [(f . 2),(f . 1)] in the InternalRel of H1
assume [(f . 2),(f . 1)] in the InternalRel of H1 ; :: thesis: contradiction
then f . 1 in rng the InternalRel of H1 by XTUPLE_0:def 13;
hence contradiction by A16, A195, A191, A197, XBOOLE_0:3; :: thesis: verum
end;
A199: not H1 is empty by A17, Th4;
A200: cH2 <> cS
proof
A201: cS = cH1 \/ cH2 by A138, Def2;
assume A202: cH2 = cS ; :: thesis: contradiction
consider x being object such that
A203: x in cH1 by A199, XBOOLE_0:def 1;
cH1 /\ cH2 = {} by A16, XBOOLE_0:def 7;
then not x in cH2 by A203, XBOOLE_0:def 4;
hence contradiction by A202, A201, A203, XBOOLE_0:def 3; :: thesis: verum
end;
cS = cH1 \/ cH2 by A138, Def2;
then cH2 c= cS by XBOOLE_1:7;
then cH2 c< cS by A200, XBOOLE_0:def 8;
then A204: card cH2 < card cS by CARD_2:48;
A205: [(f . 2),(f . 3)] in the InternalRel of H1 \/ the InternalRel of H2 by A138, A143, Def2;
A206: [(f . 1),(f . 2)] in the InternalRel of H1 \/ the InternalRel of H2 by A138, A145, Def2;
now :: thesis: not [(f . 1),(f . 2)] in the InternalRel of H1
assume [(f . 1),(f . 2)] in the InternalRel of H1 ; :: thesis: contradiction
then f . 1 in dom the InternalRel of H1 by XTUPLE_0:def 12;
hence contradiction by A16, A195, A189, A197, XBOOLE_0:3; :: thesis: verum
end;
then A207: [(f . 1),(f . 2)] in the InternalRel of H2 by A206, XBOOLE_0:def 3;
then A208: f . 2 in rng the InternalRel of H2 by XTUPLE_0:def 13;
now :: thesis: not [(f . 2),(f . 3)] in the InternalRel of H1
assume [(f . 2),(f . 3)] in the InternalRel of H1 ; :: thesis: contradiction
then f . 2 in dom the InternalRel of H1 by XTUPLE_0:def 12;
hence contradiction by A16, A195, A189, A208, XBOOLE_0:3; :: thesis: verum
end;
then A209: [(f . 2),(f . 3)] in the InternalRel of H2 by A205, XBOOLE_0:def 3;
[(f . 2),(f . 1)] in the InternalRel of H1 \/ the InternalRel of H2 by A138, A144, Def2;
then A210: [(f . 2),(f . 1)] in the InternalRel of H2 by A198, XBOOLE_0:def 3;
A211: now :: thesis: not [(f . 3),(f . 2)] in the InternalRel of H1
assume [(f . 3),(f . 2)] in the InternalRel of H1 ; :: thesis: contradiction
then f . 2 in rng the InternalRel of H1 by XTUPLE_0:def 13;
hence contradiction by A16, A195, A191, A208, XBOOLE_0:3; :: thesis: verum
end;
[(f . 3),(f . 2)] in the InternalRel of H1 \/ the InternalRel of H2 by A138, A142, Def2;
then A212: [(f . 3),(f . 2)] in the InternalRel of H2 by A211, XBOOLE_0:def 3;
A213: 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;
suppose A215: [x,y] = [0,1] ; :: thesis: [(f . x),(f . y)] in the InternalRel of H2
then x = 0 by XTUPLE_0:1;
hence [(f . x),(f . y)] in the InternalRel of H2 by A196, A215, XTUPLE_0:1; :: thesis: verum
end;
suppose A216: [x,y] = [1,0] ; :: thesis: [(f . x),(f . y)] in the InternalRel of H2
then x = 1 by XTUPLE_0:1;
hence [(f . x),(f . y)] in the InternalRel of H2 by A193, A216, XTUPLE_0:1; :: thesis: verum
end;
suppose A217: [x,y] = [1,2] ; :: thesis: [(f . x),(f . y)] in the InternalRel of H2
then x = 1 by XTUPLE_0:1;
hence [(f . x),(f . y)] in the InternalRel of H2 by A207, A217, XTUPLE_0:1; :: thesis: verum
end;
suppose A218: [x,y] = [2,1] ; :: thesis: [(f . x),(f . y)] in the InternalRel of H2
then x = 2 by XTUPLE_0:1;
hence [(f . x),(f . y)] in the InternalRel of H2 by A210, A218, XTUPLE_0:1; :: thesis: verum
end;
suppose A219: [x,y] = [2,3] ; :: thesis: [(f . x),(f . y)] in the InternalRel of H2
then x = 2 by XTUPLE_0:1;
hence [(f . x),(f . y)] in the InternalRel of H2 by A209, A219, XTUPLE_0:1; :: thesis: verum
end;
suppose A220: [x,y] = [3,2] ; :: thesis: [(f . x),(f . y)] in the InternalRel of H2
then x = 3 by XTUPLE_0:1;
hence [(f . x),(f . y)] in the InternalRel of H2 by A212, A220, XTUPLE_0:1; :: thesis: verum
end;
end;
end;
thus ( [(f . x),(f . y)] in the InternalRel of H2 implies [x,y] in the InternalRel of (Necklace 4) ) :: thesis: verum
proof
( [(f . x),(f . y)] in the InternalRel of S implies [x,y] in the InternalRel of (Necklace 4) ) by A137;
then A221: ( [(f . x),(f . y)] in the InternalRel of H1 \/ the InternalRel of H2 implies [x,y] in the InternalRel of (Necklace 4) ) by A138, Def2;
assume [(f . x),(f . y)] in the InternalRel of H2 ; :: thesis: [x,y] in the InternalRel of (Necklace 4)
hence [x,y] in the InternalRel of (Necklace 4) by A221, XBOOLE_0:def 3; :: thesis: verum
end;
end;
A222: f . 3 in rng the InternalRel of H2 by A209, XTUPLE_0:def 13;
rng f c= the carrier of H2
proof
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng f or y in the carrier of H2 )
assume y in rng f ; :: thesis: y in the carrier of H2
then consider x being object such that
A223: x in dom f and
A224: y = f . x by FUNCT_1:def 3;
per cases ( x = 0 or x = 1 or x = 2 or x = 3 ) by A187, A223, Lm1, ENUMSET1:def 2;
suppose x = 0 ; :: thesis: y in the carrier of H2
hence y in the carrier of H2 by A186, A224; :: thesis: verum
end;
suppose x = 1 ; :: thesis: y in the carrier of H2
hence y in the carrier of H2 by A195, A197, A224; :: thesis: verum
end;
suppose x = 2 ; :: thesis: y in the carrier of H2
hence y in the carrier of H2 by A195, A208, A224; :: thesis: verum
end;
suppose x = 3 ; :: thesis: y in the carrier of H2
hence y in the carrier of H2 by A195, A222, A224; :: thesis: verum
end;
end;
end;
then f is Function of the carrier of (Necklace 4), the carrier of H2 by FUNCT_2:6;
then H2 embeds Necklace 4 by A136, A213, NECKLACE:def 1;
hence ex n being Nat st
( n < m & S1[n] ) by A5, A18, A194, A204; :: thesis: verum
end;
end;
end;
hence ex n being Nat st
( n < m & S1[n] ) by A19, A20; :: thesis: verum
end;
end;
end;
assume R embeds Necklace 4 ; :: according to NECKLA_2:def 1 :: thesis: contradiction
then S1[ card C] by A1;
then A225: ex i being Nat st S1[i] ;
S1[ 0 ] from NAT_1:sch 7(A225, A2);
 hence contradiction ; :: thesis: verum