:: 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;