let n be Nat; :: thesis: ( not Necklace n, ComplRelStr (Necklace n) are_isomorphic or n = 0 or n = 1 or n = 4 )
assume A1:
Necklace n, ComplRelStr (Necklace n) are_isomorphic
; :: thesis: ( n = 0 or n = 1 or n = 4 )
assume A2:
( not n = 0 & not n = 1 & not n = 4 )
; :: thesis: contradiction
per cases
( n = 2 or n = 3 or n > 4 )
by A2, NAT_1:29;
suppose A3:
n = 2
;
:: thesis: contradictionset S =
Necklace 2;
set T =
ComplRelStr (Necklace 2);
set X =
{[0 ,1],[1,0 ]};
set Y = the
InternalRel of
(Necklace 2);
A4:
card the
InternalRel of
(Necklace 2) =
2
* (2 - 1)
by Th28
.=
2
;
A5:
the
InternalRel of
(Necklace 2) = { [i,(i + 1)] where i is Element of NAT : i + 1 < 2 } \/ { [(i + 1),i] where i is Element of NAT : i + 1 < 2 }
by Th19;
A6:
[0 ,(0 + 1)] in { [i,(i + 1)] where i is Element of NAT : i + 1 < 2 }
;
A7:
[(0 + 1),0 ] in { [(i + 1),i] where i is Element of NAT : i + 1 < 2 }
;
A8:
{[0 ,1],[1,0 ]} c= the
InternalRel of
(Necklace 2)
A10:
the
InternalRel of
(Necklace 2) c= {[0 ,1],[1,0 ]}
then A17:
{[0 ,1],[1,0 ]} = the
InternalRel of
(Necklace 2)
by A8, XBOOLE_0:def 10;
the
InternalRel of
(ComplRelStr (Necklace 2)) is
empty
proof
assume
not the
InternalRel of
(ComplRelStr (Necklace 2)) is
empty
;
:: thesis: contradiction
then consider x being
set such that A18:
x in the
InternalRel of
(ComplRelStr (Necklace 2))
by XBOOLE_0:def 1;
x in (the InternalRel of (Necklace 2) ` ) \ (id the carrier of (Necklace 2))
by A18, Def9;
then A19:
(
x in the
InternalRel of
(Necklace 2) ` & not
x in id the
carrier of
(Necklace 2) )
by XBOOLE_0:def 5;
A20: the
carrier of
(Necklace 2) =
the
carrier of
(2 -SuccRelStr )
by Def8
.=
{0 ,1}
by Def7, CARD_1:88
;
A21:
id the
carrier of
(Necklace 2) = {[0 ,0 ],[1,1]}
proof
A22:
id the
carrier of
(Necklace 2) c= {[0 ,0 ],[1,1]}
proof
let x be
set ;
:: according to TARSKI:def 3 :: thesis: ( not x in id the carrier of (Necklace 2) or x in {[0 ,0 ],[1,1]} )
assume A23:
x in id the
carrier of
(Necklace 2)
;
:: thesis: x in {[0 ,0 ],[1,1]}
then consider x1,
x2 being
set such that A24:
x = [x1,x2]
by RELAT_1:def 1;
A25:
(
x1 in {0 ,1} &
x1 = x2 )
by A20, A23, A24, RELAT_1:def 10;
then
(
x1 = 0 or
x1 = 1 )
by TARSKI:def 2;
hence
x in {[0 ,0 ],[1,1]}
by A24, A25, TARSKI:def 2;
:: thesis: verum
end;
{[0 ,0 ],[1,1]} c= id the
carrier of
(Necklace 2)
proof
let x be
set ;
:: according to TARSKI:def 3 :: thesis: ( not x in {[0 ,0 ],[1,1]} or x in id the carrier of (Necklace 2) )
assume
x in {[0 ,0 ],[1,1]}
;
:: thesis: x in id the carrier of (Necklace 2)
then A26:
(
x = [0 ,0 ] or
x = [1,1] )
by TARSKI:def 2;
(
0 in the
carrier of
(Necklace 2) & 1
in the
carrier of
(Necklace 2) )
by A20, TARSKI:def 2;
hence
x in id the
carrier of
(Necklace 2)
by A26, RELAT_1:def 10;
:: thesis: verum
end;
hence
id the
carrier of
(Necklace 2) = {[0 ,0 ],[1,1]}
by A22, XBOOLE_0:def 10;
:: thesis: verum
end;
the
InternalRel of
(Necklace 2) ` = id the
carrier of
(Necklace 2)
proof
thus
the
InternalRel of
(Necklace 2) ` c= id the
carrier of
(Necklace 2)
:: according to XBOOLE_0:def 10 :: thesis: id the carrier of (Necklace 2) c= the InternalRel of (Necklace 2) ` proof
let x be
set ;
:: according to TARSKI:def 3 :: thesis: ( not x in the InternalRel of (Necklace 2) ` or x in id the carrier of (Necklace 2) )
assume
x in the
InternalRel of
(Necklace 2) `
;
:: thesis: x in id the carrier of (Necklace 2)
then A27:
(
x in [:the carrier of (Necklace 2),the carrier of (Necklace 2):] & not
x in the
InternalRel of
(Necklace 2) )
by XBOOLE_0:def 5;
then
x in {[0 ,0 ],[0 ,1],[1,0 ],[1,1]}
by A20, MCART_1:25;
then
(
x = [0 ,0 ] or
x = [0 ,1] or
x = [1,0 ] or
x = [1,1] )
by ENUMSET1:def 2;
hence
x in id the
carrier of
(Necklace 2)
by A17, A21, A27, TARSKI:def 2;
:: thesis: verum
end;
let x be
set ;
:: according to TARSKI:def 3 :: thesis: ( not x in id the carrier of (Necklace 2) or x in the InternalRel of (Necklace 2) ` )
assume A28:
x in id the
carrier of
(Necklace 2)
;
:: thesis: x in the InternalRel of (Necklace 2) `
then A29:
(
x = [0 ,0 ] or
x = [1,1] )
by A21, TARSKI:def 2;
not
x in the
InternalRel of
(Necklace 2)
then
(
x in {[0 ,0 ],[0 ,1],[1,0 ],[1,1]} & not
x in the
InternalRel of
(Necklace 2) )
by A29, ENUMSET1:def 2;
then
(
x in [:the carrier of (Necklace 2),the carrier of (Necklace 2):] & not
x in the
InternalRel of
(Necklace 2) )
by A20, MCART_1:25;
hence
x in the
InternalRel of
(Necklace 2) `
by XBOOLE_0:def 5;
:: thesis: verum
end;
hence
contradiction
by A19;
:: thesis: verum
end; hence
contradiction
by A1, A3, A4, Th18, CARD_1:47;
:: thesis: verum end; suppose A34:
n = 3
;
:: thesis: contradictionset S =
Necklace 3;
set T =
ComplRelStr (Necklace 3);
set X =
{[0 ,1],[1,0 ],[1,2],[2,1]};
set Y = the
InternalRel of
(Necklace 3);
A35:
the
carrier of
(Necklace 3) = {0 ,1,2}
by Th21, YELLOW11:1;
A36:
card the
InternalRel of
(Necklace 3) =
2
* (3 - 1)
by Th28
.=
4
;
A37:
the
InternalRel of
(Necklace 3) = { [i,(i + 1)] where i is Element of NAT : i + 1 < 3 } \/ { [(i + 1),i] where i is Element of NAT : i + 1 < 3 }
by Th19;
A38:
[0 ,(0 + 1)] in { [i,(i + 1)] where i is Element of NAT : i + 1 < 3 }
;
A39:
[(0 + 1),0 ] in { [(i + 1),i] where i is Element of NAT : i + 1 < 3 }
;
A40:
[(0 + 1),(1 + 1)] in { [i,(i + 1)] where i is Element of NAT : i + 1 < 3 }
;
A41:
[(1 + 1),(0 + 1)] in { [(i + 1),i] where i is Element of NAT : i + 1 < 3 }
;
A42:
{[0 ,1],[1,0 ],[1,2],[2,1]} c= the
InternalRel of
(Necklace 3)
proof
let x be
set ;
:: according to TARSKI:def 3 :: thesis: ( not x in {[0 ,1],[1,0 ],[1,2],[2,1]} or x in the InternalRel of (Necklace 3) )
assume A43:
x in {[0 ,1],[1,0 ],[1,2],[2,1]}
;
:: thesis: x in the InternalRel of (Necklace 3)
end;
the
InternalRel of
(Necklace 3) c= {[0 ,1],[1,0 ],[1,2],[2,1]}
proof
let x be
set ;
:: according to TARSKI:def 3 :: thesis: ( not x in the InternalRel of (Necklace 3) or x in {[0 ,1],[1,0 ],[1,2],[2,1]} )
assume A44:
x in the
InternalRel of
(Necklace 3)
;
:: thesis: x in {[0 ,1],[1,0 ],[1,2],[2,1]}
then consider y,
z being
set such that A45:
x = [y,z]
by RELAT_1:def 1;
per cases
( x in { [i,(i + 1)] where i is Element of NAT : i + 1 < 3 } or x in { [(i + 1),i] where i is Element of NAT : i + 1 < 3 } )
by A37, A44, XBOOLE_0:def 3;
suppose
x in { [i,(i + 1)] where i is Element of NAT : i + 1 < 3 }
;
:: thesis: x in {[0 ,1],[1,0 ],[1,2],[2,1]}then consider i being
Element of
NAT such that A46:
(
[y,z] = [i,(i + 1)] &
i + 1
< 3 )
by A45;
A47:
(
y = i &
z = i + 1 )
by A46, ZFMISC_1:33;
i + 1
< 1
+ 2
by A46;
then
i < 1
+ 1
by XREAL_1:9;
then
i <= 1
by NAT_1:13;
then
(
y = 0 or
y = 1 )
by A47, NAT_1:26;
hence
x in {[0 ,1],[1,0 ],[1,2],[2,1]}
by A45, A47, ENUMSET1:def 2;
:: thesis: verum end; suppose
x in { [(i + 1),i] where i is Element of NAT : i + 1 < 3 }
;
:: thesis: x in {[0 ,1],[1,0 ],[1,2],[2,1]}then consider i being
Element of
NAT such that A48:
(
[y,z] = [(i + 1),i] &
i + 1
< 3 )
by A45;
A49:
(
y = i + 1 &
z = i )
by A48, ZFMISC_1:33;
i + 1
< 1
+ 2
by A48;
then
i < 1
+ 1
by XREAL_1:9;
then
i <= 1
by NAT_1:13;
then
(
z = 0 or
z = 1 )
by A49, NAT_1:26;
hence
x in {[0 ,1],[1,0 ],[1,2],[2,1]}
by A45, A49, ENUMSET1:def 2;
:: thesis: verum end;
end; then A50:
{[0 ,1],[1,0 ],[1,2],[2,1]} = the
InternalRel of
(Necklace 3)
by A42, XBOOLE_0:def 10;
A51:
id the
carrier of
(Necklace 3) = {[0 ,0 ],[1,1],[2,2]}
proof
A52:
id the
carrier of
(Necklace 3) c= {[0 ,0 ],[1,1],[2,2]}
proof
let x be
set ;
:: according to TARSKI:def 3 :: thesis: ( not x in id the carrier of (Necklace 3) or x in {[0 ,0 ],[1,1],[2,2]} )
assume A53:
x in id the
carrier of
(Necklace 3)
;
:: thesis: x in {[0 ,0 ],[1,1],[2,2]}
then consider x1,
x2 being
set such that A54:
x = [x1,x2]
by RELAT_1:def 1;
A55:
(
x1 in {0 ,1,2} &
x1 = x2 )
by A35, A53, A54, RELAT_1:def 10;
then
(
x1 = 0 or
x1 = 1 or
x1 = 2 )
by ENUMSET1:def 1;
hence
x in {[0 ,0 ],[1,1],[2,2]}
by A54, A55, ENUMSET1:def 1;
:: thesis: verum
end;
{[0 ,0 ],[1,1],[2,2]} c= id the
carrier of
(Necklace 3)
proof
let x be
set ;
:: according to TARSKI:def 3 :: thesis: ( not x in {[0 ,0 ],[1,1],[2,2]} or x in id the carrier of (Necklace 3) )
assume A56:
x in {[0 ,0 ],[1,1],[2,2]}
;
:: thesis: x in id the carrier of (Necklace 3)
end;
hence
id the
carrier of
(Necklace 3) = {[0 ,0 ],[1,1],[2,2]}
by A52, XBOOLE_0:def 10;
:: thesis: verum
end; A59:
the
InternalRel of
(ComplRelStr (Necklace 3)) = (the InternalRel of (Necklace 3) ` ) \ (id the carrier of (Necklace 3))
by Def9;
A60:
[:the carrier of (Necklace 3),the carrier of (Necklace 3):] = {[0 ,0 ],[0 ,1],[0 ,2],[1,0 ],[1,1],[1,2],[2,0 ],[2,1],[2,2]}
by A35, Th3;
A61:
the
InternalRel of
(Necklace 3) ` = {[0 ,2],[2,0 ],[0 ,0 ],[1,1],[2,2]}
proof
thus
the
InternalRel of
(Necklace 3) ` c= {[0 ,2],[2,0 ],[0 ,0 ],[1,1],[2,2]}
:: according to XBOOLE_0:def 10 :: thesis: {[0 ,2],[2,0 ],[0 ,0 ],[1,1],[2,2]} c= the InternalRel of (Necklace 3) ` proof
let x be
set ;
:: according to TARSKI:def 3 :: thesis: ( not x in the InternalRel of (Necklace 3) ` or x in {[0 ,2],[2,0 ],[0 ,0 ],[1,1],[2,2]} )
assume
x in the
InternalRel of
(Necklace 3) `
;
:: thesis: x in {[0 ,2],[2,0 ],[0 ,0 ],[1,1],[2,2]}
then
(
x in {[0 ,0 ],[0 ,1],[0 ,2],[1,0 ],[1,1],[1,2],[2,0 ],[2,1],[2,2]} & not
x in {[0 ,1],[1,0 ],[1,2],[2,1]} )
by A42, A60, XBOOLE_0:def 5;
then
(
x in {[0 ,0 ],[0 ,1],[0 ,2],[1,0 ],[1,1],[1,2],[2,0 ],[2,1],[2,2]} &
x <> [0 ,1] &
x <> [1,0 ] &
x <> [1,2] &
x <> [2,1] )
by ENUMSET1:def 2;
then
(
x = [0 ,2] or
x = [2,0 ] or
x = [0 ,0 ] or
x = [1,1] or
x = [2,2] )
by ENUMSET1:def 7;
hence
x in {[0 ,2],[2,0 ],[0 ,0 ],[1,1],[2,2]}
by ENUMSET1:def 3;
:: thesis: verum
end;
let x be
set ;
:: according to TARSKI:def 3 :: thesis: ( not x in {[0 ,2],[2,0 ],[0 ,0 ],[1,1],[2,2]} or x in the InternalRel of (Necklace 3) ` )
assume
x in {[0 ,2],[2,0 ],[0 ,0 ],[1,1],[2,2]}
;
:: thesis: x in the InternalRel of (Necklace 3) `
then A62:
(
x = [0 ,2] or
x = [2,0 ] or
x = [0 ,0 ] or
x = [1,1] or
x = [2,2] )
by ENUMSET1:def 3;
then
(
x <> [0 ,1] &
x <> [1,0 ] &
x <> [1,2] &
x <> [2,1] )
by ZFMISC_1:33;
then A63:
not
x in {[0 ,1],[1,0 ],[1,2],[2,1]}
by ENUMSET1:def 2;
x in {[0 ,0 ],[0 ,1],[0 ,2],[1,0 ],[1,1],[1,2],[2,0 ],[2,1],[2,2]}
by A62, ENUMSET1:def 7;
hence
x in the
InternalRel of
(Necklace 3) `
by A50, A60, A63, XBOOLE_0:def 5;
:: thesis: verum
end; A64:
the
InternalRel of
(ComplRelStr (Necklace 3)) = {[0 ,2],[2,0 ]}
proof
thus
the
InternalRel of
(ComplRelStr (Necklace 3)) c= {[0 ,2],[2,0 ]}
:: according to XBOOLE_0:def 10 :: thesis: {[0 ,2],[2,0 ]} c= the InternalRel of (ComplRelStr (Necklace 3))proof
let x be
set ;
:: according to TARSKI:def 3 :: thesis: ( not x in the InternalRel of (ComplRelStr (Necklace 3)) or x in {[0 ,2],[2,0 ]} )
assume
x in the
InternalRel of
(ComplRelStr (Necklace 3))
;
:: thesis: x in {[0 ,2],[2,0 ]}
then A65:
(
x in {[0 ,2],[2,0 ],[0 ,0 ],[1,1],[2,2]} & not
x in {[0 ,0 ],[1,1],[2,2]} )
by A51, A59, A61, XBOOLE_0:def 5;
then
(
x = [0 ,2] or
x = [2,0 ] or
x = [0 ,0 ] or
x = [1,1] or
x = [2,2] )
by ENUMSET1:def 3;
hence
x in {[0 ,2],[2,0 ]}
by A65, ENUMSET1:def 1, TARSKI:def 2;
:: thesis: verum
end;
let x be
set ;
:: according to TARSKI:def 3 :: thesis: ( not x in {[0 ,2],[2,0 ]} or x in the InternalRel of (ComplRelStr (Necklace 3)) )
assume
x in {[0 ,2],[2,0 ]}
;
:: thesis: x in the InternalRel of (ComplRelStr (Necklace 3))
then A66:
(
x = [0 ,2] or
x = [2,0 ] )
by TARSKI:def 2;
then A67:
x in {[0 ,2],[2,0 ],[0 ,0 ],[1,1],[2,2]}
by ENUMSET1:def 3;
(
x <> [0 ,0 ] &
x <> [1,1] &
x <> [2,2] )
by A66, ZFMISC_1:33;
then
not
x in {[0 ,0 ],[1,1],[2,2]}
by ENUMSET1:def 1;
hence
x in the
InternalRel of
(ComplRelStr (Necklace 3))
by A51, A59, A61, A67, XBOOLE_0:def 5;
:: thesis: verum
end;
[0 ,2] <> [2,0 ]
by ZFMISC_1:33;
then
card the
InternalRel of
(ComplRelStr (Necklace 3)) = 2
by A64, CARD_2:76;
hence
contradiction
by A1, A34, A36, Th18;
:: thesis: verum end; suppose A68:
n > 4
;
:: thesis: contradictionset S =
Necklace n;
set T =
ComplRelStr (Necklace n);
A69:
the
carrier of
(Necklace n) = n
by Th21;
A70:
card the
InternalRel of
(Necklace n) = 2
* (n - 1)
by A68, Th28;
A71:
the
carrier of
(Necklace n) = n
by Th21;
card n = n
by CARD_1:def 5;
then
card [:n,n:] = n * n
by CARD_2:65;
then A72:
card (the InternalRel of (Necklace n) ` ) = (n * n) - (2 * (n - 1))
by A70, A71, CARD_2:63;
n = card n
by CARD_1:def 5;
then A73:
card (id the carrier of (Necklace n)) = n
by A69, Th6;
A74:
id the
carrier of
(Necklace n) misses the
InternalRel of
(Necklace n)
A80:
card the
InternalRel of
(ComplRelStr (Necklace n)) =
card ((the InternalRel of (Necklace n) ` ) \ (id the carrier of (Necklace n)))
by Def9
.=
((n * n) - (2 * (n - 1))) - n
by A72, A73, A74, CARD_2:63, XBOOLE_1:86
;
((n * n) - (2 * (n - 1))) - n <> 2
* (n - 1)
hence
contradiction
by A1, A70, A80, Th18;
:: thesis: verum end;