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 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 A4, Th6;
suppose A7: S is non empty trivial 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 2;
A11: the carrier of (Necklace 4) = {0 ,1,2,3} by NECKLACE:2, NECKLACE:21;
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:26;
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 RELAT_1:20;
f . 0 in dom the InternalRel of S by A14, RELAT_1:20;
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 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
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
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
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 A24, Th2, ENUMSET1:def 4;
end;
end;
A25: the carrier of (Necklace 4) = {0 ,1,2,3} by NECKLACE:2, NECKLACE:21;
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
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 A28, Th2, ENUMSET1:def 4;
end;
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 set ; :: 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 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 )
(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 2;
[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 RELAT_1:20;
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 RELAT_1:20;
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, RELAT_1:20;
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 RELAT_1:20;
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
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:106;
hence contradiction by A16, A55, XBOOLE_0:3; :: thesis: verum
end;
A57: now
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:106;
hence contradiction by A40, A26, A42, A23, A31; :: thesis: verum
end;
A59: now
assume [(f . 1),(f . 0 )] in the InternalRel of H2 ; :: thesis: contradiction
then f . 0 in rng the InternalRel of H2 by RELAT_1:20;
hence contradiction by A16, A45, A55, XBOOLE_0:3; :: thesis: verum
end;
A60: now
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:106;
hence contradiction by A16, A55, XBOOLE_0:3; :: thesis: verum
end;
A61: now
assume [(f . 0 ),(f . 1)] in the InternalRel of H2 ; :: thesis: contradiction
then f . 0 in dom the InternalRel of H2 by RELAT_1:20;
hence contradiction by A16, A54, A55, XBOOLE_0:3; :: thesis: verum
end;
A63: now
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:106;
hence contradiction by A40, A26, A34, A27, A31; :: thesis: verum
end;
then A64: f . 3 in the carrier of H1 by A47, XBOOLE_0:def 3;
A65: now
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 A64, ZFMISC_1:106;
hence contradiction by A40, A38, A34, A21, A35; :: thesis: verum
end;
A67: dom f = the carrier of (Necklace 4) by FUNCT_2:def 1;
rng f c= the carrier of H1
proof
let y be set ; :: 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 set such that
A68: x in dom f and
A69: y = f . x by FUNCT_1:def 5;
per cases ( x = 0 or x = 1 or x = 2 or x = 3 ) by A67, A68, Lm1, ENUMSET1:def 2;
suppose x = 0 ; :: thesis: y in the carrier of H1
hence y in the carrier of H1 by A55, A69; :: thesis: verum
end;
suppose x = 1 ; :: thesis: y in the carrier of H1
hence y in the carrier of H1 by A50, A65, A69, 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, A69, 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, A63, A69, XBOOLE_0:def 3; :: thesis: verum
end;
end;
end;
then A70: f is Function of the carrier of (Necklace 4),the carrier of H1 by FUNCT_2:8;
H1 is finite by A17, Th4;
then reconsider cH1 = the carrier of H1 as finite set ;
A71: H1 is non empty strict RelStr by A17, Th4;
A72: now
assume [(f . 3),(f . 2)] in the InternalRel of H2 ; :: thesis: contradiction
then f . 2 in rng the InternalRel of H2 by RELAT_1:20;
hence contradiction by A45, A57; :: thesis: verum
end;
A73: now
assume [(f . 2),(f . 3)] in the InternalRel of H2 ; :: thesis: contradiction
then f . 2 in dom the InternalRel of H2 by RELAT_1:20;
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 A76: [(f . 1),(f . 0 )] in the InternalRel of H1 by A59, A60, A65, ZFMISC_1:106, XBOOLE_0:def 3;
A77: now
assume [(f . 1),(f . 2)] in the InternalRel of H2 ; :: thesis: contradiction
then f . 1 in dom the InternalRel of H2 by RELAT_1:20;
hence contradiction by A54, A65; :: 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 A78: [(f . 1),(f . 2)] in the InternalRel of H1 by A77, A57, A65, ZFMISC_1:106, XBOOLE_0:def 3;
[(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 A82: [(f . 3),(f . 2)] in the InternalRel of H1 by A72, A57, A63, ZFMISC_1:106, XBOOLE_0:def 3;
[(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 A85: [(f . 2),(f . 3)] in the InternalRel of H1 by A73, A63, A57, ZFMISC_1:106, XBOOLE_0:def 3;
A86: now
assume [(f . 2),(f . 1)] in the InternalRel of H2 ; :: thesis: contradiction
then f . 1 in rng the InternalRel of H2 by RELAT_1:20;
hence contradiction by A45, A65; :: 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 ;
A87: not H2 is empty by A18, Th4;
A88: cH1 <> cS
proof
A89: cS = cH1 \/ cH2 by A30, Def3;
assume A90: cH1 = cS ; :: thesis: contradiction
consider x being set such that
A91: x in cH2 by A87, XBOOLE_0:def 1;
cH1 /\ cH2 = {} by A16, XBOOLE_0:def 7;
then not x in cH1 by A91, XBOOLE_0:def 4;
hence contradiction by A90, A89, A91, 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 A88, XBOOLE_0:def 8;
then A92: card cH1 < card cS by CARD_2:67;
[(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 A93: [(f . 2),(f . 1)] in the InternalRel of H1 by A86, A65, A57, ZFMISC_1:106, XBOOLE_0:def 3;
[(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 A94: [(f . 0 ),(f . 1)] in the InternalRel of H1 by A61, A65, ZFMISC_1:106, A56, XBOOLE_0:def 3;
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 A95: [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 A95, Th2, ENUMSET1:def 4;
suppose A96: [x,y] = [0 ,1] ; :: thesis: [(f . x),(f . y)] in the InternalRel of H1
then x = 0 by ZFMISC_1:33;
hence [(f . x),(f . y)] in the InternalRel of H1 by A94, A96, ZFMISC_1:33; :: thesis: verum
end;
suppose A97: [x,y] = [1,0 ] ; :: thesis: [(f . x),(f . y)] in the InternalRel of H1
then x = 1 by ZFMISC_1:33;
hence [(f . x),(f . y)] in the InternalRel of H1 by A76, A97, ZFMISC_1:33; :: thesis: verum
end;
suppose A98: [x,y] = [1,2] ; :: thesis: [(f . x),(f . y)] in the InternalRel of H1
then x = 1 by ZFMISC_1:33;
hence [(f . x),(f . y)] in the InternalRel of H1 by A78, A98, ZFMISC_1:33; :: thesis: verum
end;
suppose A99: [x,y] = [2,1] ; :: thesis: [(f . x),(f . y)] in the InternalRel of H1
then x = 2 by ZFMISC_1:33;
hence [(f . x),(f . y)] in the InternalRel of H1 by A93, A99, ZFMISC_1:33; :: thesis: verum
end;
suppose A100: [x,y] = [2,3] ; :: thesis: [(f . x),(f . y)] in the InternalRel of H1
then x = 2 by ZFMISC_1:33;
hence [(f . x),(f . y)] in the InternalRel of H1 by A85, A100, ZFMISC_1:33; :: thesis: verum
end;
suppose A101: [x,y] = [3,2] ; :: thesis: [(f . x),(f . y)] in the InternalRel of H1
then x = 3 by ZFMISC_1:33;
hence [(f . x),(f . y)] in the InternalRel of H1 by A82, A101, ZFMISC_1:33; :: 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 A102: ( [(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 A102, XBOOLE_0:def 3; :: thesis: verum
end;
end;
then H1 embeds Necklace 4 by A39, A70, NECKLACE:def 2;
hence ex n being Nat st
( n < m & S1[n] ) by A5, A17, A71, A92; :: thesis: verum
end;
suppose A103: 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)];
A104: now
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:106;
hence contradiction by A16, A103, XBOOLE_0:3; :: thesis: verum
end;
A105: now
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:106;
hence contradiction by A16, A103, XBOOLE_0:3; :: thesis: verum
end;
A106: now
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 A103, ZFMISC_1:106;
hence contradiction by A40, A26, A34, A27, A35; :: thesis: verum
end;
then A107: f . 3 in the carrier of H2 by A47, XBOOLE_0:def 3;
A108: now
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 A107, ZFMISC_1:106;
hence contradiction by A40, A38, A34, A21, A31; :: thesis: verum
end;
A112: now
assume [(f . 1),(f . 0 )] in the InternalRel of H1 ; :: thesis: contradiction
then f . 1 in dom the InternalRel of H1 by RELAT_1:20;
hence contradiction by A51, A108; :: 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 A113: [(f . 1),(f . 0 )] in the InternalRel of H2 by A112, A108, ZFMISC_1:106, A105, XBOOLE_0:def 3;
A114: now
assume [(f . 2),(f . 1)] in the InternalRel of H1 ; :: thesis: contradiction
then f . 1 in rng the InternalRel of H1 by RELAT_1:20;
hence contradiction by A37, A108; :: thesis: verum
end;
A115: now
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 A103, ZFMISC_1:106;
hence contradiction by A40, A26, A42, A23, A35; :: thesis: verum
end;
A117: dom f = the carrier of (Necklace 4) by FUNCT_2:def 1;
rng f c= the carrier of H2
proof
let y be set ; :: 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 set such that
A118: x in dom f and
A119: y = f . x by FUNCT_1:def 5;
per cases ( x = 0 or x = 1 or x = 2 or x = 3 ) by A117, A118, Lm1, ENUMSET1:def 2;
suppose x = 0 ; :: thesis: y in the carrier of H2
hence y in the carrier of H2 by A103, A119; :: thesis: verum
end;
suppose x = 1 ; :: thesis: y in the carrier of H2
hence y in the carrier of H2 by A50, A108, A119, 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, A115, A119, 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, A106, A119, XBOOLE_0:def 3; :: thesis: verum
end;
end;
end;
then A120: f is Function of the carrier of (Necklace 4),the carrier of H2 by FUNCT_2:8;
H1 is finite by A17, Th4;
then reconsider cH1 = the carrier of H1 as finite set ;
A121: H2 is non empty strict RelStr by A18, Th4;
A122: now
assume [(f . 0 ),(f . 1)] in the InternalRel of H1 ; :: thesis: contradiction
then f . 0 in dom the InternalRel of H1 by RELAT_1:20;
hence contradiction by A16, A51, A103, XBOOLE_0:3; :: thesis: verum
end;
A124: now
assume [(f . 3),(f . 2)] in the InternalRel of H1 ; :: thesis: contradiction
then f . 2 in rng the InternalRel of H1 by RELAT_1:20;
hence contradiction by A37, A115; :: thesis: verum
end;
A125: now
assume [(f . 2),(f . 3)] in the InternalRel of H1 ; :: thesis: contradiction
then f . 2 in dom the InternalRel of H1 by RELAT_1:20;
hence contradiction by A51, A115; :: 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 A127: [(f . 3),(f . 2)] in the InternalRel of H2 by A124, A106, ZFMISC_1:106, A115, XBOOLE_0:def 3;
A130: now
assume [(f . 1),(f . 2)] in the InternalRel of H1 ; :: thesis: contradiction
then f . 2 in rng the InternalRel of H1 by RELAT_1:20;
hence contradiction by A37, A115; :: 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 A131: [(f . 1),(f . 2)] in the InternalRel of H2 by A130, A108, A115, ZFMISC_1:106, XBOOLE_0:def 3;
[(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 A134: [(f . 2),(f . 3)] in the InternalRel of H2 by A125, A115, A106, ZFMISC_1:106, XBOOLE_0:def 3;
[(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 A135: [(f . 2),(f . 1)] in the InternalRel of H2 by A114, A115, A108, ZFMISC_1:106, XBOOLE_0:def 3;
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 ;
A136: not H1 is empty by A17, Th4;
A137: cH2 <> cS
proof
A138: cS = cH1 \/ cH2 by A30, Def3;
assume A139: cH2 = cS ; :: thesis: contradiction
consider x being set such that
A140: x in cH1 by A136, XBOOLE_0:def 1;
cH1 /\ cH2 = {} by A16, XBOOLE_0:def 7;
then not x in cH2 by A140, XBOOLE_0:def 4;
hence contradiction by A139, A138, A140, 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 A137, XBOOLE_0:def 8;
then A141: card cH2 < card cS by CARD_2:67;
[(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 A142: [(f . 0 ),(f . 1)] in the InternalRel of H2 by A122, A104, A108, ZFMISC_1:106, XBOOLE_0:def 3;
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 A143: [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 A143, Th2, ENUMSET1:def 4;
suppose A144: [x,y] = [0 ,1] ; :: thesis: [(f . x),(f . y)] in the InternalRel of H2
then x = 0 by ZFMISC_1:33;
hence [(f . x),(f . y)] in the InternalRel of H2 by A142, A144, ZFMISC_1:33; :: thesis: verum
end;
suppose A145: [x,y] = [1,0 ] ; :: thesis: [(f . x),(f . y)] in the InternalRel of H2
then x = 1 by ZFMISC_1:33;
hence [(f . x),(f . y)] in the InternalRel of H2 by A113, A145, ZFMISC_1:33; :: thesis: verum
end;
suppose A146: [x,y] = [1,2] ; :: thesis: [(f . x),(f . y)] in the InternalRel of H2
then x = 1 by ZFMISC_1:33;
hence [(f . x),(f . y)] in the InternalRel of H2 by A131, A146, ZFMISC_1:33; :: thesis: verum
end;
suppose A147: [x,y] = [2,1] ; :: thesis: [(f . x),(f . y)] in the InternalRel of H2
then x = 2 by ZFMISC_1:33;
hence [(f . x),(f . y)] in the InternalRel of H2 by A135, A147, ZFMISC_1:33; :: thesis: verum
end;
suppose A148: [x,y] = [2,3] ; :: thesis: [(f . x),(f . y)] in the InternalRel of H2
then x = 2 by ZFMISC_1:33;
hence [(f . x),(f . y)] in the InternalRel of H2 by A134, A148, ZFMISC_1:33; :: thesis: verum
end;
suppose A149: [x,y] = [3,2] ; :: thesis: [(f . x),(f . y)] in the InternalRel of H2
then x = 3 by ZFMISC_1:33;
hence [(f . x),(f . y)] in the InternalRel of H2 by A127, A149, ZFMISC_1:33; :: 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 A150: ( [(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 A150, XBOOLE_0:def 3; :: thesis: verum
end;
end;
then H2 embeds Necklace 4 by A39, A120, NECKLACE:def 2;
hence ex n being Nat st
( n < m & S1[n] ) by A5, A18, A121, A141; :: thesis: verum
end;
end;
end;
now
A151: the carrier of (Necklace 4) = {0 ,1,2,3} by NECKLACE:2, NECKLACE:21;
then A152: 0 in the carrier of (Necklace 4) by ENUMSET1:def 2;
A153: 3 in the carrier of (Necklace 4) by A151, ENUMSET1:def 2;
A154: 1 in the carrier of (Necklace 4) by A151, ENUMSET1:def 2;
A155: 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
A156: f is one-to-one and
A157: 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 2;
assume A158: 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 A159: [(f . 0 ),(f . 1)] in the InternalRel of S by A157, A152, A154;
then f . 0 in dom the InternalRel of S by RELAT_1:20;
then f . 0 in the carrier of S by A155;
then A160: f . 0 in the carrier of H1 \/ the carrier of H2 by A158, Def2;
A161: 2 in the carrier of (Necklace 4) by A151, ENUMSET1:def 2;
[3,2] in the InternalRel of (Necklace 4) by Th2, ENUMSET1:def 4;
then A162: [(f . 3),(f . 2)] in the InternalRel of S by A157, A161, A153;
[2,3] in the InternalRel of (Necklace 4) by Th2, ENUMSET1:def 4;
then A163: [(f . 2),(f . 3)] in the InternalRel of S by A157, A161, A153;
[2,1] in the InternalRel of (Necklace 4) by Th2, ENUMSET1:def 4;
then A164: [(f . 2),(f . 1)] in the InternalRel of S by A157, A154, A161;
[1,2] in the InternalRel of (Necklace 4) by Th2, ENUMSET1:def 4;
then A165: [(f . 1),(f . 2)] in the InternalRel of S by A157, A154, A161;
[1,0 ] in the InternalRel of (Necklace 4) by Th2, ENUMSET1:def 4;
then A166: [(f . 1),(f . 0 )] in the InternalRel of S by A157, A152, A154;
per cases ( f . 0 in the carrier of H1 or f . 0 in the carrier of H2 ) by A160, XBOOLE_0:def 3;
suppose A167: 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;
A168: 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 ;
A169: the carrier of S = cH1 \/ cH2 by A158, Def2;
A170: dom the InternalRel of H2 c= the carrier of H2 by RELAT_1:def 18;
A171: now
assume [(f . 0 ),(f . 1)] in the InternalRel of H2 ; :: thesis: contradiction
then f . 0 in dom the InternalRel of H2 by RELAT_1:20;
hence contradiction by A16, A167, A170, XBOOLE_0:3; :: thesis: verum
end;
A172: rng the InternalRel of H2 c= the carrier of H2 by RELAT_1:def 19;
A173: now
assume [(f . 1),(f . 0 )] in the InternalRel of H2 ; :: thesis: contradiction
then f . 0 in rng the InternalRel of H2 by RELAT_1:20;
hence contradiction by A16, A167, A172, XBOOLE_0:3; :: thesis: verum
end;
[(f . 1),(f . 0 )] in the InternalRel of H1 \/ the InternalRel of H2 by A158, A166, Def2;
then A174: [(f . 1),(f . 0 )] in the InternalRel of H1 by A173, XBOOLE_0:def 3;
A175: H1 is non empty strict RelStr by A17, Th4;
reconsider cS = the carrier of S as finite set by A169;
A176: 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 A158, A159, Def2;
then A177: [(f . 0 ),(f . 1)] in the InternalRel of H1 by A171, XBOOLE_0:def 3;
then A178: f . 1 in rng the InternalRel of H1 by RELAT_1:20;
A179: now
assume [(f . 2),(f . 1)] in the InternalRel of H2 ; :: thesis: contradiction
then f . 1 in rng the InternalRel of H2 by RELAT_1:20;
hence contradiction by A16, A176, A172, A178, XBOOLE_0:3; :: thesis: verum
end;
A180: not H2 is empty by A18, Th4;
A181: cH1 <> cS
proof
A182: cS = cH1 \/ cH2 by A158, Def2;
assume A183: cH1 = cS ; :: thesis: contradiction
consider x being set such that
A184: x in cH2 by A180, XBOOLE_0:def 1;
cH1 /\ cH2 = {} by A16, XBOOLE_0:def 7;
then not x in cH1 by A184, XBOOLE_0:def 4;
hence contradiction by A183, A182, A184, XBOOLE_0:def 3; :: thesis: verum
end;
cS = cH1 \/ cH2 by A158, Def2;
then cH1 c= cS by XBOOLE_1:7;
then cH1 c< cS by A181, XBOOLE_0:def 8;
then A185: card cH1 < card cS by CARD_2:67;
A186: [(f . 2),(f . 3)] in the InternalRel of H1 \/ the InternalRel of H2 by A158, A163, Def2;
A187: [(f . 1),(f . 2)] in the InternalRel of H1 \/ the InternalRel of H2 by A158, A165, Def2;
now
assume [(f . 1),(f . 2)] in the InternalRel of H2 ; :: thesis: contradiction
then f . 1 in dom the InternalRel of H2 by RELAT_1:20;
hence contradiction by A16, A176, A170, A178, XBOOLE_0:3; :: thesis: verum
end;
then A188: [(f . 1),(f . 2)] in the InternalRel of H1 by A187, XBOOLE_0:def 3;
then A189: f . 2 in rng the InternalRel of H1 by RELAT_1:20;
now
assume [(f . 2),(f . 3)] in the InternalRel of H2 ; :: thesis: contradiction
then f . 2 in dom the InternalRel of H2 by RELAT_1:20;
hence contradiction by A16, A176, A170, A189, XBOOLE_0:3; :: thesis: verum
end;
then A190: [(f . 2),(f . 3)] in the InternalRel of H1 by A186, XBOOLE_0:def 3;
[(f . 2),(f . 1)] in the InternalRel of H1 \/ the InternalRel of H2 by A158, A164, Def2;
then A191: [(f . 2),(f . 1)] in the InternalRel of H1 by A179, XBOOLE_0:def 3;
A192: now
assume [(f . 3),(f . 2)] in the InternalRel of H2 ; :: thesis: contradiction
then f . 2 in rng the InternalRel of H2 by RELAT_1:20;
hence contradiction by A16, A176, A172, A189, XBOOLE_0:3; :: thesis: verum
end;
[(f . 3),(f . 2)] in the InternalRel of H1 \/ the InternalRel of H2 by A158, A162, Def2;
then A193: [(f . 3),(f . 2)] in the InternalRel of H1 by A192, XBOOLE_0:def 3;
A194: 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 A195: [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 A195, Th2, ENUMSET1:def 4;
suppose A196: [x,y] = [0 ,1] ; :: thesis: [(f . x),(f . y)] in the InternalRel of H1
then x = 0 by ZFMISC_1:33;
hence [(f . x),(f . y)] in the InternalRel of H1 by A177, A196, ZFMISC_1:33; :: thesis: verum
end;
suppose A197: [x,y] = [1,0 ] ; :: thesis: [(f . x),(f . y)] in the InternalRel of H1
then x = 1 by ZFMISC_1:33;
hence [(f . x),(f . y)] in the InternalRel of H1 by A174, A197, ZFMISC_1:33; :: thesis: verum
end;
suppose A198: [x,y] = [1,2] ; :: thesis: [(f . x),(f . y)] in the InternalRel of H1
then x = 1 by ZFMISC_1:33;
hence [(f . x),(f . y)] in the InternalRel of H1 by A188, A198, ZFMISC_1:33; :: thesis: verum
end;
suppose A199: [x,y] = [2,1] ; :: thesis: [(f . x),(f . y)] in the InternalRel of H1
then x = 2 by ZFMISC_1:33;
hence [(f . x),(f . y)] in the InternalRel of H1 by A191, A199, ZFMISC_1:33; :: thesis: verum
end;
suppose A200: [x,y] = [2,3] ; :: thesis: [(f . x),(f . y)] in the InternalRel of H1
then x = 2 by ZFMISC_1:33;
hence [(f . x),(f . y)] in the InternalRel of H1 by A190, A200, ZFMISC_1:33; :: thesis: verum
end;
suppose A201: [x,y] = [3,2] ; :: thesis: [(f . x),(f . y)] in the InternalRel of H1
then x = 3 by ZFMISC_1:33;
hence [(f . x),(f . y)] in the InternalRel of H1 by A193, A201, ZFMISC_1:33; :: 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 A157;
then A202: ( [(f . x),(f . y)] in the InternalRel of H1 \/ the InternalRel of H2 implies [x,y] in the InternalRel of (Necklace 4) ) by A158, 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 A202, XBOOLE_0:def 3; :: thesis: verum
end;
end;
A203: f . 3 in rng the InternalRel of H1 by A190, RELAT_1:20;
rng f c= the carrier of H1
proof
let y be set ; :: 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 set such that
A204: x in dom f and
A205: y = f . x by FUNCT_1:def 5;
per cases ( x = 0 or x = 1 or x = 2 or x = 3 ) by A168, A204, Lm1, ENUMSET1:def 2;
suppose x = 0 ; :: thesis: y in the carrier of H1
hence y in the carrier of H1 by A167, A205; :: thesis: verum
end;
suppose x = 1 ; :: thesis: y in the carrier of H1
hence y in the carrier of H1 by A176, A178, A205; :: thesis: verum
end;
suppose x = 2 ; :: thesis: y in the carrier of H1
hence y in the carrier of H1 by A176, A189, A205; :: thesis: verum
end;
suppose x = 3 ; :: thesis: y in the carrier of H1
hence y in the carrier of H1 by A176, A203, A205; :: thesis: verum
end;
end;
end;
then f is Function of the carrier of (Necklace 4),the carrier of H1 by FUNCT_2:8;
then H1 embeds Necklace 4 by A156, A194, NECKLACE:def 2;
hence ex n being Nat st
( n < m & S1[n] ) by A5, A17, A175, A185; :: thesis: verum
end;
suppose A206: 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;
A207: 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 ;
A208: the carrier of S = cH1 \/ cH2 by A158, Def2;
A209: dom the InternalRel of H1 c= the carrier of H1 by RELAT_1:def 18;
A210: now
assume [(f . 0 ),(f . 1)] in the InternalRel of H1 ; :: thesis: contradiction
then f . 0 in dom the InternalRel of H1 by RELAT_1:20;
hence contradiction by A16, A206, A209, XBOOLE_0:3; :: thesis: verum
end;
A211: rng the InternalRel of H1 c= the carrier of H1 by RELAT_1:def 19;
A212: now
assume [(f . 1),(f . 0 )] in the InternalRel of H1 ; :: thesis: contradiction
then f . 0 in rng the InternalRel of H1 by RELAT_1:20;
hence contradiction by A16, A206, A211, XBOOLE_0:3; :: thesis: verum
end;
[(f . 1),(f . 0 )] in the InternalRel of H1 \/ the InternalRel of H2 by A158, A166, Def2;
then A213: [(f . 1),(f . 0 )] in the InternalRel of H2 by A212, XBOOLE_0:def 3;
A214: H2 is non empty strict RelStr by A18, Th4;
reconsider cS = the carrier of S as finite set by A208;
A215: 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 A158, A159, Def2;
then A216: [(f . 0 ),(f . 1)] in the InternalRel of H2 by A210, XBOOLE_0:def 3;
then A217: f . 1 in rng the InternalRel of H2 by RELAT_1:20;
A218: now
assume [(f . 2),(f . 1)] in the InternalRel of H1 ; :: thesis: contradiction
then f . 1 in rng the InternalRel of H1 by RELAT_1:20;
hence contradiction by A16, A215, A211, A217, XBOOLE_0:3; :: thesis: verum
end;
A219: not H1 is empty by A17, Th4;
A220: cH2 <> cS
proof
A221: cS = cH1 \/ cH2 by A158, Def2;
assume A222: cH2 = cS ; :: thesis: contradiction
consider x being set such that
A223: x in cH1 by A219, XBOOLE_0:def 1;
cH1 /\ cH2 = {} by A16, XBOOLE_0:def 7;
then not x in cH2 by A223, XBOOLE_0:def 4;
hence contradiction by A222, A221, A223, XBOOLE_0:def 3; :: thesis: verum
end;
cS = cH1 \/ cH2 by A158, Def2;
then cH2 c= cS by XBOOLE_1:7;
then cH2 c< cS by A220, XBOOLE_0:def 8;
then A224: card cH2 < card cS by CARD_2:67;
A225: [(f . 2),(f . 3)] in the InternalRel of H1 \/ the InternalRel of H2 by A158, A163, Def2;
A226: [(f . 1),(f . 2)] in the InternalRel of H1 \/ the InternalRel of H2 by A158, A165, Def2;
now
assume [(f . 1),(f . 2)] in the InternalRel of H1 ; :: thesis: contradiction
then f . 1 in dom the InternalRel of H1 by RELAT_1:20;
hence contradiction by A16, A215, A209, A217, XBOOLE_0:3; :: thesis: verum
end;
then A227: [(f . 1),(f . 2)] in the InternalRel of H2 by A226, XBOOLE_0:def 3;
then A228: f . 2 in rng the InternalRel of H2 by RELAT_1:20;
now
assume [(f . 2),(f . 3)] in the InternalRel of H1 ; :: thesis: contradiction
then f . 2 in dom the InternalRel of H1 by RELAT_1:20;
hence contradiction by A16, A215, A209, A228, XBOOLE_0:3; :: thesis: verum
end;
then A229: [(f . 2),(f . 3)] in the InternalRel of H2 by A225, XBOOLE_0:def 3;
[(f . 2),(f . 1)] in the InternalRel of H1 \/ the InternalRel of H2 by A158, A164, Def2;
then A230: [(f . 2),(f . 1)] in the InternalRel of H2 by A218, XBOOLE_0:def 3;
A231: now
assume [(f . 3),(f . 2)] in the InternalRel of H1 ; :: thesis: contradiction
then f . 2 in rng the InternalRel of H1 by RELAT_1:20;
hence contradiction by A16, A215, A211, A228, XBOOLE_0:3; :: thesis: verum
end;
[(f . 3),(f . 2)] in the InternalRel of H1 \/ the InternalRel of H2 by A158, A162, Def2;
then A232: [(f . 3),(f . 2)] in the InternalRel of H2 by A231, XBOOLE_0:def 3;
A233: 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 A234: [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 A234, Th2, ENUMSET1:def 4;
suppose A235: [x,y] = [0 ,1] ; :: thesis: [(f . x),(f . y)] in the InternalRel of H2
then x = 0 by ZFMISC_1:33;
hence [(f . x),(f . y)] in the InternalRel of H2 by A216, A235, ZFMISC_1:33; :: thesis: verum
end;
suppose A236: [x,y] = [1,0 ] ; :: thesis: [(f . x),(f . y)] in the InternalRel of H2
then x = 1 by ZFMISC_1:33;
hence [(f . x),(f . y)] in the InternalRel of H2 by A213, A236, ZFMISC_1:33; :: thesis: verum
end;
suppose A237: [x,y] = [1,2] ; :: thesis: [(f . x),(f . y)] in the InternalRel of H2
then x = 1 by ZFMISC_1:33;
hence [(f . x),(f . y)] in the InternalRel of H2 by A227, A237, ZFMISC_1:33; :: thesis: verum
end;
suppose A238: [x,y] = [2,1] ; :: thesis: [(f . x),(f . y)] in the InternalRel of H2
then x = 2 by ZFMISC_1:33;
hence [(f . x),(f . y)] in the InternalRel of H2 by A230, A238, ZFMISC_1:33; :: thesis: verum
end;
suppose A239: [x,y] = [2,3] ; :: thesis: [(f . x),(f . y)] in the InternalRel of H2
then x = 2 by ZFMISC_1:33;
hence [(f . x),(f . y)] in the InternalRel of H2 by A229, A239, ZFMISC_1:33; :: thesis: verum
end;
suppose A240: [x,y] = [3,2] ; :: thesis: [(f . x),(f . y)] in the InternalRel of H2
then x = 3 by ZFMISC_1:33;
hence [(f . x),(f . y)] in the InternalRel of H2 by A232, A240, ZFMISC_1:33; :: 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 A157;
then A241: ( [(f . x),(f . y)] in the InternalRel of H1 \/ the InternalRel of H2 implies [x,y] in the InternalRel of (Necklace 4) ) by A158, 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 A241, XBOOLE_0:def 3; :: thesis: verum
end;
end;
A242: f . 3 in rng the InternalRel of H2 by A229, RELAT_1:20;
rng f c= the carrier of H2
proof
let y be set ; :: 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 set such that
A243: x in dom f and
A244: y = f . x by FUNCT_1:def 5;
per cases ( x = 0 or x = 1 or x = 2 or x = 3 ) by A207, A243, Lm1, ENUMSET1:def 2;
suppose x = 0 ; :: thesis: y in the carrier of H2
hence y in the carrier of H2 by A206, A244; :: thesis: verum
end;
suppose x = 1 ; :: thesis: y in the carrier of H2
hence y in the carrier of H2 by A215, A217, A244; :: thesis: verum
end;
suppose x = 2 ; :: thesis: y in the carrier of H2
hence y in the carrier of H2 by A215, A228, A244; :: thesis: verum
end;
suppose x = 3 ; :: thesis: y in the carrier of H2
hence y in the carrier of H2 by A215, A242, A244; :: thesis: verum
end;
end;
end;
then f is Function of the carrier of (Necklace 4),the carrier of H2 by FUNCT_2:8;
then H2 embeds Necklace 4 by A156, A233, NECKLACE:def 2;
hence ex n being Nat st
( n < m & S1[n] ) by A5, A18, A214, A224; :: 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 A245: ex i being Nat st S1[i] ;
S1[ 0 ] from NAT_1:sch 7(A245, A2);
 hence contradiction ; :: thesis: verum