let G be non empty irreflexive RelStr ; :: thesis: ( G embeds Necklace 4 iff ComplRelStr G embeds Necklace 4 )
set N4 = Necklace 4;
set CmpN4 = ComplRelStr (Necklace 4);
set CmpG = ComplRelStr G;
A1: the carrier of (ComplRelStr G) = the carrier of G by NECKLACE:def 8;
A2: the carrier of (Necklace 4) = {0,1,2,3} by NECKLACE:1, NECKLACE:20;
then A3: 0 in the carrier of (Necklace 4) by ENUMSET1:def 2;
A4: the carrier of (ComplRelStr (Necklace 4)) = the carrier of (Necklace 4) by NECKLACE:def 8;
thus ( G embeds Necklace 4 implies ComplRelStr G embeds Necklace 4 ) :: thesis: ( ComplRelStr G embeds Necklace 4 implies G embeds Necklace 4 )
proof
ComplRelStr (Necklace 4), Necklace 4 are_isomorphic by NECKLACE:29, WAYBEL_1:6;
then consider g being Function of (ComplRelStr (Necklace 4)),(Necklace 4) such that
A5: g is isomorphic by WAYBEL_1:def 8;
assume G embeds Necklace 4 ; :: thesis: ComplRelStr G embeds Necklace 4
then consider f being Function of (Necklace 4),G such that
A6: f is V24() and
A7: for x, y being Element of (Necklace 4) holds
( [x,y] in the InternalRel of (Necklace 4) iff [(f . x),(f . y)] in the InternalRel of G ) ;
reconsider h = f * g as Function of (ComplRelStr (Necklace 4)),G ;
A8: ( g is V24() & g is monotone ) by A5, WAYBEL_0:def 38;
A9: for x, y being Element of (ComplRelStr (Necklace 4)) holds
( [x,y] in the InternalRel of (ComplRelStr (Necklace 4)) iff [(h . x),(h . y)] in the InternalRel of G )
proof
let x, y be Element of (ComplRelStr (Necklace 4)); :: thesis: ( [x,y] in the InternalRel of (ComplRelStr (Necklace 4)) iff [(h . x),(h . y)] in the InternalRel of G )
thus ( [x,y] in the InternalRel of (ComplRelStr (Necklace 4)) implies [(h . x),(h . y)] in the InternalRel of G ) :: thesis: ( [(h . x),(h . y)] in the InternalRel of G implies [x,y] in the InternalRel of (ComplRelStr (Necklace 4)) )
proof
assume [x,y] in the InternalRel of (ComplRelStr (Necklace 4)) ; :: thesis: [(h . x),(h . y)] in the InternalRel of G
then x <= y by ORDERS_2:def 5;
then g . x <= g . y by A8, WAYBEL_1:def 2;
then [(g . x),(g . y)] in the InternalRel of (Necklace 4) by ORDERS_2:def 5;
then [(f . (g . x)),(f . (g . y))] in the InternalRel of G by A7;
then [((f * g) . x),(f . (g . y))] in the InternalRel of G by FUNCT_2:15;
hence [(h . x),(h . y)] in the InternalRel of G by FUNCT_2:15; :: thesis: verum
end;
assume [(h . x),(h . y)] in the InternalRel of G ; :: thesis: [x,y] in the InternalRel of (ComplRelStr (Necklace 4))
then [(f . (g . x)),(h . y)] in the InternalRel of G by FUNCT_2:15;
then [(f . (g . x)),(f . (g . y))] in the InternalRel of G by FUNCT_2:15;
then [(g . x),(g . y)] in the InternalRel of (Necklace 4) by A7;
then g . x <= g . y by ORDERS_2:def 5;
then x <= y by A5, WAYBEL_0:66;
hence [x,y] in the InternalRel of (ComplRelStr (Necklace 4)) by ORDERS_2:def 5; :: thesis: verum
end;
A10: 0 in the carrier of (ComplRelStr (Necklace 4)) by A2, A4, ENUMSET1:def 2;
A11: 1 in the carrier of (ComplRelStr (Necklace 4)) by A2, A4, ENUMSET1:def 2;
A12: dom h = the carrier of (ComplRelStr (Necklace 4)) by FUNCT_2:def 1;
A13: [(h . 0),(h . 1)] in the InternalRel of (ComplRelStr G)
proof
assume A14: not [(h . 0),(h . 1)] in the InternalRel of (ComplRelStr G) ; :: thesis: contradiction
[(h . 0),(h . 1)] in the InternalRel of G
proof
( h . 0 in the carrier of G & h . 1 in the carrier of G ) by A10, A11, FUNCT_2:5;
then [(h . 0),(h . 1)] in [: the carrier of G, the carrier of G:] by ZFMISC_1:87;
then [(h . 0),(h . 1)] in ((id the carrier of G) \/ the InternalRel of G) \/ the InternalRel of (ComplRelStr G) by Th14;
then A15: ( [(h . 0),(h . 1)] in (id the carrier of G) \/ the InternalRel of G or [(h . 0),(h . 1)] in the InternalRel of (ComplRelStr G) ) by XBOOLE_0:def 3;
assume not [(h . 0),(h . 1)] in the InternalRel of G ; :: thesis: contradiction
then [(h . 0),(h . 1)] in id the carrier of G by A14, A15, XBOOLE_0:def 3;
then h . 0 = h . 1 by RELAT_1:def 10;
hence contradiction by A6, A8, A12, A10, A11, FUNCT_1:def 4; :: thesis: verum
end;
then A16: [0,1] in the InternalRel of (ComplRelStr (Necklace 4)) by A9, A10, A11;
[0,1] in the InternalRel of (Necklace 4) by ENUMSET1:def 4, NECKLA_2:2;
then [0,1] in the InternalRel of (Necklace 4) /\ the InternalRel of (ComplRelStr (Necklace 4)) by A16, XBOOLE_0:def 4;
then the InternalRel of (Necklace 4) meets the InternalRel of (ComplRelStr (Necklace 4)) ;
hence contradiction by Th12; :: thesis: verum
end;
A17: 2 in the carrier of (ComplRelStr (Necklace 4)) by A2, A4, ENUMSET1:def 2;
A18: [(h . 1),(h . 2)] in the InternalRel of (ComplRelStr G)
proof
assume A19: not [(h . 1),(h . 2)] in the InternalRel of (ComplRelStr G) ; :: thesis: contradiction
[(h . 1),(h . 2)] in the InternalRel of G
proof
( h . 1 in the carrier of G & h . 2 in the carrier of G ) by A11, A17, FUNCT_2:5;
then [(h . 1),(h . 2)] in [: the carrier of G, the carrier of G:] by ZFMISC_1:87;
then [(h . 1),(h . 2)] in ((id the carrier of G) \/ the InternalRel of G) \/ the InternalRel of (ComplRelStr G) by Th14;
then A20: ( [(h . 1),(h . 2)] in (id the carrier of G) \/ the InternalRel of G or [(h . 1),(h . 2)] in the InternalRel of (ComplRelStr G) ) by XBOOLE_0:def 3;
assume not [(h . 1),(h . 2)] in the InternalRel of G ; :: thesis: contradiction
then [(h . 1),(h . 2)] in id the carrier of G by A19, A20, XBOOLE_0:def 3;
then h . 1 = h . 2 by RELAT_1:def 10;
hence contradiction by A6, A8, A12, A11, A17, FUNCT_1:def 4; :: thesis: verum
end;
then A21: [1,2] in the InternalRel of (ComplRelStr (Necklace 4)) by A9, A11, A17;
[1,2] in the InternalRel of (Necklace 4) by ENUMSET1:def 4, NECKLA_2:2;
then [1,2] in the InternalRel of (Necklace 4) /\ the InternalRel of (ComplRelStr (Necklace 4)) by A21, XBOOLE_0:def 4;
then the InternalRel of (Necklace 4) meets the InternalRel of (ComplRelStr (Necklace 4)) ;
hence contradiction by Th12; :: thesis: verum
end;
A22: 3 in the carrier of (ComplRelStr (Necklace 4)) by A2, A4, ENUMSET1:def 2;
A23: [(h . 2),(h . 3)] in the InternalRel of (ComplRelStr G)
proof
assume A24: not [(h . 2),(h . 3)] in the InternalRel of (ComplRelStr G) ; :: thesis: contradiction
[(h . 2),(h . 3)] in the InternalRel of G
proof
( h . 2 in the carrier of G & h . 3 in the carrier of G ) by A17, A22, FUNCT_2:5;
then [(h . 2),(h . 3)] in [: the carrier of G, the carrier of G:] by ZFMISC_1:87;
then [(h . 2),(h . 3)] in ((id the carrier of G) \/ the InternalRel of G) \/ the InternalRel of (ComplRelStr G) by Th14;
then A25: ( [(h . 2),(h . 3)] in (id the carrier of G) \/ the InternalRel of G or [(h . 2),(h . 3)] in the InternalRel of (ComplRelStr G) ) by XBOOLE_0:def 3;
assume not [(h . 2),(h . 3)] in the InternalRel of G ; :: thesis: contradiction
then [(h . 2),(h . 3)] in id the carrier of G by A24, A25, XBOOLE_0:def 3;
then h . 2 = h . 3 by RELAT_1:def 10;
hence contradiction by A6, A8, A12, A17, A22, FUNCT_1:def 4; :: thesis: verum
end;
then A26: [2,3] in the InternalRel of (ComplRelStr (Necklace 4)) by A9, A17, A22;
[2,3] in the InternalRel of (Necklace 4) by ENUMSET1:def 4, NECKLA_2:2;
then [2,3] in the InternalRel of (Necklace 4) /\ the InternalRel of (ComplRelStr (Necklace 4)) by A26, XBOOLE_0:def 4;
then the InternalRel of (Necklace 4) meets the InternalRel of (ComplRelStr (Necklace 4)) ;
hence contradiction by Th12; :: thesis: verum
end;
[3,1] in the InternalRel of (ComplRelStr (Necklace 4)) by Th11, ENUMSET1:def 4;
then A27: [(h . 3),(h . 1)] in the InternalRel of G by A9, A11, A22;
[1,3] in the InternalRel of (ComplRelStr (Necklace 4)) by Th11, ENUMSET1:def 4;
then A28: [(h . 1),(h . 3)] in the InternalRel of G by A9, A11, A22;
[3,0] in the InternalRel of (ComplRelStr (Necklace 4)) by Th11, ENUMSET1:def 4;
then A29: [(h . 3),(h . 0)] in the InternalRel of G by A9, A10, A22;
[0,3] in the InternalRel of (ComplRelStr (Necklace 4)) by Th11, ENUMSET1:def 4;
then A30: [(h . 0),(h . 3)] in the InternalRel of G by A9, A10, A22;
A31: [(h . 1),(h . 0)] in the InternalRel of (ComplRelStr G)
proof
assume A32: not [(h . 1),(h . 0)] in the InternalRel of (ComplRelStr G) ; :: thesis: contradiction
[(h . 1),(h . 0)] in the InternalRel of G
proof
( h . 0 in the carrier of G & h . 1 in the carrier of G ) by A10, A11, FUNCT_2:5;
then [(h . 1),(h . 0)] in [: the carrier of G, the carrier of G:] by ZFMISC_1:87;
then [(h . 1),(h . 0)] in ((id the carrier of G) \/ the InternalRel of G) \/ the InternalRel of (ComplRelStr G) by Th14;
then A33: ( [(h . 1),(h . 0)] in (id the carrier of G) \/ the InternalRel of G or [(h . 1),(h . 0)] in the InternalRel of (ComplRelStr G) ) by XBOOLE_0:def 3;
assume not [(h . 1),(h . 0)] in the InternalRel of G ; :: thesis: contradiction
then [(h . 1),(h . 0)] in id the carrier of G by A32, A33, XBOOLE_0:def 3;
then h . 0 = h . 1 by RELAT_1:def 10;
hence contradiction by A6, A8, A12, A10, A11, FUNCT_1:def 4; :: thesis: verum
end;
then A34: [1,0] in the InternalRel of (ComplRelStr (Necklace 4)) by A9, A10, A11;
[1,0] in the InternalRel of (Necklace 4) by ENUMSET1:def 4, NECKLA_2:2;
then [1,0] in the InternalRel of (Necklace 4) /\ the InternalRel of (ComplRelStr (Necklace 4)) by A34, XBOOLE_0:def 4;
then the InternalRel of (Necklace 4) meets the InternalRel of (ComplRelStr (Necklace 4)) ;
hence contradiction by Th12; :: thesis: verum
end;
A35: [(h . 2),(h . 1)] in the InternalRel of (ComplRelStr G)
proof
assume A36: not [(h . 2),(h . 1)] in the InternalRel of (ComplRelStr G) ; :: thesis: contradiction
[(h . 2),(h . 1)] in the InternalRel of G
proof
( h . 1 in the carrier of G & h . 2 in the carrier of G ) by A11, A17, FUNCT_2:5;
then [(h . 2),(h . 1)] in [: the carrier of G, the carrier of G:] by ZFMISC_1:87;
then [(h . 2),(h . 1)] in ((id the carrier of G) \/ the InternalRel of G) \/ the InternalRel of (ComplRelStr G) by Th14;
then A37: ( [(h . 2),(h . 1)] in (id the carrier of G) \/ the InternalRel of G or [(h . 2),(h . 1)] in the InternalRel of (ComplRelStr G) ) by XBOOLE_0:def 3;
assume not [(h . 2),(h . 1)] in the InternalRel of G ; :: thesis: contradiction
then [(h . 2),(h . 1)] in id the carrier of G by A36, A37, XBOOLE_0:def 3;
then h . 1 = h . 2 by RELAT_1:def 10;
hence contradiction by A6, A8, A12, A11, A17, FUNCT_1:def 4; :: thesis: verum
end;
then A38: [2,1] in the InternalRel of (ComplRelStr (Necklace 4)) by A9, A11, A17;
[2,1] in the InternalRel of (Necklace 4) by ENUMSET1:def 4, NECKLA_2:2;
then [2,1] in the InternalRel of (Necklace 4) /\ the InternalRel of (ComplRelStr (Necklace 4)) by A38, XBOOLE_0:def 4;
then the InternalRel of (Necklace 4) meets the InternalRel of (ComplRelStr (Necklace 4)) ;
hence contradiction by Th12; :: thesis: verum
end;
A39: [(h . 3),(h . 2)] in the InternalRel of (ComplRelStr G)
proof
assume A40: not [(h . 3),(h . 2)] in the InternalRel of (ComplRelStr G) ; :: thesis: contradiction
[(h . 3),(h . 2)] in the InternalRel of G
proof
( h . 2 in the carrier of G & h . 3 in the carrier of G ) by A17, A22, FUNCT_2:5;
then [(h . 3),(h . 2)] in [: the carrier of G, the carrier of G:] by ZFMISC_1:87;
then [(h . 3),(h . 2)] in ((id the carrier of G) \/ the InternalRel of G) \/ the InternalRel of (ComplRelStr G) by Th14;
then A41: ( [(h . 3),(h . 2)] in (id the carrier of G) \/ the InternalRel of G or [(h . 3),(h . 2)] in the InternalRel of (ComplRelStr G) ) by XBOOLE_0:def 3;
assume not [(h . 3),(h . 2)] in the InternalRel of G ; :: thesis: contradiction
then [(h . 3),(h . 2)] in id the carrier of G by A40, A41, XBOOLE_0:def 3;
then h . 2 = h . 3 by RELAT_1:def 10;
hence contradiction by A6, A8, A12, A17, A22, FUNCT_1:def 4; :: thesis: verum
end;
then A42: [3,2] in the InternalRel of (ComplRelStr (Necklace 4)) by A9, A17, A22;
[3,2] in the InternalRel of (Necklace 4) by ENUMSET1:def 4, NECKLA_2:2;
then [3,2] in the InternalRel of (Necklace 4) /\ the InternalRel of (ComplRelStr (Necklace 4)) by A42, XBOOLE_0:def 4;
then the InternalRel of (Necklace 4) meets the InternalRel of (ComplRelStr (Necklace 4)) ;
hence contradiction by Th12; :: thesis: verum
end;
[2,0] in the InternalRel of (ComplRelStr (Necklace 4)) by Th11, ENUMSET1:def 4;
then A43: [(h . 2),(h . 0)] in the InternalRel of G by A9, A10, A17;
[0,2] in the InternalRel of (ComplRelStr (Necklace 4)) by Th11, ENUMSET1:def 4;
then A44: [(h . 0),(h . 2)] in the InternalRel of G by A9, A10, A17;
for x, y being Element of (Necklace 4) holds
( [x,y] in the InternalRel of (Necklace 4) iff [(h . x),(h . y)] in the InternalRel of (ComplRelStr G) )
proof
let x, y be Element of (Necklace 4); :: thesis: ( [x,y] in the InternalRel of (Necklace 4) iff [(h . x),(h . y)] in the InternalRel of (ComplRelStr G) )
thus ( [x,y] in the InternalRel of (Necklace 4) implies [(h . x),(h . y)] in the InternalRel of (ComplRelStr G) ) :: thesis: ( [(h . x),(h . y)] in the InternalRel of (ComplRelStr G) implies [x,y] in the InternalRel of (Necklace 4) )
proof
assume A45: [x,y] in the InternalRel of (Necklace 4) ; :: thesis: [(h . x),(h . y)] in the InternalRel of (ComplRelStr G)
per cases ( [x,y] = [0,1] or [x,y] = [1,0] or [x,y] = [1,2] or [x,y] = [2,1] or [x,y] = [2,3] or [x,y] = [3,2] ) by A45, ENUMSET1:def 4, NECKLA_2:2;
suppose A46: [x,y] = [0,1] ; :: thesis: [(h . x),(h . y)] in the InternalRel of (ComplRelStr G)
then x = 0 by XTUPLE_0:1;
hence [(h . x),(h . y)] in the InternalRel of (ComplRelStr G) by A13, A46, XTUPLE_0:1; :: thesis: verum
end;
suppose A47: [x,y] = [1,0] ; :: thesis: [(h . x),(h . y)] in the InternalRel of (ComplRelStr G)
then x = 1 by XTUPLE_0:1;
hence [(h . x),(h . y)] in the InternalRel of (ComplRelStr G) by A31, A47, XTUPLE_0:1; :: thesis: verum
end;
suppose A48: [x,y] = [1,2] ; :: thesis: [(h . x),(h . y)] in the InternalRel of (ComplRelStr G)
then x = 1 by XTUPLE_0:1;
hence [(h . x),(h . y)] in the InternalRel of (ComplRelStr G) by A18, A48, XTUPLE_0:1; :: thesis: verum
end;
suppose A49: [x,y] = [2,1] ; :: thesis: [(h . x),(h . y)] in the InternalRel of (ComplRelStr G)
then x = 2 by XTUPLE_0:1;
hence [(h . x),(h . y)] in the InternalRel of (ComplRelStr G) by A35, A49, XTUPLE_0:1; :: thesis: verum
end;
suppose A50: [x,y] = [2,3] ; :: thesis: [(h . x),(h . y)] in the InternalRel of (ComplRelStr G)
then x = 2 by XTUPLE_0:1;
hence [(h . x),(h . y)] in the InternalRel of (ComplRelStr G) by A23, A50, XTUPLE_0:1; :: thesis: verum
end;
suppose A51: [x,y] = [3,2] ; :: thesis: [(h . x),(h . y)] in the InternalRel of (ComplRelStr G)
then x = 3 by XTUPLE_0:1;
hence [(h . x),(h . y)] in the InternalRel of (ComplRelStr G) by A39, A51, XTUPLE_0:1; :: thesis: verum
end;
end;
end;
assume A52: [(h . x),(h . y)] in the InternalRel of (ComplRelStr G) ; :: thesis: [x,y] in the InternalRel of (Necklace 4)
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 A2, ENUMSET1:def 2;
suppose ( x = 1 & y = 3 ) ; :: thesis: [x,y] in the InternalRel of (Necklace 4)
then [(h . 1),(h . 3)] in the InternalRel of G /\ the InternalRel of (ComplRelStr G) by A28, A52, XBOOLE_0:def 4;
then the InternalRel of G meets the InternalRel of (ComplRelStr G) ;
hence [x,y] in the InternalRel of (Necklace 4) by Th12; :: thesis: verum
end;
suppose ( x = 3 & y = 1 ) ; :: thesis: [x,y] in the InternalRel of (Necklace 4)
then [(h . 3),(h . 1)] in the InternalRel of G /\ the InternalRel of (ComplRelStr G) by A27, A52, XBOOLE_0:def 4;
then the InternalRel of G meets the InternalRel of (ComplRelStr G) ;
hence [x,y] in the InternalRel of (Necklace 4) by Th12; :: thesis: verum
end;
end;
end;
hence ComplRelStr G embeds Necklace 4 by A4, A1, A6, A8; :: thesis: verum
end;
assume ComplRelStr G embeds Necklace 4 ; :: thesis: G embeds Necklace 4
then consider f being Function of (Necklace 4),(ComplRelStr G) such that
A57: f is V24() and
A58: for x, y being Element of (Necklace 4) holds
( [x,y] in the InternalRel of (Necklace 4) iff [(f . x),(f . y)] in the InternalRel of (ComplRelStr G) ) ;
consider g being Function of (Necklace 4),(ComplRelStr (Necklace 4)) such that
A59: g is isomorphic by NECKLACE:29, WAYBEL_1:def 8;
A60: 2 in the carrier of (Necklace 4) by A2, ENUMSET1:def 2;
A61: dom f = the carrier of (Necklace 4) by FUNCT_2:def 1;
A62: [(f . 0),(f . 2)] in the InternalRel of G
proof
assume A63: not [(f . 0),(f . 2)] in the InternalRel of G ; :: thesis: contradiction
[(f . 0),(f . 2)] in the InternalRel of (ComplRelStr G)
proof
( f . 0 in the carrier of (ComplRelStr G) & f . 2 in the carrier of (ComplRelStr G) ) by A3, A60, FUNCT_2:5;
then [(f . 0),(f . 2)] in [: the carrier of G, the carrier of G:] by A1, ZFMISC_1:87;
then [(f . 0),(f . 2)] in ((id the carrier of G) \/ the InternalRel of G) \/ the InternalRel of (ComplRelStr G) by Th14;
then A64: ( [(f . 0),(f . 2)] in (id the carrier of G) \/ the InternalRel of G or [(f . 0),(f . 2)] in the InternalRel of (ComplRelStr G) ) by XBOOLE_0:def 3;
assume not [(f . 0),(f . 2)] in the InternalRel of (ComplRelStr G) ; :: thesis: contradiction
then [(f . 0),(f . 2)] in id the carrier of G by A63, A64, XBOOLE_0:def 3;
then f . 0 = f . 2 by RELAT_1:def 10;
hence contradiction by A57, A61, A3, A60, FUNCT_1:def 4; :: thesis: verum
end;
then A65: [0,2] in the InternalRel of (Necklace 4) by A58, A3, A60;
[0,2] in the InternalRel of (ComplRelStr (Necklace 4)) by Th11, ENUMSET1:def 4;
then [0,2] in the InternalRel of (Necklace 4) /\ the InternalRel of (ComplRelStr (Necklace 4)) by A65, XBOOLE_0:def 4;
then the InternalRel of (Necklace 4) meets the InternalRel of (ComplRelStr (Necklace 4)) ;
hence contradiction by Th12; :: thesis: verum
end;
A66: 3 in the carrier of (Necklace 4) by A2, ENUMSET1:def 2;
A67: [(f . 0),(f . 3)] in the InternalRel of G
proof
assume A68: not [(f . 0),(f . 3)] in the InternalRel of G ; :: thesis: contradiction
[(f . 0),(f . 3)] in the InternalRel of (ComplRelStr G)
proof
( f . 0 in the carrier of (ComplRelStr G) & f . 3 in the carrier of (ComplRelStr G) ) by A3, A66, FUNCT_2:5;
then [(f . 0),(f . 3)] in [: the carrier of G, the carrier of G:] by A1, ZFMISC_1:87;
then [(f . 0),(f . 3)] in ((id the carrier of G) \/ the InternalRel of G) \/ the InternalRel of (ComplRelStr G) by Th14;
then A69: ( [(f . 0),(f . 3)] in (id the carrier of G) \/ the InternalRel of G or [(f . 0),(f . 3)] in the InternalRel of (ComplRelStr G) ) by XBOOLE_0:def 3;
assume not [(f . 0),(f . 3)] in the InternalRel of (ComplRelStr G) ; :: thesis: contradiction
then [(f . 0),(f . 3)] in id the carrier of G by A68, A69, XBOOLE_0:def 3;
then f . 0 = f . 3 by RELAT_1:def 10;
hence contradiction by A57, A61, A3, A66, FUNCT_1:def 4; :: thesis: verum
end;
then A70: [0,3] in the InternalRel of (Necklace 4) by A58, A3, A66;
[0,3] in the InternalRel of (ComplRelStr (Necklace 4)) by Th11, ENUMSET1:def 4;
then [0,3] in the InternalRel of (Necklace 4) /\ the InternalRel of (ComplRelStr (Necklace 4)) by A70, XBOOLE_0:def 4;
then the InternalRel of (Necklace 4) meets the InternalRel of (ComplRelStr (Necklace 4)) ;
hence contradiction by Th12; :: thesis: verum
end;
A71: 1 in the carrier of (Necklace 4) by A2, ENUMSET1:def 2;
A72: [(f . 1),(f . 3)] in the InternalRel of G
proof
assume A73: not [(f . 1),(f . 3)] in the InternalRel of G ; :: thesis: contradiction
[(f . 1),(f . 3)] in the InternalRel of (ComplRelStr G)
proof
( f . 1 in the carrier of (ComplRelStr G) & f . 3 in the carrier of (ComplRelStr G) ) by A71, A66, FUNCT_2:5;
then [(f . 1),(f . 3)] in [: the carrier of G, the carrier of G:] by A1, ZFMISC_1:87;
then [(f . 1),(f . 3)] in ((id the carrier of G) \/ the InternalRel of G) \/ the InternalRel of (ComplRelStr G) by Th14;
then A74: ( [(f . 1),(f . 3)] in (id the carrier of G) \/ the InternalRel of G or [(f . 1),(f . 3)] in the InternalRel of (ComplRelStr G) ) by XBOOLE_0:def 3;
assume not [(f . 1),(f . 3)] in the InternalRel of (ComplRelStr G) ; :: thesis: contradiction
then [(f . 1),(f . 3)] in id the carrier of G by A73, A74, XBOOLE_0:def 3;
then f . 1 = f . 3 by RELAT_1:def 10;
hence contradiction by A57, A61, A71, A66, FUNCT_1:def 4; :: thesis: verum
end;
then A75: [1,3] in the InternalRel of (Necklace 4) by A58, A71, A66;
[1,3] in the InternalRel of (ComplRelStr (Necklace 4)) by Th11, ENUMSET1:def 4;
then [1,3] in the InternalRel of (Necklace 4) /\ the InternalRel of (ComplRelStr (Necklace 4)) by A75, XBOOLE_0:def 4;
then the InternalRel of (Necklace 4) meets the InternalRel of (ComplRelStr (Necklace 4)) ;
hence contradiction by Th12; :: thesis: verum
end;
[3,2] in the InternalRel of (Necklace 4) by ENUMSET1:def 4, NECKLA_2:2;
then A76: [(f . 3),(f . 2)] in the InternalRel of (ComplRelStr G) by A58, A60, A66;
[2,3] in the InternalRel of (Necklace 4) by ENUMSET1:def 4, NECKLA_2:2;
then A77: [(f . 2),(f . 3)] in the InternalRel of (ComplRelStr G) by A58, A60, A66;
[1,2] in the InternalRel of (Necklace 4) by ENUMSET1:def 4, NECKLA_2:2;
then A78: [(f . 1),(f . 2)] in the InternalRel of (ComplRelStr G) by A58, A71, A60;
[1,0] in the InternalRel of (Necklace 4) by ENUMSET1:def 4, NECKLA_2:2;
then A79: [(f . 1),(f . 0)] in the InternalRel of (ComplRelStr G) by A58, A3, A71;
A80: [(f . 2),(f . 0)] in the InternalRel of G
proof
assume A81: not [(f . 2),(f . 0)] in the InternalRel of G ; :: thesis: contradiction
[(f . 2),(f . 0)] in the InternalRel of (ComplRelStr G)
proof
( f . 0 in the carrier of (ComplRelStr G) & f . 2 in the carrier of (ComplRelStr G) ) by A3, A60, FUNCT_2:5;
then [(f . 2),(f . 0)] in [: the carrier of G, the carrier of G:] by A1, ZFMISC_1:87;
then [(f . 2),(f . 0)] in ((id the carrier of G) \/ the InternalRel of G) \/ the InternalRel of (ComplRelStr G) by Th14;
then A82: ( [(f . 2),(f . 0)] in (id the carrier of G) \/ the InternalRel of G or [(f . 2),(f . 0)] in the InternalRel of (ComplRelStr G) ) by XBOOLE_0:def 3;
assume not [(f . 2),(f . 0)] in the InternalRel of (ComplRelStr G) ; :: thesis: contradiction
then [(f . 2),(f . 0)] in id the carrier of G by A81, A82, XBOOLE_0:def 3;
then f . 0 = f . 2 by RELAT_1:def 10;
hence contradiction by A57, A61, A3, A60, FUNCT_1:def 4; :: thesis: verum
end;
then A83: [2,0] in the InternalRel of (Necklace 4) by A58, A3, A60;
[2,0] in the InternalRel of (ComplRelStr (Necklace 4)) by Th11, ENUMSET1:def 4;
then [2,0] in the InternalRel of (Necklace 4) /\ the InternalRel of (ComplRelStr (Necklace 4)) by A83, XBOOLE_0:def 4;
then the InternalRel of (Necklace 4) meets the InternalRel of (ComplRelStr (Necklace 4)) ;
hence contradiction by Th12; :: thesis: verum
end;
A84: [(f . 3),(f . 0)] in the InternalRel of G
proof
assume A85: not [(f . 3),(f . 0)] in the InternalRel of G ; :: thesis: contradiction
[(f . 3),(f . 0)] in the InternalRel of (ComplRelStr G)
proof
( f . 0 in the carrier of (ComplRelStr G) & f . 3 in the carrier of (ComplRelStr G) ) by A3, A66, FUNCT_2:5;
then [(f . 3),(f . 0)] in [: the carrier of G, the carrier of G:] by A1, ZFMISC_1:87;
then [(f . 3),(f . 0)] in ((id the carrier of G) \/ the InternalRel of G) \/ the InternalRel of (ComplRelStr G) by Th14;
then A86: ( [(f . 3),(f . 0)] in (id the carrier of G) \/ the InternalRel of G or [(f . 3),(f . 0)] in the InternalRel of (ComplRelStr G) ) by XBOOLE_0:def 3;
assume not [(f . 3),(f . 0)] in the InternalRel of (ComplRelStr G) ; :: thesis: contradiction
then [(f . 3),(f . 0)] in id the carrier of G by A85, A86, XBOOLE_0:def 3;
then f . 0 = f . 3 by RELAT_1:def 10;
hence contradiction by A57, A61, A3, A66, FUNCT_1:def 4; :: thesis: verum
end;
then A87: [3,0] in the InternalRel of (Necklace 4) by A58, A3, A66;
[3,0] in the InternalRel of (ComplRelStr (Necklace 4)) by Th11, ENUMSET1:def 4;
then [3,0] in the InternalRel of (Necklace 4) /\ the InternalRel of (ComplRelStr (Necklace 4)) by A87, XBOOLE_0:def 4;
then the InternalRel of (Necklace 4) meets the InternalRel of (ComplRelStr (Necklace 4)) ;
hence contradiction by Th12; :: thesis: verum
end;
A88: [(f . 3),(f . 1)] in the InternalRel of G
proof
assume A89: not [(f . 3),(f . 1)] in the InternalRel of G ; :: thesis: contradiction
[(f . 3),(f . 1)] in the InternalRel of (ComplRelStr G)
proof
( f . 1 in the carrier of (ComplRelStr G) & f . 3 in the carrier of (ComplRelStr G) ) by A71, A66, FUNCT_2:5;
then [(f . 3),(f . 1)] in [: the carrier of G, the carrier of G:] by A1, ZFMISC_1:87;
then [(f . 3),(f . 1)] in ((id the carrier of G) \/ the InternalRel of G) \/ the InternalRel of (ComplRelStr G) by Th14;
then A90: ( [(f . 3),(f . 1)] in (id the carrier of G) \/ the InternalRel of G or [(f . 3),(f . 1)] in the InternalRel of (ComplRelStr G) ) by XBOOLE_0:def 3;
assume not [(f . 3),(f . 1)] in the InternalRel of (ComplRelStr G) ; :: thesis: contradiction
then [(f . 3),(f . 1)] in id the carrier of G by A89, A90, XBOOLE_0:def 3;
then f . 1 = f . 3 by RELAT_1:def 10;
hence contradiction by A57, A61, A71, A66, FUNCT_1:def 4; :: thesis: verum
end;
then A91: [3,1] in the InternalRel of (Necklace 4) by A58, A71, A66;
[3,1] in the InternalRel of (ComplRelStr (Necklace 4)) by Th11, ENUMSET1:def 4;
then [3,1] in the InternalRel of (Necklace 4) /\ the InternalRel of (ComplRelStr (Necklace 4)) by A91, XBOOLE_0:def 4;
then the InternalRel of (Necklace 4) meets the InternalRel of (ComplRelStr (Necklace 4)) ;
hence contradiction by Th12; :: thesis: verum
end;
[2,1] in the InternalRel of (Necklace 4) by ENUMSET1:def 4, NECKLA_2:2;
then A92: [(f . 2),(f . 1)] in the InternalRel of (ComplRelStr G) by A58, A71, A60;
[0,1] in the InternalRel of (Necklace 4) by ENUMSET1:def 4, NECKLA_2:2;
then A93: [(f . 0),(f . 1)] in the InternalRel of (ComplRelStr G) by A58, A3, A71;
A94: for x, y being Element of (ComplRelStr (Necklace 4)) holds
( [x,y] in the InternalRel of (ComplRelStr (Necklace 4)) iff [(f . x),(f . y)] in the InternalRel of G )
proof
let x, y be Element of (ComplRelStr (Necklace 4)); :: thesis: ( [x,y] in the InternalRel of (ComplRelStr (Necklace 4)) iff [(f . x),(f . y)] in the InternalRel of G )
A95: the carrier of (Necklace 4) = the carrier of (ComplRelStr (Necklace 4)) by NECKLACE:def 8;
thus ( [x,y] in the InternalRel of (ComplRelStr (Necklace 4)) implies [(f . x),(f . y)] in the InternalRel of G ) :: thesis: ( [(f . x),(f . y)] in the InternalRel of G implies [x,y] in the InternalRel of (ComplRelStr (Necklace 4)) )
proof
assume A96: [x,y] in the InternalRel of (ComplRelStr (Necklace 4)) ; :: thesis: [(f . x),(f . y)] in the InternalRel of G
per cases ( [x,y] = [0,2] or [x,y] = [2,0] or [x,y] = [0,3] or [x,y] = [3,0] or [x,y] = [1,3] or [x,y] = [3,1] ) by A96, Th11, ENUMSET1:def 4;
suppose A97: [x,y] = [0,2] ; :: thesis: [(f . x),(f . y)] in the InternalRel of G
then x = 0 by XTUPLE_0:1;
hence [(f . x),(f . y)] in the InternalRel of G by A62, A97, XTUPLE_0:1; :: thesis: verum
end;
suppose A98: [x,y] = [2,0] ; :: thesis: [(f . x),(f . y)] in the InternalRel of G
then x = 2 by XTUPLE_0:1;
hence [(f . x),(f . y)] in the InternalRel of G by A80, A98, XTUPLE_0:1; :: thesis: verum
end;
suppose A99: [x,y] = [0,3] ; :: thesis: [(f . x),(f . y)] in the InternalRel of G
then x = 0 by XTUPLE_0:1;
hence [(f . x),(f . y)] in the InternalRel of G by A67, A99, XTUPLE_0:1; :: thesis: verum
end;
suppose A100: [x,y] = [3,0] ; :: thesis: [(f . x),(f . y)] in the InternalRel of G
then x = 3 by XTUPLE_0:1;
hence [(f . x),(f . y)] in the InternalRel of G by A84, A100, XTUPLE_0:1; :: thesis: verum
end;
suppose A101: [x,y] = [1,3] ; :: thesis: [(f . x),(f . y)] in the InternalRel of G
then x = 1 by XTUPLE_0:1;
hence [(f . x),(f . y)] in the InternalRel of G by A72, A101, XTUPLE_0:1; :: thesis: verum
end;
suppose A102: [x,y] = [3,1] ; :: thesis: [(f . x),(f . y)] in the InternalRel of G
then x = 3 by XTUPLE_0:1;
hence [(f . x),(f . y)] in the InternalRel of G by A88, A102, XTUPLE_0:1; :: thesis: verum
end;
end;
end;
assume A103: [(f . x),(f . y)] in the InternalRel of G ; :: thesis: [x,y] in the InternalRel of (ComplRelStr (Necklace 4))
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 = 2 & y = 0 ) or ( x = 3 & y = 0 ) or ( x = 1 & y = 1 ) or ( x = 1 & y = 2 ) or ( x = 1 & y = 3 ) or ( x = 2 & y = 1 ) or ( x = 2 & y = 2 ) or ( x = 2 & y = 3 ) or ( x = 3 & y = 1 ) or ( x = 3 & y = 2 ) or ( x = 3 & y = 3 ) ) by A2, A95, ENUMSET1:def 2;
end;
end;
reconsider f = f as Function of (ComplRelStr (Necklace 4)),G by A4, NECKLACE:def 8;
reconsider h = f * g as Function of (Necklace 4),G ;
A108: ( g is V24() & g is monotone ) by A59, WAYBEL_0:def 38;
for x, y being Element of (Necklace 4) holds
( [x,y] in the InternalRel of (Necklace 4) iff [(h . x),(h . y)] in the InternalRel of G )
proof
let x, y be Element of (Necklace 4); :: thesis: ( [x,y] in the InternalRel of (Necklace 4) iff [(h . x),(h . y)] in the InternalRel of G )
thus ( [x,y] in the InternalRel of (Necklace 4) implies [(h . x),(h . y)] in the InternalRel of G ) :: thesis: ( [(h . x),(h . y)] in the InternalRel of G implies [x,y] in the InternalRel of (Necklace 4) )
proof
assume [x,y] in the InternalRel of (Necklace 4) ; :: thesis: [(h . x),(h . y)] in the InternalRel of G
then x <= y by ORDERS_2:def 5;
then g . x <= g . y by A108, WAYBEL_1:def 2;
then [(g . x),(g . y)] in the InternalRel of (ComplRelStr (Necklace 4)) by ORDERS_2:def 5;
then [(f . (g . x)),(f . (g . y))] in the InternalRel of G by A94;
then [((f * g) . x),(f . (g . y))] in the InternalRel of G by FUNCT_2:15;
hence [(h . x),(h . y)] in the InternalRel of G by FUNCT_2:15; :: thesis: verum
end;
assume [(h . x),(h . y)] in the InternalRel of G ; :: thesis: [x,y] in the InternalRel of (Necklace 4)
then [(f . (g . x)),(h . y)] in the InternalRel of G by FUNCT_2:15;
then [(f . (g . x)),(f . (g . y))] in the InternalRel of G by FUNCT_2:15;
then [(g . x),(g . y)] in the InternalRel of (ComplRelStr (Necklace 4)) by A94;
then g . x <= g . y by ORDERS_2:def 5;
then x <= y by A59, WAYBEL_0:66;
hence [x,y] in the InternalRel of (Necklace 4) by ORDERS_2:def 5; :: thesis: verum
end;
hence G embeds Necklace 4 by A57, A108; :: thesis: verum