:: NECKLACE semantic presentation begin theorem :: NECKLACE:1 4 = {0,1,2,3} by CARD_1:52; theorem :: NECKLACE:2 for x1, x2, x3, y1, y2, y3 being set holds [:{x1,x2,x3},{y1,y2,y3}:] = {[x1,y1],[x1,y2],[x1,y3],[x2,y1],[x2,y2],[x2,y3],[x3,y1],[x3,y2],[x3,y3]} proof let x1, x2, x3, y1, y2, y3 be set ; ::_thesis: [:{x1,x2,x3},{y1,y2,y3}:] = {[x1,y1],[x1,y2],[x1,y3],[x2,y1],[x2,y2],[x2,y3],[x3,y1],[x3,y2],[x3,y3]} thus [:{x1,x2,x3},{y1,y2,y3}:] = [:({x1} \/ {x2,x3}),{y1,y2,y3}:] by ENUMSET1:2 .= [:({x1} \/ {x2,x3}),({y1} \/ {y2,y3}):] by ENUMSET1:2 .= (([:{x1},{y1}:] \/ [:{x1},{y2,y3}:]) \/ [:{x2,x3},{y1}:]) \/ [:{x2,x3},{y2,y3}:] by ZFMISC_1:98 .= (([:{x1},{y1}:] \/ [:{x1},{y2,y3}:]) \/ [:{x2,x3},{y1}:]) \/ ([:{x2},{y2,y3}:] \/ [:{x3},{y2,y3}:]) by ZFMISC_1:109 .= (({[x1,y1]} \/ [:{x1},{y2,y3}:]) \/ [:{x2,x3},{y1}:]) \/ ([:{x2},{y2,y3}:] \/ [:{x3},{y2,y3}:]) by ZFMISC_1:29 .= (({[x1,y1]} \/ {[x1,y2],[x1,y3]}) \/ [:{x2,x3},{y1}:]) \/ ([:{x2},{y2,y3}:] \/ [:{x3},{y2,y3}:]) by ZFMISC_1:30 .= (({[x1,y1]} \/ {[x1,y2],[x1,y3]}) \/ {[x2,y1],[x3,y1]}) \/ ([:{x2},{y2,y3}:] \/ [:{x3},{y2,y3}:]) by ZFMISC_1:30 .= (({[x1,y1]} \/ {[x1,y2],[x1,y3]}) \/ {[x2,y1],[x3,y1]}) \/ ({[x2,y2],[x2,y3]} \/ [:{x3},{y2,y3}:]) by ZFMISC_1:30 .= (({[x1,y1]} \/ {[x1,y2],[x1,y3]}) \/ {[x2,y1],[x3,y1]}) \/ ({[x2,y2],[x2,y3]} \/ {[x3,y2],[x3,y3]}) by ZFMISC_1:30 .= ({[x1,y1],[x1,y2],[x1,y3]} \/ {[x2,y1],[x3,y1]}) \/ ({[x2,y2],[x2,y3]} \/ {[x3,y2],[x3,y3]}) by ENUMSET1:2 .= {[x1,y1],[x1,y2],[x1,y3],[x2,y1],[x3,y1]} \/ ({[x2,y2],[x2,y3]} \/ {[x3,y2],[x3,y3]}) by ENUMSET1:9 .= {[x1,y1],[x1,y2],[x1,y3],[x2,y1],[x3,y1]} \/ {[x2,y2],[x2,y3],[x3,y2],[x3,y3]} by ENUMSET1:5 .= {[x1,y1],[x1,y2],[x1,y3],[x2,y1],[x3,y1],[x2,y2],[x2,y3],[x3,y2],[x3,y3]} by ENUMSET1:81 .= {[x1,y1],[x1,y2],[x1,y3],[x2,y1]} \/ {[x3,y1],[x2,y2],[x2,y3],[x3,y2],[x3,y3]} by ENUMSET1:80 .= {[x1,y1],[x1,y2],[x1,y3],[x2,y1]} \/ ({[x3,y1],[x2,y2],[x2,y3]} \/ {[x3,y2],[x3,y3]}) by ENUMSET1:9 .= {[x1,y1],[x1,y2],[x1,y3],[x2,y1]} \/ ({[x2,y2],[x2,y3],[x3,y1]} \/ {[x3,y2],[x3,y3]}) by ENUMSET1:59 .= {[x1,y1],[x1,y2],[x1,y3],[x2,y1]} \/ {[x2,y2],[x2,y3],[x3,y1],[x3,y2],[x3,y3]} by ENUMSET1:9 .= {[x1,y1],[x1,y2],[x1,y3],[x2,y1],[x2,y2],[x2,y3],[x3,y1],[x3,y2],[x3,y3]} by ENUMSET1:80 ; ::_thesis: verum end; theorem Th3: :: NECKLACE:3 for x being set for n being Nat st x in n holds x is Nat proof let x be set ; ::_thesis: for n being Nat st x in n holds x is Nat let n be Nat; ::_thesis: ( x in n implies x is Nat ) reconsider m = n as Element of NAT by ORDINAL1:def_12; assume x in n ; ::_thesis: x is Nat then x in { j where j is Element of NAT : j < m } by AXIOMS:4; then ex j being Element of NAT st ( x = j & j < m ) ; hence x is Nat ; ::_thesis: verum end; theorem Th4: :: NECKLACE:4 for x being non empty Nat holds 0 in x proof let x be non empty Nat; ::_thesis: 0 in x reconsider n = x as Element of NAT by ORDINAL1:def_12; ( n = { i where i is Element of NAT : i < n } & 0 < n ) by AXIOMS:4, NAT_1:3; hence 0 in x ; ::_thesis: verum end; registration let X be set ; cluster delta X -> one-to-one ; coherence delta X is one-to-one proof set f = delta X; let x1, x2 be set ; :: according to FUNCT_1:def_4 ::_thesis: ( not x1 in dom (delta X) or not x2 in dom (delta X) or not (delta X) . x1 = (delta X) . x2 or x1 = x2 ) assume that A1: ( x1 in dom (delta X) & x2 in dom (delta X) ) and A2: (delta X) . x1 = (delta X) . x2 ; ::_thesis: x1 = x2 ( (delta X) . x1 = [x1,x1] & (delta X) . x2 = [x2,x2] ) by A1, FUNCT_3:def_6; hence x1 = x2 by A2, XTUPLE_0:1; ::_thesis: verum end; end; theorem Th5: :: NECKLACE:5 for X being set holds card (id X) = card X proof let X be set ; ::_thesis: card (id X) = card X id X in Funcs (X,X) by FUNCT_2:9; hence card (id X) = card X by CARD_2:3; ::_thesis: verum end; registration cluster Relation-like Function-like trivial -> one-to-one for set ; coherence for b1 being Function st b1 is trivial holds b1 is one-to-one proof let f be Function; ::_thesis: ( f is trivial implies f is one-to-one ) assume A1: f is trivial ; ::_thesis: f is one-to-one let x1, x2 be set ; :: according to FUNCT_1:def_4 ::_thesis: ( not x1 in dom f or not x2 in dom f or not f . x1 = f . x2 or x1 = x2 ) assume that A2: x1 in dom f and A3: x2 in dom f and f . x1 = f . x2 ; ::_thesis: x1 = x2 reconsider f = f as trivial Function by A1; consider x being set such that A4: dom f = {x} by A2, ZFMISC_1:131; x1 = x by A2, A4, TARSKI:def_1; hence x1 = x2 by A3, A4, TARSKI:def_1; ::_thesis: verum end; end; theorem :: NECKLACE:6 for f, g being Function st dom f misses dom g holds rng (f +* g) = (rng f) \/ (rng g) by FRECHET:35, PARTFUN1:56; theorem Th7: :: NECKLACE:7 for f, g being one-to-one Function st dom f misses dom g & rng f misses rng g holds (f +* g) " = (f ") +* (g ") proof let f, g be one-to-one Function; ::_thesis: ( dom f misses dom g & rng f misses rng g implies (f +* g) " = (f ") +* (g ") ) assume that A1: dom f misses dom g and A2: rng f misses rng g ; ::_thesis: (f +* g) " = (f ") +* (g ") A3: f +* g is one-to-one by A2, FUNCT_4:92; A4: for y, x being set holds ( y in rng (f +* g) & x = ((f ") +* (g ")) . y iff ( x in dom (f +* g) & y = (f +* g) . x ) ) proof let y, x be set ; ::_thesis: ( y in rng (f +* g) & x = ((f ") +* (g ")) . y iff ( x in dom (f +* g) & y = (f +* g) . x ) ) thus ( y in rng (f +* g) & x = ((f ") +* (g ")) . y implies ( x in dom (f +* g) & y = (f +* g) . x ) ) ::_thesis: ( x in dom (f +* g) & y = (f +* g) . x implies ( y in rng (f +* g) & x = ((f ") +* (g ")) . y ) ) proof A5: rng (f +* g) c= (rng f) \/ (rng g) by FUNCT_4:17; assume that A6: y in rng (f +* g) and A7: x = ((f ") +* (g ")) . y ; ::_thesis: ( x in dom (f +* g) & y = (f +* g) . x ) percases ( y in rng f or y in rng g ) by A6, A5, XBOOLE_0:def_3; supposeA8: y in rng f ; ::_thesis: ( x in dom (f +* g) & y = (f +* g) . x ) then consider z being set such that A9: z in dom f and A10: y = f . z by FUNCT_1:def_3; dom (f +* g) = (dom f) \/ (dom g) by FUNCT_4:def_1; then A11: z in dom (f +* g) by A9, XBOOLE_0:def_3; A12: ( dom (f ") = rng f & dom (g ") = rng g ) by FUNCT_1:33; ( y = (f +* g) . z & z = (f ") . y ) by A1, A9, A10, FUNCT_1:32, FUNCT_4:16; hence ( x in dom (f +* g) & y = (f +* g) . x ) by A2, A7, A8, A11, A12, FUNCT_4:16; ::_thesis: verum end; supposeA13: y in rng g ; ::_thesis: ( x in dom (f +* g) & y = (f +* g) . x ) A14: ( dom (f ") = rng f & dom (g ") = rng g ) by FUNCT_1:33; consider z being set such that A15: z in dom g and A16: y = g . z by A13, FUNCT_1:def_3; z = (g ") . y by A15, A16, FUNCT_1:32; then z = ((g ") +* (f ")) . y by A2, A13, A14, FUNCT_4:16; then A17: z = x by A2, A7, A14, FUNCT_4:35; ( dom (f +* g) = (dom f) \/ (dom g) & y = (g +* f) . z ) by A1, A15, A16, FUNCT_4:16, FUNCT_4:def_1; hence ( x in dom (f +* g) & y = (f +* g) . x ) by A1, A15, A17, FUNCT_4:35, XBOOLE_0:def_3; ::_thesis: verum end; end; end; thus ( x in dom (f +* g) & y = (f +* g) . x implies ( y in rng (f +* g) & x = ((f ") +* (g ")) . y ) ) ::_thesis: verum proof A18: dom (f +* g) = (dom f) \/ (dom g) by FUNCT_4:def_1; assume that A19: x in dom (f +* g) and A20: y = (f +* g) . x ; ::_thesis: ( y in rng (f +* g) & x = ((f ") +* (g ")) . y ) percases ( x in dom f or x in dom g ) by A19, A18, XBOOLE_0:def_3; supposeA21: x in dom f ; ::_thesis: ( y in rng (f +* g) & x = ((f ") +* (g ")) . y ) then not x in dom g by A1, XBOOLE_0:3; then A22: y = f . x by A20, FUNCT_4:11; then A23: x = (f ") . y by A21, FUNCT_1:32; A24: ( dom (f ") = rng f & dom (g ") = rng g ) by FUNCT_1:33; A25: y in rng f by A21, A22, FUNCT_1:def_3; then y in (rng f) \/ (rng g) by XBOOLE_0:def_3; hence ( y in rng (f +* g) & x = ((f ") +* (g ")) . y ) by A1, A2, A25, A23, A24, FRECHET:35, FUNCT_4:16, PARTFUN1:56; ::_thesis: verum end; supposeA26: x in dom g ; ::_thesis: ( y in rng (f +* g) & x = ((f ") +* (g ")) . y ) then A27: y = g . x by A20, FUNCT_4:13; then A28: y in rng g by A26, FUNCT_1:def_3; then A29: y in (rng f) \/ (rng g) by XBOOLE_0:def_3; A30: ( dom (f ") = rng f & dom (g ") = rng g ) by FUNCT_1:33; x = (g ") . y by A26, A27, FUNCT_1:32; then x = ((g ") +* (f ")) . y by A2, A28, A30, FUNCT_4:16; hence ( y in rng (f +* g) & x = ((f ") +* (g ")) . y ) by A1, A2, A29, A30, FRECHET:35, FUNCT_4:35, PARTFUN1:56; ::_thesis: verum end; end; end; end; dom ((f ") +* (g ")) = (dom (f ")) \/ (dom (g ")) by FUNCT_4:def_1 .= (rng f) \/ (dom (g ")) by FUNCT_1:33 .= (rng f) \/ (rng g) by FUNCT_1:33 .= rng (f +* g) by A1, FRECHET:35, PARTFUN1:56 ; hence (f +* g) " = (f ") +* (g ") by A3, A4, FUNCT_1:32; ::_thesis: verum end; theorem :: NECKLACE:8 for A, a, b being set holds (A --> a) +* (A --> b) = A --> b proof let A, a, b be set ; ::_thesis: (A --> a) +* (A --> b) = A --> b set g = A --> b; dom (A --> b) = A by FUNCOP_1:13; then dom (A --> a) c= dom (A --> b) ; hence (A --> a) +* (A --> b) = A --> b by FUNCT_4:19; ::_thesis: verum end; theorem Th9: :: NECKLACE:9 for a, b being set holds (a .--> b) " = b .--> a proof let a, b be set ; ::_thesis: (a .--> b) " = b .--> a set f = a .--> b; set g = b .--> a; A1: for y, x being set holds ( y in rng (a .--> b) & x = (b .--> a) . y iff ( x in dom (a .--> b) & y = (a .--> b) . x ) ) proof let y, x be set ; ::_thesis: ( y in rng (a .--> b) & x = (b .--> a) . y iff ( x in dom (a .--> b) & y = (a .--> b) . x ) ) thus ( y in rng (a .--> b) & x = (b .--> a) . y implies ( x in dom (a .--> b) & y = (a .--> b) . x ) ) ::_thesis: ( x in dom (a .--> b) & y = (a .--> b) . x implies ( y in rng (a .--> b) & x = (b .--> a) . y ) ) proof assume that A2: y in rng (a .--> b) and A3: x = (b .--> a) . y ; ::_thesis: ( x in dom (a .--> b) & y = (a .--> b) . x ) A4: y in {b} by A2, FUNCOP_1:8; then A5: x = (b .--> a) . b by A3, TARSKI:def_1 .= a by FUNCOP_1:72 ; then A6: x in {a} by TARSKI:def_1; (a .--> b) . x = b by A5, FUNCOP_1:72 .= y by A4, TARSKI:def_1 ; hence ( x in dom (a .--> b) & y = (a .--> b) . x ) by A6, FUNCOP_1:13; ::_thesis: verum end; assume that A7: x in dom (a .--> b) and A8: y = (a .--> b) . x ; ::_thesis: ( y in rng (a .--> b) & x = (b .--> a) . y ) A9: x in {a} by A7; then A10: y = (a .--> b) . a by A8, TARSKI:def_1 .= b by FUNCOP_1:72 ; then A11: y in {b} by TARSKI:def_1; (b .--> a) . y = a by A10, FUNCOP_1:72 .= x by A9, TARSKI:def_1 ; hence ( y in rng (a .--> b) & x = (b .--> a) . y ) by A11, FUNCOP_1:8; ::_thesis: verum end; dom (b .--> a) = {b} by FUNCOP_1:13 .= rng (a .--> b) by FUNCOP_1:8 ; hence (a .--> b) " = b .--> a by A1, FUNCT_1:32; ::_thesis: verum end; theorem Th10: :: NECKLACE:10 for a, b, c, d being set holds not ( ( a = b implies c = d ) & ( c = d implies a = b ) & not ((a,b) --> (c,d)) " = (c,d) --> (a,b) ) proof let a, b, c, d be set ; ::_thesis: not ( ( a = b implies c = d ) & ( c = d implies a = b ) & not ((a,b) --> (c,d)) " = (c,d) --> (a,b) ) assume A1: ( a = b iff c = d ) ; ::_thesis: ((a,b) --> (c,d)) " = (c,d) --> (a,b) percases ( ( a = b & c = d ) or ( a <> b & c <> d ) ) by A1; supposeA2: ( a = b & c = d ) ; ::_thesis: ((a,b) --> (c,d)) " = (c,d) --> (a,b) ((a,a) --> (d,d)) " = (a .--> d) " by FUNCT_4:81 .= d .--> a by Th9 .= (d,d) --> (a,a) by FUNCT_4:81 ; hence ((a,b) --> (c,d)) " = (c,d) --> (a,b) by A2; ::_thesis: verum end; supposeA3: ( a <> b & c <> d ) ; ::_thesis: ((a,b) --> (c,d)) " = (c,d) --> (a,b) set f = (a,b) --> (c,d); set g = (c,d) --> (a,b); A4: for y, x being set holds ( y in rng ((a,b) --> (c,d)) & x = ((c,d) --> (a,b)) . y iff ( x in dom ((a,b) --> (c,d)) & y = ((a,b) --> (c,d)) . x ) ) proof let y, x be set ; ::_thesis: ( y in rng ((a,b) --> (c,d)) & x = ((c,d) --> (a,b)) . y iff ( x in dom ((a,b) --> (c,d)) & y = ((a,b) --> (c,d)) . x ) ) A5: ( x in dom ((a,b) --> (c,d)) & y = ((a,b) --> (c,d)) . x implies ( y in rng ((a,b) --> (c,d)) & x = ((c,d) --> (a,b)) . y ) ) proof assume that A6: x in dom ((a,b) --> (c,d)) and A7: y = ((a,b) --> (c,d)) . x ; ::_thesis: ( y in rng ((a,b) --> (c,d)) & x = ((c,d) --> (a,b)) . y ) A8: x in {a,b} by A6, FUNCT_4:62; percases ( x = a or x = b ) by A8, TARSKI:def_2; supposeA9: x = a ; ::_thesis: ( y in rng ((a,b) --> (c,d)) & x = ((c,d) --> (a,b)) . y ) then A10: y = c by A3, A7, FUNCT_4:63; then y in {c,d} by TARSKI:def_2; hence ( y in rng ((a,b) --> (c,d)) & x = ((c,d) --> (a,b)) . y ) by A3, A9, A10, FUNCT_4:63, FUNCT_4:64; ::_thesis: verum end; supposeA11: x = b ; ::_thesis: ( y in rng ((a,b) --> (c,d)) & x = ((c,d) --> (a,b)) . y ) then A12: y = d by A7, FUNCT_4:63; then y in {c,d} by TARSKI:def_2; hence ( y in rng ((a,b) --> (c,d)) & x = ((c,d) --> (a,b)) . y ) by A3, A11, A12, FUNCT_4:63, FUNCT_4:64; ::_thesis: verum end; end; end; ( y in rng ((a,b) --> (c,d)) & x = ((c,d) --> (a,b)) . y implies ( x in dom ((a,b) --> (c,d)) & y = ((a,b) --> (c,d)) . x ) ) proof assume that A13: y in rng ((a,b) --> (c,d)) and A14: x = ((c,d) --> (a,b)) . y ; ::_thesis: ( x in dom ((a,b) --> (c,d)) & y = ((a,b) --> (c,d)) . x ) A15: y in {c,d} by A3, A13, FUNCT_4:64; percases ( y = c or y = d ) by A15, TARSKI:def_2; supposeA16: y = c ; ::_thesis: ( x in dom ((a,b) --> (c,d)) & y = ((a,b) --> (c,d)) . x ) then A17: x = a by A3, A14, FUNCT_4:63; then x in {a,b} by TARSKI:def_2; hence ( x in dom ((a,b) --> (c,d)) & y = ((a,b) --> (c,d)) . x ) by A3, A16, A17, FUNCT_4:62, FUNCT_4:63; ::_thesis: verum end; supposeA18: y = d ; ::_thesis: ( x in dom ((a,b) --> (c,d)) & y = ((a,b) --> (c,d)) . x ) then A19: x = b by A14, FUNCT_4:63; then x in {a,b} by TARSKI:def_2; hence ( x in dom ((a,b) --> (c,d)) & y = ((a,b) --> (c,d)) . x ) by A18, A19, FUNCT_4:62, FUNCT_4:63; ::_thesis: verum end; end; end; hence ( y in rng ((a,b) --> (c,d)) & x = ((c,d) --> (a,b)) . y iff ( x in dom ((a,b) --> (c,d)) & y = ((a,b) --> (c,d)) . x ) ) by A5; ::_thesis: verum end; A20: (a,b) --> (c,d) is one-to-one proof A21: dom ((a,b) --> (c,d)) = {a,b} by FUNCT_4:62; let x1, x2 be set ; :: according to FUNCT_1:def_4 ::_thesis: ( not x1 in dom ((a,b) --> (c,d)) or not x2 in dom ((a,b) --> (c,d)) or not ((a,b) --> (c,d)) . x1 = ((a,b) --> (c,d)) . x2 or x1 = x2 ) assume that A22: ( x1 in dom ((a,b) --> (c,d)) & x2 in dom ((a,b) --> (c,d)) ) and A23: ((a,b) --> (c,d)) . x1 = ((a,b) --> (c,d)) . x2 ; ::_thesis: x1 = x2 percases ( ( x1 = a & x2 = a ) or ( x1 = b & x2 = b ) or ( x1 = a & x2 = b ) or ( x1 = b & x2 = a ) ) by A22, A21, TARSKI:def_2; suppose ( ( x1 = a & x2 = a ) or ( x1 = b & x2 = b ) ) ; ::_thesis: x1 = x2 hence x1 = x2 ; ::_thesis: verum end; supposeA24: ( x1 = a & x2 = b ) ; ::_thesis: x1 = x2 then ((a,b) --> (c,d)) . x1 = c by A3, FUNCT_4:63; hence x1 = x2 by A3, A23, A24, FUNCT_4:63; ::_thesis: verum end; supposeA25: ( x1 = b & x2 = a ) ; ::_thesis: x1 = x2 then ((a,b) --> (c,d)) . x1 = d by FUNCT_4:63; hence x1 = x2 by A3, A23, A25, FUNCT_4:63; ::_thesis: verum end; end; end; dom ((c,d) --> (a,b)) = {c,d} by FUNCT_4:62 .= rng ((a,b) --> (c,d)) by A3, FUNCT_4:64 ; hence ((a,b) --> (c,d)) " = (c,d) --> (a,b) by A20, A4, FUNCT_1:32; ::_thesis: verum end; end; end; scheme :: NECKLACE:sch 1 Convers{ F1() -> non empty set , F2() -> Relation, F3( set ) -> set , F4( set ) -> set , P1[ set ] } : F2() ~ = { [F3(x),F4(x)] where x is Element of F1() : P1[x] } provided A1: F2() = { [F4(x),F3(x)] where x is Element of F1() : P1[x] } proof set S = { [F3(x),F4(x)] where x is Element of F1() : P1[x] } ; { [F3(x),F4(x)] where x is Element of F1() : P1[x] } is Relation-like proof let x be set ; :: according to RELAT_1:def_1 ::_thesis: ( not x in { [F3(x),F4(x)] where x is Element of F1() : P1[x] } or ex b1, b2 being set st x = [b1,b2] ) assume x in { [F3(x),F4(x)] where x is Element of F1() : P1[x] } ; ::_thesis: ex b1, b2 being set st x = [b1,b2] then ex y being Element of F1() st ( x = [F3(y),F4(y)] & P1[y] ) ; hence ex b1, b2 being set st x = [b1,b2] ; ::_thesis: verum end; then reconsider S9 = { [F3(x),F4(x)] where x is Element of F1() : P1[x] } as Relation ; A2: for x, y being set st [y,x] in F2() holds [x,y] in S9 proof let x, y be set ; ::_thesis: ( [y,x] in F2() implies [x,y] in S9 ) assume [y,x] in F2() ; ::_thesis: [x,y] in S9 then consider z being Element of F1() such that A3: [y,x] = [F4(z),F3(z)] and A4: P1[z] by A1; ( y = F4(z) & x = F3(z) ) by A3, XTUPLE_0:1; hence [x,y] in S9 by A4; ::_thesis: verum end; for x, y being set st [x,y] in S9 holds [y,x] in F2() proof let x, y be set ; ::_thesis: ( [x,y] in S9 implies [y,x] in F2() ) assume [x,y] in S9 ; ::_thesis: [y,x] in F2() then consider z being Element of F1() such that A5: [x,y] = [F3(z),F4(z)] and A6: P1[z] ; ( x = F3(z) & y = F4(z) ) by A5, XTUPLE_0:1; hence [y,x] in F2() by A1, A6; ::_thesis: verum end; hence F2() ~ = { [F3(x),F4(x)] where x is Element of F1() : P1[x] } by A2, RELAT_1:def_7; ::_thesis: verum end; theorem :: NECKLACE:11 for i, j, n being Nat st i < j & j in n holds i in n proof let i, j, n be Nat; ::_thesis: ( i < j & j in n implies i in n ) assume that A1: i < j and A2: j in n ; ::_thesis: i in n j < n by A2, NAT_1:44; then i < n by A1, XXREAL_0:2; hence i in n by NAT_1:44; ::_thesis: verum end; begin definition let R, S be RelStr ; predS embeds R means :Def1: :: NECKLACE:def 1 ex f being Function of R,S st ( f is one-to-one & ( for x, y being Element of R holds ( [x,y] in the InternalRel of R iff [(f . x),(f . y)] in the InternalRel of S ) ) ); end; :: deftheorem Def1 defines embeds NECKLACE:def_1_:_ for R, S being RelStr holds ( S embeds R iff ex f being Function of R,S st ( f is one-to-one & ( for x, y being Element of R holds ( [x,y] in the InternalRel of R iff [(f . x),(f . y)] in the InternalRel of S ) ) ) ); definition let R, S be non empty RelStr ; :: original: embeds redefine predS embeds R; reflexivity for S being non empty RelStr holds (b1,b1) proof let R be non empty RelStr ; ::_thesis: (R,R) set f = id the carrier of R; reconsider f = id the carrier of R as Function of R,R ; take f ; :: according to NECKLACE:def_1 ::_thesis: ( f is one-to-one & ( for x, y being Element of R holds ( [x,y] in the InternalRel of R iff [(f . x),(f . y)] in the InternalRel of R ) ) ) thus f is V7() ; ::_thesis: for x, y being Element of R holds ( [x,y] in the InternalRel of R iff [(f . x),(f . y)] in the InternalRel of R ) let x, y be Element of R; ::_thesis: ( [x,y] in the InternalRel of R iff [(f . x),(f . y)] in the InternalRel of R ) x = f . x by FUNCT_1:18; hence ( [x,y] in the InternalRel of R iff [(f . x),(f . y)] in the InternalRel of R ) by FUNCT_1:18; ::_thesis: verum end; end; theorem Th12: :: NECKLACE:12 for R, S, T being non empty RelStr st R embeds S & S embeds T holds R embeds T proof let R, S, T be non empty RelStr ; ::_thesis: ( R embeds S & S embeds T implies R embeds T ) assume R embeds S ; ::_thesis: ( not S embeds T or R embeds T ) then consider f being Function of S,R such that A1: f is V7() and A2: for x, y being Element of S holds ( [x,y] in the InternalRel of S iff [(f . x),(f . y)] in the InternalRel of R ) by Def1; assume S embeds T ; ::_thesis: R embeds T then consider g being Function of T,S such that A3: g is V7() and A4: for x, y being Element of T holds ( [x,y] in the InternalRel of T iff [(g . x),(g . y)] in the InternalRel of S ) by Def1; reconsider h = f * g as Function of T,R ; take h ; :: according to NECKLACE:def_1 ::_thesis: ( h is one-to-one & ( for x, y being Element of T holds ( [x,y] in the InternalRel of T iff [(h . x),(h . y)] in the InternalRel of R ) ) ) thus h is V7() by A1, A3; ::_thesis: for x, y being Element of T holds ( [x,y] in the InternalRel of T iff [(h . x),(h . y)] in the InternalRel of R ) thus for x, y being Element of T holds ( [x,y] in the InternalRel of T iff [(h . x),(h . y)] in the InternalRel of R ) ::_thesis: verum proof let x, y be Element of T; ::_thesis: ( [x,y] in the InternalRel of T iff [(h . x),(h . y)] in the InternalRel of R ) thus ( [x,y] in the InternalRel of T implies [(h . x),(h . y)] in the InternalRel of R ) ::_thesis: ( [(h . x),(h . y)] in the InternalRel of R implies [x,y] in the InternalRel of T ) proof assume [x,y] in the InternalRel of T ; ::_thesis: [(h . x),(h . y)] in the InternalRel of R then A5: [(g . x),(g . y)] in the InternalRel of S by A4; ( h . x = f . (g . x) & h . y = f . (g . y) ) by FUNCT_2:15; hence [(h . x),(h . y)] in the InternalRel of R by A2, A5; ::_thesis: verum end; thus ( [(h . x),(h . y)] in the InternalRel of R implies [x,y] in the InternalRel of T ) ::_thesis: verum proof A6: ( h . x = f . (g . x) & h . y = f . (g . y) ) by FUNCT_2:15; assume [(h . x),(h . y)] in the InternalRel of R ; ::_thesis: [x,y] in the InternalRel of T then [(g . x),(g . y)] in the InternalRel of S by A2, A6; hence [x,y] in the InternalRel of T by A4; ::_thesis: verum end; end; end; definition let R, S be non empty RelStr ; predR is_equimorphic_to S means :Def2: :: NECKLACE:def 2 ( R embeds S & S embeds R ); reflexivity for R being non empty RelStr holds ( R embeds R & R embeds R ) ; symmetry for R, S being non empty RelStr st R embeds S & S embeds R holds ( S embeds R & R embeds S ) ; end; :: deftheorem Def2 defines is_equimorphic_to NECKLACE:def_2_:_ for R, S being non empty RelStr holds ( R is_equimorphic_to S iff ( R embeds S & S embeds R ) ); theorem :: NECKLACE:13 for R, S, T being non empty RelStr st R is_equimorphic_to S & S is_equimorphic_to T holds R is_equimorphic_to T proof let R, S, T be non empty RelStr ; ::_thesis: ( R is_equimorphic_to S & S is_equimorphic_to T implies R is_equimorphic_to T ) assume A1: ( R is_equimorphic_to S & S is_equimorphic_to T ) ; ::_thesis: R is_equimorphic_to T then ( S embeds R & T embeds S ) by Def2; then A2: T embeds R by Th12; ( R embeds S & S embeds T ) by A1, Def2; then R embeds T by Th12; hence R is_equimorphic_to T by A2, Def2; ::_thesis: verum end; notation let R be non empty RelStr ; synonym parallel R for connected ; end; definition let R be RelStr ; attrR is symmetric means :Def3: :: NECKLACE:def 3 the InternalRel of R is_symmetric_in the carrier of R; end; :: deftheorem Def3 defines symmetric NECKLACE:def_3_:_ for R being RelStr holds ( R is symmetric iff the InternalRel of R is_symmetric_in the carrier of R ); definition let R be RelStr ; attrR is asymmetric means :Def4: :: NECKLACE:def 4 the InternalRel of R is asymmetric ; end; :: deftheorem Def4 defines asymmetric NECKLACE:def_4_:_ for R being RelStr holds ( R is asymmetric iff the InternalRel of R is asymmetric ); theorem :: NECKLACE:14 for R being RelStr st R is asymmetric holds the InternalRel of R misses the InternalRel of R ~ proof let R be RelStr ; ::_thesis: ( R is asymmetric implies the InternalRel of R misses the InternalRel of R ~ ) assume R is asymmetric ; ::_thesis: the InternalRel of R misses the InternalRel of R ~ then the InternalRel of R is asymmetric by Def4; then A1: the InternalRel of R is_asymmetric_in field the InternalRel of R by RELAT_2:def_13; assume the InternalRel of R meets the InternalRel of R ~ ; ::_thesis: contradiction then consider x being set such that A2: x in the InternalRel of R and A3: x in the InternalRel of R ~ by XBOOLE_0:3; consider y, z being set such that A4: x = [y,z] by A3, RELAT_1:def_1; A5: z in field the InternalRel of R by A2, A4, RELAT_1:15; ( [z,y] in the InternalRel of R & y in field the InternalRel of R ) by A2, A3, A4, RELAT_1:15, RELAT_1:def_7; hence contradiction by A2, A4, A1, A5, RELAT_2:def_5; ::_thesis: verum end; definition let R be RelStr ; attrR is irreflexive means :: NECKLACE:def 5 for x being set st x in the carrier of R holds not [x,x] in the InternalRel of R; end; :: deftheorem defines irreflexive NECKLACE:def_5_:_ for R being RelStr holds ( R is irreflexive iff for x being set st x in the carrier of R holds not [x,x] in the InternalRel of R ); definition let n be Nat; funcn -SuccRelStr -> strict RelStr means :Def6: :: NECKLACE:def 6 ( the carrier of it = n & the InternalRel of it = { [i,(i + 1)] where i is Element of NAT : i + 1 < n } ); existence ex b1 being strict RelStr st ( the carrier of b1 = n & the InternalRel of b1 = { [i,(i + 1)] where i is Element of NAT : i + 1 < n } ) proof set r = { [i,(i + 1)] where i is Element of NAT : i + 1 < n } ; { [i,(i + 1)] where i is Element of NAT : i + 1 < n } c= [:n,n:] proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { [i,(i + 1)] where i is Element of NAT : i + 1 < n } or x in [:n,n:] ) assume x in { [i,(i + 1)] where i is Element of NAT : i + 1 < n } ; ::_thesis: x in [:n,n:] then consider i being Element of NAT such that A1: x = [i,(i + 1)] and A2: i + 1 < n ; i <= i + 1 by NAT_1:11; then i < n by A2, XXREAL_0:2; then A3: i in n by NAT_1:44; i + 1 in n by A2, NAT_1:44; hence x in [:n,n:] by A1, A3, ZFMISC_1:87; ::_thesis: verum end; then reconsider r = { [i,(i + 1)] where i is Element of NAT : i + 1 < n } as Relation of n ; take RelStr(# n,r #) ; ::_thesis: ( the carrier of RelStr(# n,r #) = n & the InternalRel of RelStr(# n,r #) = { [i,(i + 1)] where i is Element of NAT : i + 1 < n } ) thus ( the carrier of RelStr(# n,r #) = n & the InternalRel of RelStr(# n,r #) = { [i,(i + 1)] where i is Element of NAT : i + 1 < n } ) ; ::_thesis: verum end; uniqueness for b1, b2 being strict RelStr st the carrier of b1 = n & the InternalRel of b1 = { [i,(i + 1)] where i is Element of NAT : i + 1 < n } & the carrier of b2 = n & the InternalRel of b2 = { [i,(i + 1)] where i is Element of NAT : i + 1 < n } holds b1 = b2 ; end; :: deftheorem Def6 defines -SuccRelStr NECKLACE:def_6_:_ for n being Nat for b2 being strict RelStr holds ( b2 = n -SuccRelStr iff ( the carrier of b2 = n & the InternalRel of b2 = { [i,(i + 1)] where i is Element of NAT : i + 1 < n } ) ); theorem :: NECKLACE:15 for n being Nat holds n -SuccRelStr is asymmetric proof let n be Nat; ::_thesis: n -SuccRelStr is asymmetric set S = n -SuccRelStr ; the InternalRel of (n -SuccRelStr) is_asymmetric_in field the InternalRel of (n -SuccRelStr) proof let x, y be set ; :: according to RELAT_2:def_5 ::_thesis: ( not x in field the InternalRel of (n -SuccRelStr) or not y in field the InternalRel of (n -SuccRelStr) or not [x,y] in the InternalRel of (n -SuccRelStr) or not [y,x] in the InternalRel of (n -SuccRelStr) ) assume that x in field the InternalRel of (n -SuccRelStr) and y in field the InternalRel of (n -SuccRelStr) and A1: [x,y] in the InternalRel of (n -SuccRelStr) ; ::_thesis: not [y,x] in the InternalRel of (n -SuccRelStr) A2: [x,y] in { [i,(i + 1)] where i is Element of NAT : i + 1 < n } by A1, Def6; assume [y,x] in the InternalRel of (n -SuccRelStr) ; ::_thesis: contradiction then [y,x] in { [i9,(i9 + 1)] where i9 is Element of NAT : i9 + 1 < n } by Def6; then consider j being Element of NAT such that A3: [y,x] = [j,(j + 1)] and j + 1 < n ; A4: ( y = j & x = j + 1 ) by A3, XTUPLE_0:1; consider i being Element of NAT such that A5: [x,y] = [i,(i + 1)] and i + 1 < n by A2; ( x = i & y = i + 1 ) by A5, XTUPLE_0:1; hence contradiction by A4; ::_thesis: verum end; hence the InternalRel of (n -SuccRelStr) is asymmetric by RELAT_2:def_13; :: according to NECKLACE:def_4 ::_thesis: verum end; theorem Th16: :: NECKLACE:16 for n being Nat st n > 0 holds card the InternalRel of (n -SuccRelStr) = n - 1 proof let n be Nat; ::_thesis: ( n > 0 implies card the InternalRel of (n -SuccRelStr) = n - 1 ) deffunc H1( Element of NAT ) -> set = [$1,($1 + 1)]; defpred S1[ Element of NAT ] means $1 + 1 < n; defpred S2[ set ] means $1 in n -' 1; A1: n -' 1 c= NAT ; assume A2: n > 0 ; ::_thesis: card the InternalRel of (n -SuccRelStr) = n - 1 then A3: n >= 0 + 1 by NAT_1:13; A4: for i being Nat st i in n -' 1 holds i + 1 < n proof let i be Nat; ::_thesis: ( i in n -' 1 implies i + 1 < n ) assume i in n -' 1 ; ::_thesis: i + 1 < n then A5: i < n -' 1 by NAT_1:44; n >= 0 + 1 by A2, NAT_1:13; then i < n - 1 by A5, XREAL_1:233; hence i + 1 < n by XREAL_1:20; ::_thesis: verum end; A6: for i being Element of NAT holds ( S1[i] iff S2[i] ) proof let i be Element of NAT ; ::_thesis: ( S1[i] iff S2[i] ) thus ( i + 1 < n implies i in n -' 1 ) ::_thesis: ( S2[i] implies S1[i] ) proof assume i + 1 < n ; ::_thesis: i in n -' 1 then i < n - 1 by XREAL_1:20; then i < n -' 1 by A3, XREAL_1:233; hence i in n -' 1 by NAT_1:44; ::_thesis: verum end; thus ( S2[i] implies S1[i] ) by A4; ::_thesis: verum end; A7: { H1(i) where i is Element of NAT : S1[i] } = { H1(i) where i is Element of NAT : S2[i] } from FRAENKEL:sch_3(A6); deffunc H2( Element of NAT ) -> set = [$1,($1 + 1)]; A8: for d1, d2 being Element of NAT st H2(d1) = H2(d2) holds d1 = d2 by XTUPLE_0:1; A9: n -' 1, { H2(i) where i is Element of NAT : i in n -' 1 } are_equipotent from FUNCT_7:sch_4(A1, A8); thus card the InternalRel of (n -SuccRelStr) = card { [i,(i + 1)] where i is Element of NAT : i + 1 < n } by Def6 .= card (n -' 1) by A7, A9, CARD_1:5 .= n -' 1 by CARD_1:def_2 .= n - 1 by A3, XREAL_1:233 ; ::_thesis: verum end; definition let R be RelStr ; func SymRelStr R -> strict RelStr means :Def7: :: NECKLACE:def 7 ( the carrier of it = the carrier of R & the InternalRel of it = the InternalRel of R \/ ( the InternalRel of R ~) ); existence ex b1 being strict RelStr st ( the carrier of b1 = the carrier of R & the InternalRel of b1 = the InternalRel of R \/ ( the InternalRel of R ~) ) proof take RelStr(# the carrier of R,( the InternalRel of R \/ ( the InternalRel of R ~)) #) ; ::_thesis: ( the carrier of RelStr(# the carrier of R,( the InternalRel of R \/ ( the InternalRel of R ~)) #) = the carrier of R & the InternalRel of RelStr(# the carrier of R,( the InternalRel of R \/ ( the InternalRel of R ~)) #) = the InternalRel of R \/ ( the InternalRel of R ~) ) thus ( the carrier of RelStr(# the carrier of R,( the InternalRel of R \/ ( the InternalRel of R ~)) #) = the carrier of R & the InternalRel of RelStr(# the carrier of R,( the InternalRel of R \/ ( the InternalRel of R ~)) #) = the InternalRel of R \/ ( the InternalRel of R ~) ) ; ::_thesis: verum end; uniqueness for b1, b2 being strict RelStr st the carrier of b1 = the carrier of R & the InternalRel of b1 = the InternalRel of R \/ ( the InternalRel of R ~) & the carrier of b2 = the carrier of R & the InternalRel of b2 = the InternalRel of R \/ ( the InternalRel of R ~) holds b1 = b2 ; end; :: deftheorem Def7 defines SymRelStr NECKLACE:def_7_:_ for R being RelStr for b2 being strict RelStr holds ( b2 = SymRelStr R iff ( the carrier of b2 = the carrier of R & the InternalRel of b2 = the InternalRel of R \/ ( the InternalRel of R ~) ) ); registration let R be RelStr ; cluster SymRelStr R -> strict symmetric ; coherence SymRelStr R is symmetric proof let x, y be set ; :: according to RELAT_2:def_3,NECKLACE:def_3 ::_thesis: ( not x in the carrier of (SymRelStr R) or not y in the carrier of (SymRelStr R) or not [x,y] in the InternalRel of (SymRelStr R) or [y,x] in the InternalRel of (SymRelStr R) ) assume that x in the carrier of (SymRelStr R) and y in the carrier of (SymRelStr R) and A1: [x,y] in the InternalRel of (SymRelStr R) ; ::_thesis: [y,x] in the InternalRel of (SymRelStr R) A2: [x,y] in the InternalRel of R \/ ( the InternalRel of R ~) by A1, Def7; percases ( [x,y] in the InternalRel of R or [x,y] in the InternalRel of R ~ ) by A2, XBOOLE_0:def_3; suppose [x,y] in the InternalRel of R ; ::_thesis: [y,x] in the InternalRel of (SymRelStr R) then [y,x] in the InternalRel of R ~ by RELAT_1:def_7; then [y,x] in the InternalRel of R \/ ( the InternalRel of R ~) by XBOOLE_0:def_3; hence [y,x] in the InternalRel of (SymRelStr R) by Def7; ::_thesis: verum end; suppose [x,y] in the InternalRel of R ~ ; ::_thesis: [y,x] in the InternalRel of (SymRelStr R) then [y,x] in the InternalRel of R by RELAT_1:def_7; then [y,x] in the InternalRel of R \/ ( the InternalRel of R ~) by XBOOLE_0:def_3; hence [y,x] in the InternalRel of (SymRelStr R) by Def7; ::_thesis: verum end; end; end; end; registration cluster non empty symmetric for RelStr ; existence ex b1 being RelStr st ( not b1 is empty & b1 is symmetric ) proof set R = {[0,0]}; {[0,0]} c= [:{0},{0}:] by ZFMISC_1:29; then reconsider R = {[0,0]} as Relation of {0} ; take S = RelStr(# {0},R #); ::_thesis: ( not S is empty & S is symmetric ) thus not S is empty ; ::_thesis: S is symmetric thus the InternalRel of S is_symmetric_in the carrier of S :: according to NECKLACE:def_3 ::_thesis: verum proof let x, y be set ; :: according to RELAT_2:def_3 ::_thesis: ( not x in the carrier of S or not y in the carrier of S or not [x,y] in the InternalRel of S or [y,x] in the InternalRel of S ) assume that x in the carrier of S and y in the carrier of S and A1: [x,y] in the InternalRel of S ; ::_thesis: [y,x] in the InternalRel of S ( x = 0 & y = 0 ) by A1, ZFMISC_1:28; then [y,x] in [:{0},{0}:] by ZFMISC_1:28; hence [y,x] in the InternalRel of S by ZFMISC_1:29; ::_thesis: verum end; end; end; registration let R be symmetric RelStr ; cluster the InternalRel of R -> symmetric ; coherence the InternalRel of R is symmetric proof let x, y be set ; :: according to RELAT_2:def_3,RELAT_2:def_11 ::_thesis: ( not x in field the InternalRel of R or not y in field the InternalRel of R or not [x,y] in the InternalRel of R or [y,x] in the InternalRel of R ) assume A1: ( x in field the InternalRel of R & y in field the InternalRel of R & [x,y] in the InternalRel of R ) ; ::_thesis: [y,x] in the InternalRel of R ( the InternalRel of R is_symmetric_in the carrier of R & field the InternalRel of R c= the carrier of R \/ the carrier of R ) by Def3, RELSET_1:8; hence [y,x] in the InternalRel of R by A1, RELAT_2:def_3; ::_thesis: verum end; end; Lm1: for S, R being non empty RelStr st S,R are_isomorphic holds card the InternalRel of S = card the InternalRel of R proof let S, R be non empty RelStr ; ::_thesis: ( S,R are_isomorphic implies card the InternalRel of S = card the InternalRel of R ) set A = the carrier of S; set B = the carrier of R; set C = the InternalRel of S; set D = the InternalRel of R; reconsider C = the InternalRel of S as set ; assume S,R are_isomorphic ; ::_thesis: card the InternalRel of S = card the InternalRel of R then consider f being Function of S,R such that A1: f is isomorphic by WAYBEL_1:def_8; reconsider f9 = f as one-to-one Function by A1, WAYBEL_0:def_38; A2: [:f9,f9:] is one-to-one ; A3: dom f = the carrier of S by FUNCT_2:def_1; A4: rng f = the carrier of R by A1, WAYBEL_0:66; A5: f is monotone by A1, WAYBEL_0:def_38; the InternalRel of S, the InternalRel of R are_equipotent proof set P = [:f,f:]; set F = [:f,f:] | C; set L = dom ([:f,f:] | C); A6: dom ([:f,f:] | C) = (dom [:f,f:]) /\ C by RELAT_1:61 .= [:(dom f),(dom f):] /\ C by FUNCT_3:def_8 .= C by A3, XBOOLE_1:28 ; A7: rng ([:f,f:] | C) c= the InternalRel of R proof let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in rng ([:f,f:] | C) or a in the InternalRel of R ) assume a in rng ([:f,f:] | C) ; ::_thesis: a in the InternalRel of R then consider x being set such that A8: x in dom ([:f,f:] | C) and A9: a = ([:f,f:] | C) . x by FUNCT_1:def_3; consider x1, x2 being set such that A10: x = [x1,x2] by A8, RELAT_1:def_1; A11: x in dom [:f,f:] by A8, RELAT_1:57; then reconsider X1 = x1, X2 = x2 as Element of S by A10, ZFMISC_1:87; X1 <= X2 by A8, A10, ORDERS_2:def_5; then A12: f . X1 <= f . X2 by A5, ORDERS_3:def_5; A13: a = [:f,f:] . (x1,x2) by A8, A9, A10, FUNCT_1:47; ( x1 in dom f & x2 in dom f ) by A3, A10, A11, ZFMISC_1:87; then a = [(f . x1),(f . x2)] by A13, FUNCT_3:def_8; hence a in the InternalRel of R by A12, ORDERS_2:def_5; ::_thesis: verum end; then reconsider F = [:f,f:] | C as Function of (dom ([:f,f:] | C)),[: the carrier of R, the carrier of R:] by FUNCT_2:2, XBOOLE_1:1; reconsider F = F as Function of (dom ([:f,f:] | C)), the InternalRel of R by A7, FUNCT_2:6; A14: rng F = the InternalRel of R proof thus rng F c= the InternalRel of R by A7; :: according to XBOOLE_0:def_10 ::_thesis: the InternalRel of R c= rng F let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the InternalRel of R or x in rng F ) assume A15: x in the InternalRel of R ; ::_thesis: x in rng F then consider x1, x2 being set such that A16: x = [x1,x2] by RELAT_1:def_1; reconsider x19 = x1, x29 = x2 as Element of the carrier of R by A15, A16, ZFMISC_1:87; x1 in the carrier of R by A15, A16, ZFMISC_1:87; then consider X1 being set such that A17: X1 in dom f and A18: x1 = f . X1 by A4, FUNCT_1:def_3; x2 in the carrier of R by A15, A16, ZFMISC_1:87; then consider X2 being set such that A19: X2 in dom f and A20: x2 = f . X2 by A4, FUNCT_1:def_3; reconsider X19 = X1, X29 = X2 as Element of S by A17, A19; x19 <= x29 by A15, A16, ORDERS_2:def_5; then X19 <= X29 by A1, A18, A20, WAYBEL_0:66; then A21: [X1,X2] in C by ORDERS_2:def_5; set Pi = [X1,X2]; [X1,X2] in [:(dom f),(dom f):] by A17, A19, ZFMISC_1:87; then x = [:f,f:] . (X1,X2) by A16, A18, A20, FUNCT_3:65 .= F . [X1,X2] by A6, A21, FUNCT_1:47 ; hence x in rng F by A6, A21, FUNCT_1:def_3; ::_thesis: verum end; F is one-to-one by A2, FUNCT_1:52; hence the InternalRel of S, the InternalRel of R are_equipotent by A6, A14, WELLORD2:def_4; ::_thesis: verum end; hence card the InternalRel of S = card the InternalRel of R by CARD_1:5; ::_thesis: verum end; definition let R be RelStr ; func ComplRelStr R -> strict RelStr means :Def8: :: NECKLACE:def 8 ( the carrier of it = the carrier of R & the InternalRel of it = ( the InternalRel of R `) \ (id the carrier of R) ); existence ex b1 being strict RelStr st ( the carrier of b1 = the carrier of R & the InternalRel of b1 = ( the InternalRel of R `) \ (id the carrier of R) ) proof reconsider r = ( the InternalRel of R `) \ (id the carrier of R) as Relation of the carrier of R ; take RelStr(# the carrier of R,r #) ; ::_thesis: ( the carrier of RelStr(# the carrier of R,r #) = the carrier of R & the InternalRel of RelStr(# the carrier of R,r #) = ( the InternalRel of R `) \ (id the carrier of R) ) thus ( the carrier of RelStr(# the carrier of R,r #) = the carrier of R & the InternalRel of RelStr(# the carrier of R,r #) = ( the InternalRel of R `) \ (id the carrier of R) ) ; ::_thesis: verum end; uniqueness for b1, b2 being strict RelStr st the carrier of b1 = the carrier of R & the InternalRel of b1 = ( the InternalRel of R `) \ (id the carrier of R) & the carrier of b2 = the carrier of R & the InternalRel of b2 = ( the InternalRel of R `) \ (id the carrier of R) holds b1 = b2 ; end; :: deftheorem Def8 defines ComplRelStr NECKLACE:def_8_:_ for R being RelStr for b2 being strict RelStr holds ( b2 = ComplRelStr R iff ( the carrier of b2 = the carrier of R & the InternalRel of b2 = ( the InternalRel of R `) \ (id the carrier of R) ) ); registration let R be non empty RelStr ; cluster ComplRelStr R -> non empty strict ; coherence not ComplRelStr R is empty proof the carrier of (ComplRelStr R) = the carrier of R by Def8; hence not the carrier of (ComplRelStr R) is empty ; :: according to STRUCT_0:def_1 ::_thesis: verum end; end; theorem Th17: :: NECKLACE:17 for S, R being RelStr st S,R are_isomorphic holds card the InternalRel of S = card the InternalRel of R proof let S, R be RelStr ; ::_thesis: ( S,R are_isomorphic implies card the InternalRel of S = card the InternalRel of R ) assume A1: S,R are_isomorphic ; ::_thesis: card the InternalRel of S = card the InternalRel of R then A2: ex f being Function of S,R st f is isomorphic by WAYBEL_1:def_8; percases ( ( not S is empty & not R is empty ) or ( S is empty & R is empty ) ) by A2, WAYBEL_0:def_38; suppose ( not S is empty & not R is empty ) ; ::_thesis: card the InternalRel of S = card the InternalRel of R hence card the InternalRel of S = card the InternalRel of R by A1, Lm1; ::_thesis: verum end; suppose ( S is empty & R is empty ) ; ::_thesis: card the InternalRel of S = card the InternalRel of R then reconsider S = S, R = R as empty RelStr ; ( the InternalRel of S = {} & the InternalRel of R = {} ) ; hence card the InternalRel of S = card the InternalRel of R ; ::_thesis: verum end; end; end; begin definition let n be Nat; func Necklace n -> strict RelStr equals :: NECKLACE:def 9 SymRelStr (n -SuccRelStr); coherence SymRelStr (n -SuccRelStr) is strict RelStr ; end; :: deftheorem defines Necklace NECKLACE:def_9_:_ for n being Nat holds Necklace n = SymRelStr (n -SuccRelStr); registration let n be Nat; cluster Necklace n -> strict symmetric ; coherence Necklace n is symmetric ; end; theorem Th18: :: NECKLACE:18 for n being Nat holds the InternalRel of (Necklace n) = { [i,(i + 1)] where i is Element of NAT : i + 1 < n } \/ { [(i + 1),i] where i is Element of NAT : i + 1 < n } proof let n be Nat; ::_thesis: the InternalRel of (Necklace n) = { [i,(i + 1)] where i is Element of NAT : i + 1 < n } \/ { [(i + 1),i] where i is Element of NAT : i + 1 < n } set I = { [i,(i + 1)] where i is Element of NAT : i + 1 < n } ; { [i,(i + 1)] where i is Element of NAT : i + 1 < n } is Relation-like proof let x be set ; :: according to RELAT_1:def_1 ::_thesis: ( not x in { [i,(i + 1)] where i is Element of NAT : i + 1 < n } or ex b1, b2 being set st x = [b1,b2] ) assume x in { [i,(i + 1)] where i is Element of NAT : i + 1 < n } ; ::_thesis: ex b1, b2 being set st x = [b1,b2] then ex i being Element of NAT st ( x = [i,(i + 1)] & i + 1 < n ) ; hence ex b1, b2 being set st x = [b1,b2] ; ::_thesis: verum end; then reconsider I = { [i,(i + 1)] where i is Element of NAT : i + 1 < n } as Relation ; set B = n -SuccRelStr ; deffunc H1( Element of NAT ) -> Element of NAT = $1; deffunc H2( Element of NAT ) -> Element of NAT = $1 + 1; defpred S1[ Element of NAT ] means $1 + 1 < n; set R = { [H2(i),H1(i)] where i is Element of NAT : S1[i] } ; A1: I = { [H1(i),H2(i)] where i is Element of NAT : S1[i] } ; A2: I ~ = { [H2(i),H1(i)] where i is Element of NAT : S1[i] } from NECKLACE:sch_1(A1); the InternalRel of (n -SuccRelStr) = I by Def6; hence the InternalRel of (Necklace n) = { [i,(i + 1)] where i is Element of NAT : i + 1 < n } \/ { [(i + 1),i] where i is Element of NAT : i + 1 < n } by A2, Def7; ::_thesis: verum end; theorem Th19: :: NECKLACE:19 for n being Nat for x being set holds ( x in the InternalRel of (Necklace n) iff ex i being Element of NAT st ( i + 1 < n & ( x = [i,(i + 1)] or x = [(i + 1),i] ) ) ) proof let n be Nat; ::_thesis: for x being set holds ( x in the InternalRel of (Necklace n) iff ex i being Element of NAT st ( i + 1 < n & ( x = [i,(i + 1)] or x = [(i + 1),i] ) ) ) let x be set ; ::_thesis: ( x in the InternalRel of (Necklace n) iff ex i being Element of NAT st ( i + 1 < n & ( x = [i,(i + 1)] or x = [(i + 1),i] ) ) ) thus ( x in the InternalRel of (Necklace n) implies ex i being Element of NAT st ( i + 1 < n & ( x = [i,(i + 1)] or x = [(i + 1),i] ) ) ) ::_thesis: ( ex i being Element of NAT st ( i + 1 < n & ( x = [i,(i + 1)] or x = [(i + 1),i] ) ) implies x in the InternalRel of (Necklace n) ) proof assume x in the InternalRel of (Necklace n) ; ::_thesis: ex i being Element of NAT st ( i + 1 < n & ( x = [i,(i + 1)] or x = [(i + 1),i] ) ) then x in { [i,(i + 1)] where i is Element of NAT : i + 1 < n } \/ { [(i + 1),i] where i is Element of NAT : i + 1 < n } by Th18; then ( x in { [i,(i + 1)] where i is Element of NAT : i + 1 < n } or x in { [(i + 1),i] where i is Element of NAT : i + 1 < n } ) by XBOOLE_0:def_3; then ( ex i being Element of NAT st ( x = [i,(i + 1)] & i + 1 < n ) or ex i being Element of NAT st ( x = [(i + 1),i] & i + 1 < n ) ) ; hence ex i being Element of NAT st ( i + 1 < n & ( x = [i,(i + 1)] or x = [(i + 1),i] ) ) ; ::_thesis: verum end; thus ( ex i being Element of NAT st ( i + 1 < n & ( x = [i,(i + 1)] or x = [(i + 1),i] ) ) implies x in the InternalRel of (Necklace n) ) ::_thesis: verum proof given i being Element of NAT such that A1: ( i + 1 < n & ( x = [i,(i + 1)] or x = [(i + 1),i] ) ) ; ::_thesis: x in the InternalRel of (Necklace n) percases ( ( i + 1 < n & x = [i,(i + 1)] ) or ( i + 1 < n & x = [(i + 1),i] ) ) by A1; suppose ( i + 1 < n & x = [i,(i + 1)] ) ; ::_thesis: x in the InternalRel of (Necklace n) then x in { [j,(j + 1)] where j is Element of NAT : j + 1 < n } ; then x in { [j,(j + 1)] where j is Element of NAT : j + 1 < n } \/ { [(j + 1),j] where j is Element of NAT : j + 1 < n } by XBOOLE_0:def_3; hence x in the InternalRel of (Necklace n) by Th18; ::_thesis: verum end; suppose ( i + 1 < n & x = [(i + 1),i] ) ; ::_thesis: x in the InternalRel of (Necklace n) then x in { [(j + 1),j] where j is Element of NAT : j + 1 < n } ; then x in { [(j + 1),j] where j is Element of NAT : j + 1 < n } \/ { [j,(j + 1)] where j is Element of NAT : j + 1 < n } by XBOOLE_0:def_3; hence x in the InternalRel of (Necklace n) by Th18; ::_thesis: verum end; end; end; end; registration let n be Nat; cluster Necklace n -> strict irreflexive ; coherence Necklace n is irreflexive proof let x be set ; :: according to NECKLACE:def_5 ::_thesis: ( x in the carrier of (Necklace n) implies not [x,x] in the InternalRel of (Necklace n) ) set A = Necklace n; assume x in the carrier of (Necklace n) ; ::_thesis: not [x,x] in the InternalRel of (Necklace n) A1: the InternalRel of (Necklace n) = { [i,(i + 1)] where i is Element of NAT : i + 1 < n } \/ { [(i + 1),i] where i is Element of NAT : i + 1 < n } by Th18; assume A2: [x,x] in the InternalRel of (Necklace n) ; ::_thesis: contradiction percases ( [x,x] in { [i,(i + 1)] where i is Element of NAT : i + 1 < n } or [x,x] in { [(i + 1),i] where i is Element of NAT : i + 1 < n } ) by A2, A1, XBOOLE_0:def_3; suppose [x,x] in { [i,(i + 1)] where i is Element of NAT : i + 1 < n } ; ::_thesis: contradiction then consider i being Element of NAT such that A3: [x,x] = [i,(i + 1)] and i + 1 < n ; ( x = i & x = i + 1 ) by A3, XTUPLE_0:1; hence contradiction ; ::_thesis: verum end; suppose [x,x] in { [(i + 1),i] where i is Element of NAT : i + 1 < n } ; ::_thesis: contradiction then consider i being Element of NAT such that A4: [x,x] = [(i + 1),i] and i + 1 < n ; ( x = i + 1 & x = i ) by A4, XTUPLE_0:1; hence contradiction ; ::_thesis: verum end; end; end; end; theorem Th20: :: NECKLACE:20 for n being Nat holds the carrier of (Necklace n) = n proof let n be Nat; ::_thesis: the carrier of (Necklace n) = n the carrier of (Necklace n) = the carrier of (n -SuccRelStr) by Def7 .= n by Def6 ; hence the carrier of (Necklace n) = n ; ::_thesis: verum end; registration let n be non empty Nat; cluster Necklace n -> non empty strict ; coherence not Necklace n is empty by Th20; end; registration let n be Nat; cluster the carrier of (Necklace n) -> finite ; coherence the carrier of (Necklace n) is finite by Th20; end; theorem Th21: :: NECKLACE:21 for n, i being Nat st i + 1 < n holds [i,(i + 1)] in the InternalRel of (Necklace n) proof let n, j be Nat; ::_thesis: ( j + 1 < n implies [j,(j + 1)] in the InternalRel of (Necklace n) ) assume A1: j + 1 < n ; ::_thesis: [j,(j + 1)] in the InternalRel of (Necklace n) reconsider j = j as Element of NAT by ORDINAL1:def_12; A2: [j,(j + 1)] in { [i,(i + 1)] where i is Element of NAT : i + 1 < n } by A1; the InternalRel of (Necklace n) = { [i,(i + 1)] where i is Element of NAT : i + 1 < n } \/ { [(i + 1),i] where i is Element of NAT : i + 1 < n } by Th18; hence [j,(j + 1)] in the InternalRel of (Necklace n) by A2, XBOOLE_0:def_3; ::_thesis: verum end; theorem Th22: :: NECKLACE:22 for n, i being Nat st i in the carrier of (Necklace n) holds i < n proof let n, i be Nat; ::_thesis: ( i in the carrier of (Necklace n) implies i < n ) assume i in the carrier of (Necklace n) ; ::_thesis: i < n then i in n by Th20; hence i < n by NAT_1:44; ::_thesis: verum end; theorem :: NECKLACE:23 for n being non empty Nat holds Necklace n is connected proof let n be non empty Nat; ::_thesis: Necklace n is connected given X, Y being Subset of (Necklace n) such that A1: X <> {} and A2: Y <> {} and A3: [#] (Necklace n) = X \/ Y and A4: X misses Y and A5: the InternalRel of (Necklace n) = ( the InternalRel of (Necklace n) |_2 X) \/ ( the InternalRel of (Necklace n) |_2 Y) ; :: according to ORDERS_3:def_2,ORDERS_3:def_3 ::_thesis: contradiction A6: ( the carrier of (Necklace n) = n & 0 in n ) by Th4, Th20; percases ( 0 in X or 0 in Y ) by A3, A6, XBOOLE_0:def_3; supposeA7: 0 in X ; ::_thesis: contradiction defpred S1[ Nat] means $1 in Y; consider x being Element of (Necklace n) such that A8: x in Y by A2, SUBSET_1:4; x in the carrier of (Necklace n) ; then x in n by Th20; then x is natural by Th3; then A9: ex x being Nat st S1[x] by A8; consider k being Nat such that A10: S1[k] and A11: for i being Nat st S1[i] holds k <= i from NAT_1:sch_5(A9); k <> 0 by A4, A7, A10, XBOOLE_0:3; then consider i being Nat such that A12: k = i + 1 by NAT_1:6; reconsider i = i as Element of NAT by ORDINAL1:def_12; A13: not i in Y by A11, A12, XREAL_1:29; A14: not i + 1 in X by A4, A10, A12, XBOOLE_0:3; A15: [i,(i + 1)] in the InternalRel of (Necklace n) by A10, A12, Th21, Th22; now__::_thesis:_contradiction percases ( [i,(i + 1)] in the InternalRel of (Necklace n) |_2 X or [i,(i + 1)] in the InternalRel of (Necklace n) |_2 Y ) by A5, A15, XBOOLE_0:def_3; suppose [i,(i + 1)] in the InternalRel of (Necklace n) |_2 X ; ::_thesis: contradiction then [i,(i + 1)] in [:X,X:] by XBOOLE_0:def_4; hence contradiction by A14, ZFMISC_1:87; ::_thesis: verum end; suppose [i,(i + 1)] in the InternalRel of (Necklace n) |_2 Y ; ::_thesis: contradiction then [i,(i + 1)] in [:Y,Y:] by XBOOLE_0:def_4; hence contradiction by A13, ZFMISC_1:87; ::_thesis: verum end; end; end; hence contradiction ; ::_thesis: verum end; supposeA16: 0 in Y ; ::_thesis: contradiction defpred S1[ Nat] means $1 in X; consider y being Element of (Necklace n) such that A17: y in X by A1, SUBSET_1:4; y in the carrier of (Necklace n) ; then y in n by Th20; then y is natural by Th3; then A18: ex y being Nat st S1[y] by A17; consider k being Nat such that A19: S1[k] and A20: for i being Nat st S1[i] holds k <= i from NAT_1:sch_5(A18); k <> 0 by A4, A16, A19, XBOOLE_0:3; then consider i being Nat such that A21: k = i + 1 by NAT_1:6; reconsider i = i as Element of NAT by ORDINAL1:def_12; A22: not i in X by A20, A21, XREAL_1:29; A23: not i + 1 in Y by A4, A19, A21, XBOOLE_0:3; A24: [i,(i + 1)] in the InternalRel of (Necklace n) by A19, A21, Th21, Th22; now__::_thesis:_contradiction percases ( [i,(i + 1)] in the InternalRel of (Necklace n) |_2 Y or [i,(i + 1)] in the InternalRel of (Necklace n) |_2 X ) by A5, A24, XBOOLE_0:def_3; suppose [i,(i + 1)] in the InternalRel of (Necklace n) |_2 Y ; ::_thesis: contradiction then [i,(i + 1)] in [:Y,Y:] by XBOOLE_0:def_4; hence contradiction by A23, ZFMISC_1:87; ::_thesis: verum end; suppose [i,(i + 1)] in the InternalRel of (Necklace n) |_2 X ; ::_thesis: contradiction then [i,(i + 1)] in [:X,X:] by XBOOLE_0:def_4; hence contradiction by A22, ZFMISC_1:87; ::_thesis: verum end; end; end; hence contradiction ; ::_thesis: verum end; end; end; theorem Th24: :: NECKLACE:24 for n, i, j being Nat holds ( not [i,j] in the InternalRel of (Necklace n) or i = j + 1 or j = i + 1 ) proof let n be Nat; ::_thesis: for i, j being Nat holds ( not [i,j] in the InternalRel of (Necklace n) or i = j + 1 or j = i + 1 ) let i, j be Nat; ::_thesis: ( not [i,j] in the InternalRel of (Necklace n) or i = j + 1 or j = i + 1 ) assume [i,j] in the InternalRel of (Necklace n) ; ::_thesis: ( i = j + 1 or j = i + 1 ) then [i,j] in { [k,(k + 1)] where k is Element of NAT : k + 1 < n } \/ { [(l + 1),l] where l is Element of NAT : l + 1 < n } by Th18; then A1: ( [i,j] in { [k,(k + 1)] where k is Element of NAT : k + 1 < n } or [i,j] in { [(k + 1),k] where k is Element of NAT : k + 1 < n } ) by XBOOLE_0:def_3; ( i + 1 = j or j + 1 = i ) proof percases ( ex k being Element of NAT st ( [i,j] = [k,(k + 1)] & k + 1 < n ) or ex k being Element of NAT st ( [i,j] = [(k + 1),k] & k + 1 < n ) ) by A1; suppose ex k being Element of NAT st ( [i,j] = [k,(k + 1)] & k + 1 < n ) ; ::_thesis: ( i + 1 = j or j + 1 = i ) then consider k being Nat such that A2: [i,j] = [k,(k + 1)] and k + 1 < n ; i = k by A2, XTUPLE_0:1; hence ( i + 1 = j or j + 1 = i ) by A2, XTUPLE_0:1; ::_thesis: verum end; suppose ex k being Element of NAT st ( [i,j] = [(k + 1),k] & k + 1 < n ) ; ::_thesis: ( i + 1 = j or j + 1 = i ) then consider k being Nat such that A3: [i,j] = [(k + 1),k] and k + 1 < n ; i = k + 1 by A3, XTUPLE_0:1; hence ( i + 1 = j or j + 1 = i ) by A3, XTUPLE_0:1; ::_thesis: verum end; end; end; hence ( i = j + 1 or j = i + 1 ) ; ::_thesis: verum end; theorem Th25: :: NECKLACE:25 for n, i, j being Nat st ( i = j + 1 or j = i + 1 ) & i in the carrier of (Necklace n) & j in the carrier of (Necklace n) holds [i,j] in the InternalRel of (Necklace n) proof let n be Nat; ::_thesis: for i, j being Nat st ( i = j + 1 or j = i + 1 ) & i in the carrier of (Necklace n) & j in the carrier of (Necklace n) holds [i,j] in the InternalRel of (Necklace n) let i, j be Nat; ::_thesis: ( ( i = j + 1 or j = i + 1 ) & i in the carrier of (Necklace n) & j in the carrier of (Necklace n) implies [i,j] in the InternalRel of (Necklace n) ) assume that A1: ( i = j + 1 or j = i + 1 ) and A2: i in the carrier of (Necklace n) and A3: j in the carrier of (Necklace n) ; ::_thesis: [i,j] in the InternalRel of (Necklace n) percases ( i = j + 1 or j = i + 1 ) by A1; supposeA4: i = j + 1 ; ::_thesis: [i,j] in the InternalRel of (Necklace n) then [j,(j + 1)] in the InternalRel of (Necklace n) by A2, Th21, Th22; then [(j + 1),j] in the InternalRel of (Necklace n) ~ by RELAT_1:def_7; hence [i,j] in the InternalRel of (Necklace n) by A4, RELAT_2:13; ::_thesis: verum end; suppose j = i + 1 ; ::_thesis: [i,j] in the InternalRel of (Necklace n) hence [i,j] in the InternalRel of (Necklace n) by A3, Th21, Th22; ::_thesis: verum end; end; end; theorem Th26: :: NECKLACE:26 for n being Nat st n > 0 holds card { [(i + 1),i] where i is Element of NAT : i + 1 < n } = n - 1 proof let n be Nat; ::_thesis: ( n > 0 implies card { [(i + 1),i] where i is Element of NAT : i + 1 < n } = n - 1 ) deffunc H1( Element of NAT ) -> set = [($1 + 1),$1]; defpred S1[ Element of NAT ] means $1 + 1 < n; defpred S2[ Element of NAT ] means $1 in n -' 1; A1: for d1, d2 being Element of NAT st H1(d1) = H1(d2) holds d1 = d2 by XTUPLE_0:1; assume A2: n > 0 ; ::_thesis: card { [(i + 1),i] where i is Element of NAT : i + 1 < n } = n - 1 then A3: n >= 0 + 1 by NAT_1:13; A4: for i being Nat st i in n -' 1 holds i + 1 < n proof let i be Nat; ::_thesis: ( i in n -' 1 implies i + 1 < n ) assume i in n -' 1 ; ::_thesis: i + 1 < n then A5: i < n -' 1 by NAT_1:44; n >= 0 + 1 by A2, NAT_1:13; then i < n - 1 by A5, XREAL_1:233; hence i + 1 < n by XREAL_1:20; ::_thesis: verum end; A6: for i being Element of NAT holds ( S1[i] iff S2[i] ) proof let i be Element of NAT ; ::_thesis: ( S1[i] iff S2[i] ) thus ( i + 1 < n implies i in n -' 1 ) ::_thesis: ( S2[i] implies S1[i] ) proof assume i + 1 < n ; ::_thesis: i in n -' 1 then i < n - 1 by XREAL_1:20; then i < n -' 1 by A3, XREAL_1:233; hence i in n -' 1 by NAT_1:44; ::_thesis: verum end; thus ( S2[i] implies S1[i] ) by A4; ::_thesis: verum end; A7: { H1(i) where i is Element of NAT : S1[i] } = { H1(i) where i is Element of NAT : S2[i] } from FRAENKEL:sch_3(A6); A8: n -' 1 c= NAT ; n -' 1, { H1(i) where i is Element of NAT : i in n -' 1 } are_equipotent from FUNCT_7:sch_4(A8, A1); hence card { [(i + 1),i] where i is Element of NAT : i + 1 < n } = card (n -' 1) by A7, CARD_1:5 .= n -' 1 by CARD_1:def_2 .= n - 1 by A3, XREAL_1:233 ; ::_thesis: verum end; theorem Th27: :: NECKLACE:27 for n being Nat st n > 0 holds card the InternalRel of (Necklace n) = 2 * (n - 1) proof let n be Nat; ::_thesis: ( n > 0 implies card the InternalRel of (Necklace n) = 2 * (n - 1) ) deffunc H1( Element of NAT ) -> Element of NAT = $1 + 1; deffunc H2( Element of NAT ) -> Element of NAT = $1; defpred S1[ Element of NAT ] means $1 + 1 < n; set A = { [i,(i + 1)] where i is Element of NAT : i + 1 < n } ; set B = { [H1(i),H2(i)] where i is Element of NAT : S1[i] } ; A1: { [i,(i + 1)] where i is Element of NAT : i + 1 < n } is Relation-like proof let x be set ; :: according to RELAT_1:def_1 ::_thesis: ( not x in { [i,(i + 1)] where i is Element of NAT : i + 1 < n } or ex b1, b2 being set st x = [b1,b2] ) assume x in { [i,(i + 1)] where i is Element of NAT : i + 1 < n } ; ::_thesis: ex b1, b2 being set st x = [b1,b2] then ex i being Element of NAT st ( x = [i,(i + 1)] & i + 1 < n ) ; hence ex b1, b2 being set st x = [b1,b2] ; ::_thesis: verum end; A2: the InternalRel of (Necklace n) = { [i,(i + 1)] where i is Element of NAT : i + 1 < n } \/ { [H1(i),H2(i)] where i is Element of NAT : S1[i] } by Th18; assume A3: n > 0 ; ::_thesis: card the InternalRel of (Necklace n) = 2 * (n - 1) then n >= 0 + 1 by NAT_1:13; then A4: n -' 1 = n - 1 by XREAL_1:233; { [i,(i + 1)] where i is Element of NAT : i + 1 < n } = the InternalRel of (n -SuccRelStr) by Def6; then A5: card { [i,(i + 1)] where i is Element of NAT : i + 1 < n } = n - 1 by A3, Th16; reconsider A = { [i,(i + 1)] where i is Element of NAT : i + 1 < n } as Relation by A1; A6: A = { [H2(i),H1(i)] where i is Element of NAT : S1[i] } ; A7: A ~ = { [H1(i),H2(i)] where i is Element of NAT : S1[i] } from NECKLACE:sch_1(A6); A8: A misses { [H1(i),H2(i)] where i is Element of NAT : S1[i] } proof assume A meets { [H1(i),H2(i)] where i is Element of NAT : S1[i] } ; ::_thesis: contradiction then consider x being set such that A9: x in A and A10: x in { [H1(i),H2(i)] where i is Element of NAT : S1[i] } by XBOOLE_0:3; consider y, z being set such that A11: x = [y,z] by A9, RELAT_1:def_1; [z,y] in A by A7, A10, A11, RELAT_1:def_7; then consider j being Element of NAT such that A12: [z,y] = [j,(j + 1)] and j + 1 < n ; A13: ( z = j & y = j + 1 ) by A12, XTUPLE_0:1; consider i being Element of NAT such that A14: [y,z] = [i,(i + 1)] and i + 1 < n by A9, A11; ( y = i & z = i + 1 ) by A14, XTUPLE_0:1; hence contradiction by A13; ::_thesis: verum end; card { [H1(i),H2(i)] where i is Element of NAT : S1[i] } = n - 1 by A3, Th26; then card the InternalRel of (Necklace n) = (card (n - 1)) +` (card (n - 1)) by A2, A5, A8, CARD_2:35 .= card ((n -' 1) + (n -' 1)) by A4, CARD_2:38 .= 2 * (n - 1) by A4, CARD_1:def_2 ; hence card the InternalRel of (Necklace n) = 2 * (n - 1) ; ::_thesis: verum end; theorem :: NECKLACE:28 Necklace 1, ComplRelStr (Necklace 1) are_isomorphic proof set f = 0 .--> 0; set S = Necklace 1; set T = ComplRelStr (Necklace 1); A1: the carrier of (Necklace 1) = the carrier of (ComplRelStr (Necklace 1)) by Def8; the carrier of (Necklace 1) = {0} by Th20, CARD_1:49; then reconsider g = 0 .--> 0 as Function of (Necklace 1),(ComplRelStr (Necklace 1)) by Def8; A2: rng g = {0} by FUNCOP_1:8; A3: dom g = {0} by FUNCOP_1:13; for y, x being set holds ( y in rng g & x = g . y iff ( x in dom g & y = g . x ) ) proof let x, y be set ; ::_thesis: ( x in rng g & y = g . x iff ( y in dom g & x = g . y ) ) A4: ( x in dom g & y = g . x implies ( y in rng g & x = g . y ) ) proof assume that A5: x in dom g and A6: y = g . x ; ::_thesis: ( y in rng g & x = g . y ) the carrier of (Necklace 1) = {0} by Th20, CARD_1:49; then A7: x = 0 by A5, TARSKI:def_1; then y = 0 by A6, FUNCOP_1:72; hence ( y in rng g & x = g . y ) by A2, A7, FUNCOP_1:72, TARSKI:def_1; ::_thesis: verum end; ( y in rng g & x = g . y implies ( x in dom g & y = g . x ) ) proof assume that A8: y in rng g and A9: x = g . y ; ::_thesis: ( x in dom g & y = g . x ) A10: y = 0 by A2, A8, TARSKI:def_1; then x = 0 by A9, FUNCOP_1:72; hence ( x in dom g & y = g . x ) by A3, A10, FUNCOP_1:72, TARSKI:def_1; ::_thesis: verum end; hence ( x in rng g & y = g . x iff ( y in dom g & x = g . y ) ) by A2, A4, FUNCOP_1:13; ::_thesis: verum end; then reconsider h = g " as Function of (ComplRelStr (Necklace 1)),(Necklace 1) by A1, A3, A2, FUNCT_1:32; A11: h is monotone proof let x, y be Element of (ComplRelStr (Necklace 1)); :: according to ORDERS_3:def_5 ::_thesis: ( not x <= y or for b1, b2 being Element of the carrier of (Necklace 1) holds ( not b1 = h . x or not b2 = h . y or b1 <= b2 ) ) assume x <= y ; ::_thesis: for b1, b2 being Element of the carrier of (Necklace 1) holds ( not b1 = h . x or not b2 = h . y or b1 <= b2 ) then [x,y] in the InternalRel of (ComplRelStr (Necklace 1)) by ORDERS_2:def_5; then [x,y] in ( the InternalRel of (Necklace 1) `) \ (id the carrier of (Necklace 1)) by Def8; then not [x,y] in id the carrier of (Necklace 1) by XBOOLE_0:def_5; then A12: ( not x in the carrier of (Necklace 1) or x <> y ) by RELAT_1:def_10; let a, b be Element of (Necklace 1); ::_thesis: ( not a = h . x or not b = h . y or a <= b ) assume that a = h . x and b = h . y ; ::_thesis: a <= b A13: x in the carrier of (ComplRelStr (Necklace 1)) ; A14: the carrier of (ComplRelStr (Necklace 1)) = 1 by A1, Th20; then reconsider i = x, j = y as Nat by Th3; A15: j = 0 by A14, CARD_1:49, TARSKI:def_1; A16: i = 0 by A14, CARD_1:49, TARSKI:def_1; A17: ( i + 1 <> j & j + 1 <> i & i <> j ) proof hereby ::_thesis: i <> j assume A18: ( i + 1 = j or j + 1 = i ) ; ::_thesis: contradiction percases ( i + 1 = j or j + 1 = i ) by A18; suppose i + 1 = j ; ::_thesis: contradiction hence contradiction by A14, A16, NAT_1:44; ::_thesis: verum end; suppose j + 1 = i ; ::_thesis: contradiction hence contradiction by A14, A15, NAT_1:44; ::_thesis: verum end; end; end; thus i <> j by A12, A13, Def8; ::_thesis: verum end; A19: y = 0 by A14, CARD_1:49, TARSKI:def_1; the carrier of (ComplRelStr (Necklace 1)) = {0} by A1, Th20, CARD_1:49; hence a <= b by A17, A19, TARSKI:def_1; ::_thesis: verum end; g is monotone proof let x, y be Element of (Necklace 1); :: according to ORDERS_3:def_5 ::_thesis: ( not x <= y or for b1, b2 being Element of the carrier of (ComplRelStr (Necklace 1)) holds ( not b1 = g . x or not b2 = g . y or b1 <= b2 ) ) assume x <= y ; ::_thesis: for b1, b2 being Element of the carrier of (ComplRelStr (Necklace 1)) holds ( not b1 = g . x or not b2 = g . y or b1 <= b2 ) then A20: [x,y] in the InternalRel of (Necklace 1) by ORDERS_2:def_5; the carrier of (Necklace 1) = 1 by Th20; then reconsider i = x, j = y as Nat by Th3; let a, b be Element of (ComplRelStr (Necklace 1)); ::_thesis: ( not a = g . x or not b = g . y or a <= b ) assume that a = g . x and b = g . y ; ::_thesis: a <= b the carrier of (Necklace 1) = {0} by Th20, CARD_1:49; then A21: ( x = 0 & y = 0 ) by TARSKI:def_1; ( i = j + 1 or j = i + 1 ) by A20, Th24; hence a <= b by A21; ::_thesis: verum end; then g is isomorphic by A11, WAYBEL_0:def_38; hence Necklace 1, ComplRelStr (Necklace 1) are_isomorphic by WAYBEL_1:def_8; ::_thesis: verum end; theorem :: NECKLACE:29 Necklace 4, ComplRelStr (Necklace 4) are_isomorphic proof set g = (0,1) --> (1,3); set h = (2,3) --> (0,2); set f = ((0,1) --> (1,3)) +* ((2,3) --> (0,2)); set S = Necklace 4; set T = ComplRelStr (Necklace 4); A1: rng ((2,3) --> (0,2)) = {0,2} by FUNCT_4:64; A2: rng ((0,1) --> (1,3)) = {1,3} by FUNCT_4:64; A3: rng (((0,1) --> (1,3)) +* ((2,3) --> (0,2))) c= the carrier of (ComplRelStr (Necklace 4)) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng (((0,1) --> (1,3)) +* ((2,3) --> (0,2))) or x in the carrier of (ComplRelStr (Necklace 4)) ) assume A4: x in rng (((0,1) --> (1,3)) +* ((2,3) --> (0,2))) ; ::_thesis: x in the carrier of (ComplRelStr (Necklace 4)) A5: rng (((0,1) --> (1,3)) +* ((2,3) --> (0,2))) c= (rng ((0,1) --> (1,3))) \/ (rng ((2,3) --> (0,2))) by FUNCT_4:17; (rng ((0,1) --> (1,3))) \/ (rng ((2,3) --> (0,2))) = {1,3,0,2} by A2, A1, ENUMSET1:5 .= {0,1,2,3} by ENUMSET1:69 ; then x in 4 by A4, A5, CARD_1:52; then x in the carrier of (Necklace 4) by Th20; hence x in the carrier of (ComplRelStr (Necklace 4)) by Def8; ::_thesis: verum end; A6: dom (((0,1) --> (1,3)) +* ((2,3) --> (0,2))) = (dom ((0,1) --> (1,3))) \/ (dom ((2,3) --> (0,2))) by FUNCT_4:def_1 .= {0,1} \/ (dom ((2,3) --> (0,2))) by FUNCT_4:62 .= {0,1} \/ {2,3} by FUNCT_4:62 .= {0,1,2,3} by ENUMSET1:5 ; then A7: dom (((0,1) --> (1,3)) +* ((2,3) --> (0,2))) = the carrier of (Necklace 4) by Th20, CARD_1:52; then reconsider f = ((0,1) --> (1,3)) +* ((2,3) --> (0,2)) as Function of (Necklace 4),(ComplRelStr (Necklace 4)) by A3, FUNCT_2:def_1, RELSET_1:4; take f ; :: according to WAYBEL_1:def_8 ::_thesis: f is isomorphic percases ( ( not Necklace 4 is empty & not ComplRelStr (Necklace 4) is empty ) or Necklace 4 is empty or ComplRelStr (Necklace 4) is empty ) ; :: according to WAYBEL_0:def_38 casethat not Necklace 4 is empty and not ComplRelStr (Necklace 4) is empty ; ::_thesis: ( f is one-to-one & f is monotone & ex b1 being Element of bool [: the carrier of (ComplRelStr (Necklace 4)), the carrier of (Necklace 4):] st ( b1 = f " & b1 is monotone ) ) set A = the InternalRel of (ComplRelStr (Necklace 4)); A8: rng (0 .--> 1) misses rng (1 .--> 3) proof assume rng (0 .--> 1) meets rng (1 .--> 3) ; ::_thesis: contradiction then consider x being set such that A9: x in rng (0 .--> 1) and A10: x in rng (1 .--> 3) by XBOOLE_0:3; rng (0 .--> 1) = {1} by FUNCOP_1:8; then ( rng (1 .--> 3) = {3} & x = 1 ) by A9, FUNCOP_1:8, TARSKI:def_1; hence contradiction by A10, TARSKI:def_1; ::_thesis: verum end; A11: rng ((0,1) --> (1,3)) misses rng ((2,3) --> (0,2)) proof assume rng ((0,1) --> (1,3)) meets rng ((2,3) --> (0,2)) ; ::_thesis: contradiction then consider x being set such that A12: x in rng ((0,1) --> (1,3)) and A13: x in rng ((2,3) --> (0,2)) by XBOOLE_0:3; ( x = 1 or x = 3 ) by A2, A12, TARSKI:def_2; hence contradiction by A1, A13, TARSKI:def_2; ::_thesis: verum end; set B = {[1,3],[3,1],[0,2],[2,0],[0,3],[3,0]}; A14: rng (2 .--> 0) misses rng (3 .--> 2) proof assume rng (2 .--> 0) meets rng (3 .--> 2) ; ::_thesis: contradiction then consider x being set such that A15: x in rng (2 .--> 0) and A16: x in rng (3 .--> 2) by XBOOLE_0:3; rng (2 .--> 0) = {0} by FUNCOP_1:8; then ( rng (3 .--> 2) = {2} & x = 0 ) by A15, FUNCOP_1:8, TARSKI:def_1; hence contradiction by A16, TARSKI:def_1; ::_thesis: verum end; (2,3) --> (0,2) = (2 .--> 0) +* (3 .--> 2) by FUNCT_4:def_4; then A17: (2,3) --> (0,2) is one-to-one by A14, FUNCT_4:92; A18: dom ((0,1) --> (1,3)) misses dom ((2,3) --> (0,2)) proof assume dom ((0,1) --> (1,3)) meets dom ((2,3) --> (0,2)) ; ::_thesis: contradiction then consider x being set such that A19: x in dom ((0,1) --> (1,3)) and A20: x in dom ((2,3) --> (0,2)) by XBOOLE_0:3; ( x = 0 or x = 1 ) by A19, TARSKI:def_2; hence contradiction by A20, TARSKI:def_2; ::_thesis: verum end; then A21: rng f = (rng ((0,1) --> (1,3))) \/ (rng ((2,3) --> (0,2))) by FRECHET:35, PARTFUN1:56 .= {1,3,0,2} by A2, A1, ENUMSET1:5 .= {0,1,2,3} by ENUMSET1:69 .= the carrier of (Necklace 4) by Th20, CARD_1:52 .= the carrier of (ComplRelStr (Necklace 4)) by Def8 ; (0,1) --> (1,3) = (0 .--> 1) +* (1 .--> 3) by FUNCT_4:def_4; then A22: (0,1) --> (1,3) is one-to-one by A8, FUNCT_4:92; hence f is V7() by A17, A11, FUNCT_4:92; ::_thesis: ( f is monotone & ex b1 being Element of bool [: the carrier of (ComplRelStr (Necklace 4)), the carrier of (Necklace 4):] st ( b1 = f " & b1 is monotone ) ) then reconsider F = f " as Function of (ComplRelStr (Necklace 4)),(Necklace 4) by A21, FUNCT_2:25; A23: {[1,3],[3,1],[0,2],[2,0],[0,3],[3,0]} c= the InternalRel of (ComplRelStr (Necklace 4)) proof set C = the carrier of (Necklace 4); let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {[1,3],[3,1],[0,2],[2,0],[0,3],[3,0]} or x in the InternalRel of (ComplRelStr (Necklace 4)) ) assume x in {[1,3],[3,1],[0,2],[2,0],[0,3],[3,0]} ; ::_thesis: x in the InternalRel of (ComplRelStr (Necklace 4)) then A24: ( x = [1,3] or x = [3,1] or x = [0,2] or x = [2,0] or x = [0,3] or x = [3,0] ) by ENUMSET1:def_4; A25: ( 2 in the carrier of (Necklace 4) & 3 in the carrier of (Necklace 4) ) by A6, A7, ENUMSET1:def_2; ( 0 in the carrier of (Necklace 4) & 1 in the carrier of (Necklace 4) ) by A6, A7, ENUMSET1:def_2; then reconsider x9 = x as Element of [: the carrier of (Necklace 4), the carrier of (Necklace 4):] by A24, A25, ZFMISC_1:87; not x9 in the InternalRel of (Necklace 4) proof assume x9 in the InternalRel of (Necklace 4) ; ::_thesis: contradiction then consider i being Element of NAT such that i + 1 < 4 and A26: ( x9 = [i,(i + 1)] or x9 = [(i + 1),i] ) by Th19; ( ( i = 1 & i + 1 = 3 ) or ( i = 3 & i + 1 = 1 ) or ( i = 0 & i + 1 = 2 ) or ( i = 2 & i + 1 = 0 ) or ( i = 0 & i + 1 = 3 ) or ( i = 3 & i + 1 = 0 ) ) by A24, A26, XTUPLE_0:1; hence contradiction ; ::_thesis: verum end; then A27: x9 in the InternalRel of (Necklace 4) ` by SUBSET_1:29; not x in id the carrier of (Necklace 4) by A24, RELAT_1:def_10; then x in ( the InternalRel of (Necklace 4) `) \ (id the carrier of (Necklace 4)) by A27, XBOOLE_0:def_5; hence x in the InternalRel of (ComplRelStr (Necklace 4)) by Def8; ::_thesis: verum end; thus f is monotone ::_thesis: ex b1 being Element of bool [: the carrier of (ComplRelStr (Necklace 4)), the carrier of (Necklace 4):] st ( b1 = f " & b1 is monotone ) proof A28: dom ((2,3) --> (0,2)) = {2,3} by FUNCT_4:62; then 2 in dom ((2,3) --> (0,2)) by TARSKI:def_2; then A29: f . 2 = ((2,3) --> (0,2)) . 2 by FUNCT_4:13 .= 0 by FUNCT_4:63 ; 3 in dom ((2,3) --> (0,2)) by A28, TARSKI:def_2; then A30: f . 3 = ((2,3) --> (0,2)) . 3 by FUNCT_4:13 .= 2 by FUNCT_4:63 ; A31: dom ((0,1) --> (1,3)) = {0,1} by FUNCT_4:62; then 0 in dom ((0,1) --> (1,3)) by TARSKI:def_2; then A32: f . 0 = ((0,1) --> (1,3)) . 0 by A18, FUNCT_4:16 .= 1 by FUNCT_4:63 ; 1 in dom ((0,1) --> (1,3)) by A31, TARSKI:def_2; then A33: f . 1 = ((0,1) --> (1,3)) . 1 by A18, FUNCT_4:16 .= 3 by FUNCT_4:63 ; let x, y be Element of (Necklace 4); :: according to ORDERS_3:def_5 ::_thesis: ( not x <= y or for b1, b2 being Element of the carrier of (ComplRelStr (Necklace 4)) holds ( not b1 = f . x or not b2 = f . y or b1 <= b2 ) ) assume x <= y ; ::_thesis: for b1, b2 being Element of the carrier of (ComplRelStr (Necklace 4)) holds ( not b1 = f . x or not b2 = f . y or b1 <= b2 ) then A34: [x,y] in the InternalRel of (Necklace 4) by ORDERS_2:def_5; the carrier of (Necklace 4) = 4 by Th20; then reconsider i = x, j = y as Nat by Th3; A35: ( i = j + 1 or j = i + 1 ) by A34, Th24; let a, b be Element of (ComplRelStr (Necklace 4)); ::_thesis: ( not a = f . x or not b = f . y or a <= b ) assume A36: ( a = f . x & b = f . y ) ; ::_thesis: a <= b percases ( ( x = 0 & y = 0 ) or ( x = 0 & y = 1 ) or ( x = 0 & y = 2 ) or ( x = 0 & y = 3 ) or ( x = 1 & y = 0 ) or ( x = 1 & y = 1 ) or ( x = 1 & y = 2 ) or ( x = 1 & y = 3 ) or ( x = 2 & y = 0 ) or ( x = 2 & y = 1 ) or ( x = 2 & y = 2 ) or ( x = 2 & y = 3 ) or ( x = 3 & y = 0 ) or ( x = 3 & y = 1 ) or ( x = 3 & y = 2 ) or ( x = 3 & y = 3 ) ) by A6, A7, ENUMSET1:def_2; suppose ( x = 0 & y = 0 ) ; ::_thesis: a <= b hence a <= b by A35; ::_thesis: verum end; suppose ( x = 0 & y = 1 ) ; ::_thesis: a <= b then [a,b] in {[1,3],[3,1],[0,2],[2,0],[0,3],[3,0]} by A36, A32, A33, ENUMSET1:def_4; hence a <= b by A23, ORDERS_2:def_5; ::_thesis: verum end; suppose ( x = 0 & y = 2 ) ; ::_thesis: a <= b hence a <= b by A35; ::_thesis: verum end; suppose ( x = 0 & y = 3 ) ; ::_thesis: a <= b hence a <= b by A35; ::_thesis: verum end; suppose ( x = 1 & y = 0 ) ; ::_thesis: a <= b then [a,b] in {[1,3],[3,1],[0,2],[2,0],[0,3],[3,0]} by A36, A32, A33, ENUMSET1:def_4; hence a <= b by A23, ORDERS_2:def_5; ::_thesis: verum end; suppose ( x = 1 & y = 1 ) ; ::_thesis: a <= b hence a <= b by A35; ::_thesis: verum end; suppose ( x = 1 & y = 2 ) ; ::_thesis: a <= b then [a,b] in {[1,3],[3,1],[0,2],[2,0],[0,3],[3,0]} by A36, A33, A29, ENUMSET1:def_4; hence a <= b by A23, ORDERS_2:def_5; ::_thesis: verum end; suppose ( x = 1 & y = 3 ) ; ::_thesis: a <= b hence a <= b by A35; ::_thesis: verum end; suppose ( x = 2 & y = 0 ) ; ::_thesis: a <= b hence a <= b by A35; ::_thesis: verum end; suppose ( x = 2 & y = 1 ) ; ::_thesis: a <= b then [a,b] in {[1,3],[3,1],[0,2],[2,0],[0,3],[3,0]} by A36, A33, A29, ENUMSET1:def_4; hence a <= b by A23, ORDERS_2:def_5; ::_thesis: verum end; suppose ( x = 2 & y = 2 ) ; ::_thesis: a <= b hence a <= b by A35; ::_thesis: verum end; suppose ( x = 2 & y = 3 ) ; ::_thesis: a <= b then [a,b] in {[1,3],[3,1],[0,2],[2,0],[0,3],[3,0]} by A36, A29, A30, ENUMSET1:def_4; hence a <= b by A23, ORDERS_2:def_5; ::_thesis: verum end; suppose ( x = 3 & y = 0 ) ; ::_thesis: a <= b hence a <= b by A35; ::_thesis: verum end; suppose ( x = 3 & y = 1 ) ; ::_thesis: a <= b hence a <= b by A35; ::_thesis: verum end; suppose ( x = 3 & y = 2 ) ; ::_thesis: a <= b then [a,b] in {[1,3],[3,1],[0,2],[2,0],[0,3],[3,0]} by A36, A29, A30, ENUMSET1:def_4; hence a <= b by A23, ORDERS_2:def_5; ::_thesis: verum end; suppose ( x = 3 & y = 3 ) ; ::_thesis: a <= b hence a <= b by A35; ::_thesis: verum end; end; end; take F ; ::_thesis: ( F = f " & F is monotone ) thus F = f " ; ::_thesis: F is monotone thus F is monotone ::_thesis: verum proof let x, y be Element of (ComplRelStr (Necklace 4)); :: according to ORDERS_3:def_5 ::_thesis: ( not x <= y or for b1, b2 being Element of the carrier of (Necklace 4) holds ( not b1 = F . x or not b2 = F . y or b1 <= b2 ) ) assume x <= y ; ::_thesis: for b1, b2 being Element of the carrier of (Necklace 4) holds ( not b1 = F . x or not b2 = F . y or b1 <= b2 ) then [x,y] in the InternalRel of (ComplRelStr (Necklace 4)) by ORDERS_2:def_5; then A37: [x,y] in ( the InternalRel of (Necklace 4) `) \ (id the carrier of (Necklace 4)) by Def8; then not [x,y] in id the carrier of (Necklace 4) by XBOOLE_0:def_5; then A38: ( not x in the carrier of (Necklace 4) or x <> y ) by RELAT_1:def_10; ( [x,y] in the InternalRel of (Necklace 4) ` implies not [x,y] in the InternalRel of (Necklace 4) ) by XBOOLE_0:def_5; then A39: not [x,y] in { [k,(k + 1)] where k is Element of NAT : k + 1 < 4 } \/ { [(l + 1),l] where l is Element of NAT : l + 1 < 4 } by A37, Th18, XBOOLE_0:def_5; then A40: not [x,y] in { [(k + 1),k] where k is Element of NAT : k + 1 < 4 } by XBOOLE_0:def_3; A41: the carrier of (ComplRelStr (Necklace 4)) = the carrier of (Necklace 4) by Def8 .= 4 by Th20 ; then ( x is natural & y is natural ) by Th3; then reconsider i = x, j = y as Element of NAT by ORDINAL1:def_12; A42: x in the carrier of (ComplRelStr (Necklace 4)) ; A43: not [x,y] in { [k,(k + 1)] where k is Element of NAT : k + 1 < 4 } by A39, XBOOLE_0:def_3; A44: ( i + 1 <> j & j + 1 <> i & i <> j ) proof hereby ::_thesis: i <> j assume A45: ( i + 1 = j or j + 1 = i ) ; ::_thesis: contradiction percases ( i + 1 = j or j + 1 = i ) by A45; supposeA46: i + 1 = j ; ::_thesis: contradiction then i + 1 < 4 by A41, NAT_1:44; hence contradiction by A43, A46; ::_thesis: verum end; supposeA47: j + 1 = i ; ::_thesis: contradiction then j + 1 < 4 by A41, NAT_1:44; hence contradiction by A40, A47; ::_thesis: verum end; end; end; thus i <> j by A38, A42, Def8; ::_thesis: verum end; A48: ((2,3) --> (0,2)) " = (0,2) --> (2,3) by Th10; then A49: dom (((2,3) --> (0,2)) ") = {0,2} by FUNCT_4:62; then A50: 0 in dom (((2,3) --> (0,2)) ") by TARSKI:def_2; A51: F . 0 = ((((0,1) --> (1,3)) ") +* (((2,3) --> (0,2)) ")) . 0 by A22, A17, A18, A11, Th7 .= (((2,3) --> (0,2)) ") . 0 by A50, FUNCT_4:13 .= 2 by A48, FUNCT_4:63 ; A52: ((0,1) --> (1,3)) " = (1,3) --> (0,1) by Th10; then A53: dom (((0,1) --> (1,3)) ") = {1,3} by FUNCT_4:62; then A54: 1 in dom (((0,1) --> (1,3)) ") by TARSKI:def_2; A55: dom (((0,1) --> (1,3)) ") misses dom (((2,3) --> (0,2)) ") proof assume dom (((0,1) --> (1,3)) ") meets dom (((2,3) --> (0,2)) ") ; ::_thesis: contradiction then consider x being set such that A56: x in dom (((0,1) --> (1,3)) ") and A57: x in dom (((2,3) --> (0,2)) ") by XBOOLE_0:3; ( x = 1 or x = 3 ) by A53, A56, TARSKI:def_2; hence contradiction by A49, A57, TARSKI:def_2; ::_thesis: verum end; A58: F . 1 = ((((0,1) --> (1,3)) ") +* (((2,3) --> (0,2)) ")) . 1 by A22, A17, A18, A11, Th7 .= (((0,1) --> (1,3)) ") . 1 by A55, A54, FUNCT_4:16 .= 0 by A52, FUNCT_4:63 ; A59: 2 in dom (((2,3) --> (0,2)) ") by A49, TARSKI:def_2; A60: F . 2 = ((((0,1) --> (1,3)) ") +* (((2,3) --> (0,2)) ")) . 2 by A22, A17, A18, A11, Th7 .= (((2,3) --> (0,2)) ") . 2 by A59, FUNCT_4:13 .= 3 by A48, FUNCT_4:63 ; A61: 3 in dom (((0,1) --> (1,3)) ") by A53, TARSKI:def_2; A62: F . 3 = ((((0,1) --> (1,3)) ") +* (((2,3) --> (0,2)) ")) . 3 by A22, A17, A18, A11, Th7 .= (((0,1) --> (1,3)) ") . 3 by A55, A61, FUNCT_4:16 .= 1 by A52, FUNCT_4:63 ; let a, b be Element of (Necklace 4); ::_thesis: ( not a = F . x or not b = F . y or a <= b ) assume that A63: a = F . x and A64: b = F . y ; ::_thesis: a <= b percases ( ( x = 0 & y = 0 ) or ( x = 0 & y = 1 ) or ( x = 0 & y = 2 ) or ( x = 0 & y = 3 ) or ( x = 1 & y = 0 ) or ( x = 1 & y = 1 ) or ( x = 1 & y = 2 ) or ( x = 1 & y = 3 ) or ( x = 2 & y = 0 ) or ( x = 2 & y = 1 ) or ( x = 2 & y = 2 ) or ( x = 2 & y = 3 ) or ( x = 3 & y = 0 ) or ( x = 3 & y = 1 ) or ( x = 3 & y = 2 ) or ( x = 3 & y = 3 ) ) by A41, CARD_1:52, ENUMSET1:def_2; suppose ( x = 0 & y = 0 ) ; ::_thesis: a <= b hence a <= b by A44; ::_thesis: verum end; suppose ( x = 0 & y = 1 ) ; ::_thesis: a <= b hence a <= b by A44; ::_thesis: verum end; supposeA65: ( x = 0 & y = 2 ) ; ::_thesis: a <= b then b = 2 + 1 by A64, A60; then [a,b] in the InternalRel of (Necklace 4) by A63, A51, A65, Th25; hence a <= b by ORDERS_2:def_5; ::_thesis: verum end; supposeA66: ( x = 0 & y = 3 ) ; ::_thesis: a <= b then a = 1 + 1 by A63, A51; then [a,b] in the InternalRel of (Necklace 4) by A64, A62, A66, Th25; hence a <= b by ORDERS_2:def_5; ::_thesis: verum end; suppose ( x = 1 & y = 0 ) ; ::_thesis: a <= b hence a <= b by A44; ::_thesis: verum end; suppose ( x = 1 & y = 1 ) ; ::_thesis: a <= b hence a <= b by A44; ::_thesis: verum end; suppose ( x = 1 & y = 2 ) ; ::_thesis: a <= b hence a <= b by A44; ::_thesis: verum end; supposeA67: ( x = 1 & y = 3 ) ; ::_thesis: a <= b then b = 0 + 1 by A64, A62; then [a,b] in the InternalRel of (Necklace 4) by A63, A58, A67, Th25; hence a <= b by ORDERS_2:def_5; ::_thesis: verum end; supposeA68: ( x = 2 & y = 0 ) ; ::_thesis: a <= b then a = 2 + 1 by A63, A60; then [a,b] in the InternalRel of (Necklace 4) by A64, A51, A68, Th25; hence a <= b by ORDERS_2:def_5; ::_thesis: verum end; suppose ( x = 2 & y = 1 ) ; ::_thesis: a <= b hence a <= b by A44; ::_thesis: verum end; suppose ( x = 2 & y = 2 ) ; ::_thesis: a <= b hence a <= b by A44; ::_thesis: verum end; suppose ( x = 2 & y = 3 ) ; ::_thesis: a <= b hence a <= b by A44; ::_thesis: verum end; supposeA69: ( x = 3 & y = 0 ) ; ::_thesis: a <= b then b = 1 + 1 by A64, A51; then [a,b] in the InternalRel of (Necklace 4) by A63, A62, A69, Th25; hence a <= b by ORDERS_2:def_5; ::_thesis: verum end; supposeA70: ( x = 3 & y = 1 ) ; ::_thesis: a <= b then a = 0 + 1 by A63, A62; then [a,b] in the InternalRel of (Necklace 4) by A64, A58, A70, Th25; hence a <= b by ORDERS_2:def_5; ::_thesis: verum end; suppose ( x = 3 & y = 2 ) ; ::_thesis: a <= b hence a <= b by A44; ::_thesis: verum end; suppose ( x = 3 & y = 3 ) ; ::_thesis: a <= b hence a <= b by A44; ::_thesis: verum end; end; end; end; case ( Necklace 4 is empty or ComplRelStr (Necklace 4) is empty ) ; ::_thesis: ( Necklace 4 is empty & ComplRelStr (Necklace 4) is empty ) hence ( Necklace 4 is empty & ComplRelStr (Necklace 4) is empty ) ; ::_thesis: verum end; end; end; theorem :: NECKLACE:30 for n being Nat holds ( not Necklace n, ComplRelStr (Necklace n) are_isomorphic or n = 0 or n = 1 or n = 4 ) proof 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 ) set S = Necklace n; set T = ComplRelStr (Necklace n); card n = n by CARD_1:def_2; then A2: card [:n,n:] = n * n by CARD_2:46; assume A3: ( not n = 0 & not n = 1 & not n = 4 ) ; ::_thesis: contradiction then ( n = 2 or n = 3 or n > 4 ) by NAT_1:28; then A4: card the InternalRel of (Necklace n) = 2 * (n - 1) by Th27; A5: ((n * n) - (2 * (n - 1))) - n <> 2 * (n - 1) proof A6: delta (1,(- 5),4) = ((- 5) ^2) - ((4 * 1) * 4) by QUIN_1:def_1 .= 9 ; assume not ((n * n) - (2 * (n - 1))) - n <> 2 * (n - 1) ; ::_thesis: contradiction then ((1 * (n ^2)) + ((- 5) * n)) + 4 = 0 ; then ( n = ((- (- 5)) - (sqrt (delta (1,(- 5),4)))) / (2 * 1) or n = ((- (- 5)) + (sqrt (delta (1,(- 5),4)))) / (2 * 1) ) by A6, QUIN_1:15; then ( n = (5 - (sqrt (3 ^2))) / 2 or n = (5 + (sqrt (3 ^2))) / 2 ) by A6; then A7: ( n = (5 - 3) / 2 or n = (5 + 3) / 2 ) by SQUARE_1:22; percases ( n = 1 or n = 4 ) by A7; suppose n = 1 ; ::_thesis: contradiction hence contradiction by A3; ::_thesis: verum end; suppose n = 4 ; ::_thesis: contradiction hence contradiction by A3; ::_thesis: verum end; end; end; A8: id the carrier of (Necklace n) misses the InternalRel of (Necklace n) proof assume not id the carrier of (Necklace n) misses the InternalRel of (Necklace n) ; ::_thesis: contradiction then consider x being set such that A9: x in id the carrier of (Necklace n) and A10: x in the InternalRel of (Necklace n) by XBOOLE_0:3; consider i being Element of NAT such that i + 1 < n and A11: ( x = [i,(i + 1)] or x = [(i + 1),i] ) by A10, Th19; consider x1, x2 being set such that A12: x = [x1,x2] by A9, RELAT_1:def_1; A13: x1 = x2 by A9, A12, RELAT_1:def_10; percases ( [x1,x2] = [i,(i + 1)] or [x1,x2] = [(i + 1),i] ) by A12, A11; suppose [x1,x2] = [i,(i + 1)] ; ::_thesis: contradiction then ( x1 = i & x2 = i + 1 ) by XTUPLE_0:1; hence contradiction by A13; ::_thesis: verum end; suppose [x1,x2] = [(i + 1),i] ; ::_thesis: contradiction then ( x1 = i + 1 & x2 = i ) by XTUPLE_0:1; hence contradiction by A13; ::_thesis: verum end; end; end; the carrier of (Necklace n) = n by Th20; then A14: card ( the InternalRel of (Necklace n) `) = (n * n) - (2 * (n - 1)) by A4, A2, CARD_2:44; ( the carrier of (Necklace n) = n & n = card n ) by Th20, CARD_1:def_2; then A15: card (id the carrier of (Necklace n)) = n by Th5; card the InternalRel of (ComplRelStr (Necklace n)) = card (( the InternalRel of (Necklace n) `) \ (id the carrier of (Necklace n))) by Def8 .= ((n * n) - (2 * (n - 1))) - n by A14, A15, A8, CARD_2:44, XBOOLE_1:86 ; hence contradiction by A1, A4, A5, Th17; ::_thesis: verum end;