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:67;
A2: rng (0 ,1 --> 1,3) = {1,3} by FUNCT_4:67;
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:18;
(rng (0 ,1 --> 1,3)) \/ (rng (2,3 --> 0 ,2)) = {1,3,0 ,2} by A2, A1, ENUMSET1:45
.= {0 ,1,2,3} by ENUMSET1:112 ;
then x in 4 by A4, A5, CARD_1:90;
then x in the carrier of (Necklace 4) by Th21;
hence x in the carrier of (ComplRelStr (Necklace 4)) by Def9; :: 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:65
.= {0 ,1} \/ {2,3} by FUNCT_4:65
.= {0 ,1,2,3} by ENUMSET1:45 ;
then A7: dom ((0 ,1 --> 1,3) +* (2,3 --> 0 ,2)) = the carrier of (Necklace 4) by Th21, CARD_1:90;
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:11;
take f ; :: according to WAYBEL_1:def 8 :: thesis: 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 ) ;
:: according to WAYBEL_0:def 38
case that 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:14;
then ( rng (1 .--> 3) = {3} & x = 1 ) by A9, FUNCOP_1:14, 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:14;
then ( rng (3 .--> 2) = {2} & x = 0 ) by A15, FUNCOP_1:14, 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:98;
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:39, PARTFUN1:138
.= {1,3,0 ,2} by A2, A1, ENUMSET1:45
.= {0 ,1,2,3} by ENUMSET1:112
.= the carrier of (Necklace 4) by Th21, CARD_1:90
.= the carrier of (ComplRelStr (Necklace 4)) by Def9 ;
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:98;
hence f is one-to-one by A17, A11, FUNCT_4:98; :: 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:31;
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:106;
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 Th20;
( ( 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, ZFMISC_1:33;
hence contradiction ; :: thesis: verum
end;
then A27: x9 in the InternalRel of (Necklace 4) ` by SUBSET_1:50;
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 Def9; :: 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:65;
then 2 in dom (2,3 --> 0 ,2) by TARSKI:def 2;
then A29: f . 2 = (2,3 --> 0 ,2) . 2 by FUNCT_4:14
.= 0 by FUNCT_4:66 ;
3 in dom (2,3 --> 0 ,2) by A28, TARSKI:def 2;
then A30: f . 3 = (2,3 --> 0 ,2) . 3 by FUNCT_4:14
.= 2 by FUNCT_4:66 ;
A31: dom (0 ,1 --> 1,3) = {0 ,1} by FUNCT_4:65;
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:17
.= 1 by FUNCT_4:66 ;
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:17
.= 3 by FUNCT_4:66 ;
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 9;
the carrier of (Necklace 4) = 4 by Th21;
then reconsider i = x, j = y as Nat by Th4;
A35: ( i = j + 1 or j = i + 1 ) by A34, Th25;
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
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 = 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 9; :: 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 9; :: 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 9; :: 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 9; :: 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 9; :: 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 9; :: 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 9;
then A37: [x,y] in (the InternalRel of (Necklace 4) ` ) \ (id the carrier of (Necklace 4)) by Def9;
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, Th19, 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 Def9
.= 4 by Th21 ;
then ( x is natural & y is natural ) by Th4;
then reconsider i = x, j = y as Element of NAT by ORDINAL1:def 13;
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
per cases ( i + 1 = j or j + 1 = i ) by A45;
end;
end;
thus i <> j by A38, A42, Def9; :: thesis: verum
end;
A48: (2,3 --> 0 ,2) " = 0 ,2 --> 2,3 by Th11;
then A49: dom ((2,3 --> 0 ,2) " ) = {0 ,2} by FUNCT_4:65;
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, Th8
.= ((2,3 --> 0 ,2) " ) . 0 by A50, FUNCT_4:14
.= 2 by A48, FUNCT_4:66 ;
A52: (0 ,1 --> 1,3) " = 1,3 --> 0 ,1 by Th11;
then A53: dom ((0 ,1 --> 1,3) " ) = {1,3} by FUNCT_4:65;
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, Th8
.= ((0 ,1 --> 1,3) " ) . 1 by A55, A54, FUNCT_4:17
.= 0 by A52, FUNCT_4:66 ;
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, Th8
.= ((2,3 --> 0 ,2) " ) . 2 by A59, FUNCT_4:14
.= 3 by A48, FUNCT_4:66 ;
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, Th8
.= ((0 ,1 --> 1,3) " ) . 3 by A55, A61, FUNCT_4:17
.= 1 by A52, FUNCT_4:66 ;
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
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:90, 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;
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;
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;
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;