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
object ;
TARSKI:def 3 ( 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)))
;
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 Th19;
hence
x in the
carrier of
(ComplRelStr (Necklace 4))
by Def8;
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 Th19, 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
; WAYBEL_1:def 8 f is isomorphic
per cases
( ( not Necklace 4 is empty & not ComplRelStr (Necklace 4) is empty ) or Necklace 4 is empty or ComplRelStr (Necklace 4) is empty )
;
WAYBEL_0:def 38case that
not
Necklace 4 is
empty
and
not
ComplRelStr (Necklace 4) is
empty
;
( 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)
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))
;
contradiction
then consider x being
object 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;
verum
end; set B =
{[1,3],[3,1],[0,2],[2,0],[0,3],[3,0]};
A14:
rng (2 .--> 0) misses rng (3 .--> 2)
(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))
;
contradiction
then consider x being
object 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;
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 Th19, 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;
( 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
object ;
TARSKI:def 3 ( 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]}
;
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)
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;
verum
end; thus
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 )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);
ORDERS_3:def 5 ( 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
;
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 Th19;
then
(
x in Segm 4 &
y in Segm 4 )
;
then reconsider i =
x,
j =
y as
Nat ;
A35:
(
i = j + 1 or
j = i + 1 )
by A34, Th23;
let a,
b be
Element of
(ComplRelStr (Necklace 4));
( not a = f . x or not b = f . y or a <= b )
assume A36:
(
a = f . x &
b = f . y )
;
a <= b
per cases
( ( 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 = 1 )
;
a <= bthen
[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;
verum end; suppose
(
x = 1 &
y = 0 )
;
a <= bthen
[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;
verum end; suppose
(
x = 1 &
y = 2 )
;
a <= bthen
[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;
verum end; suppose
(
x = 2 &
y = 1 )
;
a <= bthen
[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;
verum end; suppose
(
x = 2 &
y = 3 )
;
a <= bthen
[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;
verum end; suppose
(
x = 3 &
y = 2 )
;
a <= bthen
[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;
verum end; end;
end; take
F
;
( F = f " & F is monotone )thus
F = f "
;
F is monotone thus
F is
monotone
verumproof
let x,
y be
Element of
(ComplRelStr (Necklace 4));
ORDERS_3:def 5 ( 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
;
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, Th17, 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
.=
Segm 4
by Th19
;
then
(
x in Segm 4 &
y in Segm 4 )
;
then
(
x is
natural &
y is
natural )
;
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 i <> j
assume A45:
(
i + 1
= j or
j + 1
= i )
;
contradiction
end;
thus
i <> j
by A38, A42, Def8;
verum
end;
A48:
((2,3) --> (0,2)) " = (
0,2)
--> (2,3)
by Th9;
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, Th6
.=
(((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 Th9;
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)) ")
;
contradiction
then consider x being
object 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;
verum
end;
A58:
F . 1 =
((((0,1) --> (1,3)) ") +* (((2,3) --> (0,2)) ")) . 1
by A22, A17, A18, A11, Th6
.=
(((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, Th6
.=
(((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, Th6
.=
(((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);
( not a = F . x or not b = F . y or a <= b )
assume that A63:
a = F . x
and A64:
b = F . y
;
a <= b
per cases
( ( 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;
end;
end; end; end;