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 (Necklace 4) = {0 ,1,2,3} by NECKLACE:2, NECKLACE:21;
A2: the carrier of (ComplRelStr (Necklace 4)) = the carrier of (Necklace 4) by NECKLACE:def 9;
A3: the carrier of (ComplRelStr G) = the carrier of G by NECKLACE:def 9;
thus ( G embeds Necklace 4 implies ComplRelStr G embeds Necklace 4 ) :: thesis: ( ComplRelStr G embeds Necklace 4 implies G embeds Necklace 4 )
proof
assume G embeds Necklace 4 ; :: thesis: ComplRelStr G embeds Necklace 4
then consider f being Function of (Necklace 4),G such that
A4: ( f is one-to-one & ( 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 ) ) ) by NECKLACE:def 2;
ComplRelStr (Necklace 4), Necklace 4 are_isomorphic by NECKLACE:30, WAYBEL_1:7;
then consider g being Function of (ComplRelStr (Necklace 4)),(Necklace 4) such that
A5: g is isomorphic by WAYBEL_1:def 8;
A6: ( g is one-to-one & g is monotone & ex g1 being Function of (Necklace 4),(ComplRelStr (Necklace 4)) st
( g1 = g " & g1 is monotone ) ) by A5, WAYBEL_0:def 38;
reconsider h = f * g as Function of (ComplRelStr (Necklace 4)),G ;
A7: dom h = the carrier of (ComplRelStr (Necklace 4)) by FUNCT_2:def 1;
A8: h is one-to-one by A4, A6;
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 9;
then g . x <= g . y by A6, WAYBEL_1:def 2;
then [(g . x),(g . y)] in the InternalRel of (Necklace 4) by ORDERS_2:def 9;
then [(f . (g . x)),(f . (g . y))] in the InternalRel of G by A4;
then [((f * g) . x),(f . (g . y))] in the InternalRel of G by FUNCT_2:21;
hence [(h . x),(h . y)] in the InternalRel of G by FUNCT_2:21; :: 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:21;
then [(f . (g . x)),(f . (g . y))] in the InternalRel of G by FUNCT_2:21;
then [(g . x),(g . y)] in the InternalRel of (Necklace 4) by A4;
then g . x <= g . y by ORDERS_2:def 9;
then x <= y by A5, WAYBEL_0:66;
hence [x,y] in the InternalRel of (ComplRelStr (Necklace 4)) by ORDERS_2:def 9; :: thesis: verum
end;
A10: ( 0 in the carrier of (ComplRelStr (Necklace 4)) & 1 in the carrier of (ComplRelStr (Necklace 4)) & 2 in the carrier of (ComplRelStr (Necklace 4)) & 3 in the carrier of (ComplRelStr (Necklace 4)) ) by A1, A2, ENUMSET1:def 2;
( [0 ,2] in the InternalRel of (ComplRelStr (Necklace 4)) & [2,0 ] in the InternalRel of (ComplRelStr (Necklace 4)) & [0 ,3] in the InternalRel of (ComplRelStr (Necklace 4)) & [3,0 ] in the InternalRel of (ComplRelStr (Necklace 4)) & [1,3] in the InternalRel of (ComplRelStr (Necklace 4)) & [3,1] in the InternalRel of (ComplRelStr (Necklace 4)) ) by Th11, ENUMSET1:def 4;
then A11: ( [(h . 0 ),(h . 2)] in the InternalRel of G & [(h . 2),(h . 0 )] in the InternalRel of G & [(h . 0 ),(h . 3)] in the InternalRel of G & [(h . 3),(h . 0 )] in the InternalRel of G & [(h . 1),(h . 3)] in the InternalRel of G & [(h . 3),(h . 1)] in the InternalRel of G ) by A9, A10;
A12: [(h . 0 ),(h . 1)] in the InternalRel of (ComplRelStr G)
proof
assume A13: not [(h . 0 ),(h . 1)] in the InternalRel of (ComplRelStr G) ; :: thesis: contradiction
[(h . 0 ),(h . 1)] in the InternalRel of G
proof
assume A14: not [(h . 0 ),(h . 1)] in the InternalRel of G ; :: thesis: contradiction
( h . 0 in the carrier of G & h . 1 in the carrier of G ) by A10, FUNCT_2:7;
then [(h . 0 ),(h . 1)] in [:the carrier of G,the carrier of G:] by ZFMISC_1:106;
then [(h . 0 ),(h . 1)] in ((id the carrier of G) \/ the InternalRel of G) \/ the InternalRel of (ComplRelStr G) by Th14;
then ( [(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;
then [(h . 0 ),(h . 1)] in id the carrier of G by A13, A14, XBOOLE_0:def 3;
then h . 0 = h . 1 by RELAT_1:def 10;
hence contradiction by A7, A8, A10, FUNCT_1:def 8; :: thesis: verum
end;
then A15: [0 ,1] in the InternalRel of (ComplRelStr (Necklace 4)) by A9, A10;
[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 A15, XBOOLE_0:def 4;
then the InternalRel of (Necklace 4) meets the InternalRel of (ComplRelStr (Necklace 4)) by XBOOLE_0:def 7;
hence contradiction by Th12; :: thesis: verum
end;
A16: [(h . 1),(h . 0 )] in the InternalRel of (ComplRelStr G)
proof
assume A17: not [(h . 1),(h . 0 )] in the InternalRel of (ComplRelStr G) ; :: thesis: contradiction
[(h . 1),(h . 0 )] in the InternalRel of G
proof
assume A18: not [(h . 1),(h . 0 )] in the InternalRel of G ; :: thesis: contradiction
( h . 0 in the carrier of G & h . 1 in the carrier of G ) by A10, FUNCT_2:7;
then [(h . 1),(h . 0 )] in [:the carrier of G,the carrier of G:] by ZFMISC_1:106;
then [(h . 1),(h . 0 )] in ((id the carrier of G) \/ the InternalRel of G) \/ the InternalRel of (ComplRelStr G) by Th14;
then ( [(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;
then [(h . 1),(h . 0 )] in id the carrier of G by A17, A18, XBOOLE_0:def 3;
then h . 0 = h . 1 by RELAT_1:def 10;
hence contradiction by A7, A8, A10, FUNCT_1:def 8; :: thesis: verum
end;
then A19: [1,0 ] in the InternalRel of (ComplRelStr (Necklace 4)) by A9, A10;
[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 A19, XBOOLE_0:def 4;
then the InternalRel of (Necklace 4) meets the InternalRel of (ComplRelStr (Necklace 4)) by XBOOLE_0:def 7;
hence contradiction by Th12; :: thesis: verum
end;
A20: [(h . 1),(h . 2)] in the InternalRel of (ComplRelStr G)
proof
assume A21: not [(h . 1),(h . 2)] in the InternalRel of (ComplRelStr G) ; :: thesis: contradiction
[(h . 1),(h . 2)] in the InternalRel of G
proof
assume A22: not [(h . 1),(h . 2)] in the InternalRel of G ; :: thesis: contradiction
( h . 1 in the carrier of G & h . 2 in the carrier of G ) by A10, FUNCT_2:7;
then [(h . 1),(h . 2)] in [:the carrier of G,the carrier of G:] by ZFMISC_1:106;
then [(h . 1),(h . 2)] in ((id the carrier of G) \/ the InternalRel of G) \/ the InternalRel of (ComplRelStr G) by Th14;
then ( [(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;
then [(h . 1),(h . 2)] in id the carrier of G by A21, A22, XBOOLE_0:def 3;
then h . 1 = h . 2 by RELAT_1:def 10;
hence contradiction by A7, A8, A10, FUNCT_1:def 8; :: thesis: verum
end;
then A23: [1,2] in the InternalRel of (ComplRelStr (Necklace 4)) by A9, A10;
[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 A23, XBOOLE_0:def 4;
then the InternalRel of (Necklace 4) meets the InternalRel of (ComplRelStr (Necklace 4)) by XBOOLE_0:def 7;
hence contradiction by Th12; :: thesis: verum
end;
A24: [(h . 2),(h . 1)] in the InternalRel of (ComplRelStr G)
proof
assume A25: not [(h . 2),(h . 1)] in the InternalRel of (ComplRelStr G) ; :: thesis: contradiction
[(h . 2),(h . 1)] in the InternalRel of G
proof
assume A26: not [(h . 2),(h . 1)] in the InternalRel of G ; :: thesis: contradiction
( h . 1 in the carrier of G & h . 2 in the carrier of G ) by A10, FUNCT_2:7;
then [(h . 2),(h . 1)] in [:the carrier of G,the carrier of G:] by ZFMISC_1:106;
then [(h . 2),(h . 1)] in ((id the carrier of G) \/ the InternalRel of G) \/ the InternalRel of (ComplRelStr G) by Th14;
then ( [(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;
then [(h . 2),(h . 1)] in id the carrier of G by A25, A26, XBOOLE_0:def 3;
then h . 1 = h . 2 by RELAT_1:def 10;
hence contradiction by A7, A8, A10, FUNCT_1:def 8; :: thesis: verum
end;
then A27: [2,1] in the InternalRel of (ComplRelStr (Necklace 4)) by A9, A10;
[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 A27, XBOOLE_0:def 4;
then the InternalRel of (Necklace 4) meets the InternalRel of (ComplRelStr (Necklace 4)) by XBOOLE_0:def 7;
hence contradiction by Th12; :: thesis: verum
end;
A28: [(h . 2),(h . 3)] in the InternalRel of (ComplRelStr G)
proof
assume A29: not [(h . 2),(h . 3)] in the InternalRel of (ComplRelStr G) ; :: thesis: contradiction
[(h . 2),(h . 3)] in the InternalRel of G
proof
assume A30: not [(h . 2),(h . 3)] in the InternalRel of G ; :: thesis: contradiction
( h . 2 in the carrier of G & h . 3 in the carrier of G ) by A10, FUNCT_2:7;
then [(h . 2),(h . 3)] in [:the carrier of G,the carrier of G:] by ZFMISC_1:106;
then [(h . 2),(h . 3)] in ((id the carrier of G) \/ the InternalRel of G) \/ the InternalRel of (ComplRelStr G) by Th14;
then ( [(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;
then [(h . 2),(h . 3)] in id the carrier of G by A29, A30, XBOOLE_0:def 3;
then h . 2 = h . 3 by RELAT_1:def 10;
hence contradiction by A7, A8, A10, FUNCT_1:def 8; :: thesis: verum
end;
then A31: [2,3] in the InternalRel of (ComplRelStr (Necklace 4)) by A9, A10;
[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 A31, XBOOLE_0:def 4;
then the InternalRel of (Necklace 4) meets the InternalRel of (ComplRelStr (Necklace 4)) by XBOOLE_0:def 7;
hence contradiction by Th12; :: thesis: verum
end;
A32: [(h . 3),(h . 2)] in the InternalRel of (ComplRelStr G)
proof
assume A33: not [(h . 3),(h . 2)] in the InternalRel of (ComplRelStr G) ; :: thesis: contradiction
[(h . 3),(h . 2)] in the InternalRel of G
proof
assume A34: not [(h . 3),(h . 2)] in the InternalRel of G ; :: thesis: contradiction
( h . 2 in the carrier of G & h . 3 in the carrier of G ) by A10, FUNCT_2:7;
then [(h . 3),(h . 2)] in [:the carrier of G,the carrier of G:] by ZFMISC_1:106;
then [(h . 3),(h . 2)] in ((id the carrier of G) \/ the InternalRel of G) \/ the InternalRel of (ComplRelStr G) by Th14;
then ( [(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;
then [(h . 3),(h . 2)] in id the carrier of G by A33, A34, XBOOLE_0:def 3;
then h . 2 = h . 3 by RELAT_1:def 10;
hence contradiction by A7, A8, A10, FUNCT_1:def 8; :: thesis: verum
end;
then A35: [3,2] in the InternalRel of (ComplRelStr (Necklace 4)) by A9, A10;
[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 A35, XBOOLE_0:def 4;
then the InternalRel of (Necklace 4) meets the InternalRel of (ComplRelStr (Necklace 4)) by XBOOLE_0:def 7;
hence contradiction by Th12; :: thesis: verum
end;
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 A36: [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 A36, ENUMSET1:def 4, NECKLA_2:2;
suppose [x,y] = [0 ,1] ; :: thesis: [(h . x),(h . y)] in the InternalRel of (ComplRelStr G)
then ( x = 0 & y = 1 ) by ZFMISC_1:33;
hence [(h . x),(h . y)] in the InternalRel of (ComplRelStr G) by A12; :: thesis: verum
end;
suppose [x,y] = [1,0 ] ; :: thesis: [(h . x),(h . y)] in the InternalRel of (ComplRelStr G)
then ( x = 1 & y = 0 ) by ZFMISC_1:33;
hence [(h . x),(h . y)] in the InternalRel of (ComplRelStr G) by A16; :: thesis: verum
end;
suppose [x,y] = [1,2] ; :: thesis: [(h . x),(h . y)] in the InternalRel of (ComplRelStr G)
then ( x = 1 & y = 2 ) by ZFMISC_1:33;
hence [(h . x),(h . y)] in the InternalRel of (ComplRelStr G) by A20; :: thesis: verum
end;
suppose [x,y] = [2,1] ; :: thesis: [(h . x),(h . y)] in the InternalRel of (ComplRelStr G)
then ( x = 2 & y = 1 ) by ZFMISC_1:33;
hence [(h . x),(h . y)] in the InternalRel of (ComplRelStr G) by A24; :: thesis: verum
end;
suppose [x,y] = [2,3] ; :: thesis: [(h . x),(h . y)] in the InternalRel of (ComplRelStr G)
then ( x = 2 & y = 3 ) by ZFMISC_1:33;
hence [(h . x),(h . y)] in the InternalRel of (ComplRelStr G) by A28; :: thesis: verum
end;
suppose [x,y] = [3,2] ; :: thesis: [(h . x),(h . y)] in the InternalRel of (ComplRelStr G)
then ( x = 3 & y = 2 ) by ZFMISC_1:33;
hence [(h . x),(h . y)] in the InternalRel of (ComplRelStr G) by A32; :: thesis: verum
end;
end;
end;
assume A37: [(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 A1, ENUMSET1:def 2;
end;
end;
hence ComplRelStr G embeds Necklace 4 by A2, A3, A8, NECKLACE:def 2; :: 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
A42: ( f is one-to-one & ( 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) ) ) ) by NECKLACE:def 2;
A43: dom f = the carrier of (Necklace 4) by FUNCT_2:def 1;
A44: ( 0 in the carrier of (Necklace 4) & 1 in the carrier of (Necklace 4) & 2 in the carrier of (Necklace 4) & 3 in the carrier of (Necklace 4) ) by A1, ENUMSET1:def 2;
( [0 ,1] in the InternalRel of (Necklace 4) & [1,0 ] in the InternalRel of (Necklace 4) & [1,2] in the InternalRel of (Necklace 4) & [2,1] in the InternalRel of (Necklace 4) & [2,3] in the InternalRel of (Necklace 4) & [3,2] in the InternalRel of (Necklace 4) ) by ENUMSET1:def 4, NECKLA_2:2;
then A45: ( [(f . 0 ),(f . 1)] in the InternalRel of (ComplRelStr G) & [(f . 1),(f . 0 )] in the InternalRel of (ComplRelStr G) & [(f . 1),(f . 2)] in the InternalRel of (ComplRelStr G) & [(f . 2),(f . 1)] in the InternalRel of (ComplRelStr G) & [(f . 2),(f . 3)] in the InternalRel of (ComplRelStr G) & [(f . 3),(f . 2)] in the InternalRel of (ComplRelStr G) ) by A42, A44;
A46: [(f . 0 ),(f . 2)] in the InternalRel of G
proof
assume A47: not [(f . 0 ),(f . 2)] in the InternalRel of G ; :: thesis: contradiction
[(f . 0 ),(f . 2)] in the InternalRel of (ComplRelStr G)
proof
assume A48: not [(f . 0 ),(f . 2)] in the InternalRel of (ComplRelStr G) ; :: thesis: contradiction
( f . 0 in the carrier of (ComplRelStr G) & f . 2 in the carrier of (ComplRelStr G) ) by A44, FUNCT_2:7;
then [(f . 0 ),(f . 2)] in [:the carrier of G,the carrier of G:] by A3, ZFMISC_1:106;
then [(f . 0 ),(f . 2)] in ((id the carrier of G) \/ the InternalRel of G) \/ the InternalRel of (ComplRelStr G) by Th14;
then ( [(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;
then [(f . 0 ),(f . 2)] in id the carrier of G by A47, A48, XBOOLE_0:def 3;
then f . 0 = f . 2 by RELAT_1:def 10;
hence contradiction by A42, A43, A44, FUNCT_1:def 8; :: thesis: verum
end;
then A49: [0 ,2] in the InternalRel of (Necklace 4) by A42, A44;
[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 A49, XBOOLE_0:def 4;
then the InternalRel of (Necklace 4) meets the InternalRel of (ComplRelStr (Necklace 4)) by XBOOLE_0:def 7;
hence contradiction by Th12; :: thesis: verum
end;
A50: [(f . 2),(f . 0 )] in the InternalRel of G
proof
assume A51: not [(f . 2),(f . 0 )] in the InternalRel of G ; :: thesis: contradiction
[(f . 2),(f . 0 )] in the InternalRel of (ComplRelStr G)
proof
assume A52: not [(f . 2),(f . 0 )] in the InternalRel of (ComplRelStr G) ; :: thesis: contradiction
( f . 0 in the carrier of (ComplRelStr G) & f . 2 in the carrier of (ComplRelStr G) ) by A44, FUNCT_2:7;
then [(f . 2),(f . 0 )] in [:the carrier of G,the carrier of G:] by A3, ZFMISC_1:106;
then [(f . 2),(f . 0 )] in ((id the carrier of G) \/ the InternalRel of G) \/ the InternalRel of (ComplRelStr G) by Th14;
then ( [(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;
then [(f . 2),(f . 0 )] in id the carrier of G by A51, A52, XBOOLE_0:def 3;
then f . 0 = f . 2 by RELAT_1:def 10;
hence contradiction by A42, A43, A44, FUNCT_1:def 8; :: thesis: verum
end;
then A53: [2,0 ] in the InternalRel of (Necklace 4) by A42, A44;
[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 A53, XBOOLE_0:def 4;
then the InternalRel of (Necklace 4) meets the InternalRel of (ComplRelStr (Necklace 4)) by XBOOLE_0:def 7;
hence contradiction by Th12; :: thesis: verum
end;
A54: [(f . 0 ),(f . 3)] in the InternalRel of G
proof
assume A55: not [(f . 0 ),(f . 3)] in the InternalRel of G ; :: thesis: contradiction
[(f . 0 ),(f . 3)] in the InternalRel of (ComplRelStr G)
proof
assume A56: not [(f . 0 ),(f . 3)] in the InternalRel of (ComplRelStr G) ; :: thesis: contradiction
( f . 0 in the carrier of (ComplRelStr G) & f . 3 in the carrier of (ComplRelStr G) ) by A44, FUNCT_2:7;
then [(f . 0 ),(f . 3)] in [:the carrier of G,the carrier of G:] by A3, ZFMISC_1:106;
then [(f . 0 ),(f . 3)] in ((id the carrier of G) \/ the InternalRel of G) \/ the InternalRel of (ComplRelStr G) by Th14;
then ( [(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;
then [(f . 0 ),(f . 3)] in id the carrier of G by A55, A56, XBOOLE_0:def 3;
then f . 0 = f . 3 by RELAT_1:def 10;
hence contradiction by A42, A43, A44, FUNCT_1:def 8; :: thesis: verum
end;
then A57: [0 ,3] in the InternalRel of (Necklace 4) by A42, A44;
[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 A57, XBOOLE_0:def 4;
then the InternalRel of (Necklace 4) meets the InternalRel of (ComplRelStr (Necklace 4)) by XBOOLE_0:def 7;
hence contradiction by Th12; :: thesis: verum
end;
A58: [(f . 3),(f . 0 )] in the InternalRel of G
proof
assume A59: not [(f . 3),(f . 0 )] in the InternalRel of G ; :: thesis: contradiction
[(f . 3),(f . 0 )] in the InternalRel of (ComplRelStr G)
proof
assume A60: not [(f . 3),(f . 0 )] in the InternalRel of (ComplRelStr G) ; :: thesis: contradiction
( f . 0 in the carrier of (ComplRelStr G) & f . 3 in the carrier of (ComplRelStr G) ) by A44, FUNCT_2:7;
then [(f . 3),(f . 0 )] in [:the carrier of G,the carrier of G:] by A3, ZFMISC_1:106;
then [(f . 3),(f . 0 )] in ((id the carrier of G) \/ the InternalRel of G) \/ the InternalRel of (ComplRelStr G) by Th14;
then ( [(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;
then [(f . 3),(f . 0 )] in id the carrier of G by A59, A60, XBOOLE_0:def 3;
then f . 0 = f . 3 by RELAT_1:def 10;
hence contradiction by A42, A43, A44, FUNCT_1:def 8; :: thesis: verum
end;
then A61: [3,0 ] in the InternalRel of (Necklace 4) by A42, A44;
[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 A61, XBOOLE_0:def 4;
then the InternalRel of (Necklace 4) meets the InternalRel of (ComplRelStr (Necklace 4)) by XBOOLE_0:def 7;
hence contradiction by Th12; :: thesis: verum
end;
A62: [(f . 1),(f . 3)] in the InternalRel of G
proof
assume A63: not [(f . 1),(f . 3)] in the InternalRel of G ; :: thesis: contradiction
[(f . 1),(f . 3)] in the InternalRel of (ComplRelStr G)
proof
assume A64: not [(f . 1),(f . 3)] in the InternalRel of (ComplRelStr G) ; :: thesis: contradiction
( f . 1 in the carrier of (ComplRelStr G) & f . 3 in the carrier of (ComplRelStr G) ) by A44, FUNCT_2:7;
then [(f . 1),(f . 3)] in [:the carrier of G,the carrier of G:] by A3, ZFMISC_1:106;
then [(f . 1),(f . 3)] in ((id the carrier of G) \/ the InternalRel of G) \/ the InternalRel of (ComplRelStr G) by Th14;
then ( [(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;
then [(f . 1),(f . 3)] in id the carrier of G by A63, A64, XBOOLE_0:def 3;
then f . 1 = f . 3 by RELAT_1:def 10;
hence contradiction by A42, A43, A44, FUNCT_1:def 8; :: thesis: verum
end;
then A65: [1,3] in the InternalRel of (Necklace 4) by A42, A44;
[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 A65, XBOOLE_0:def 4;
then the InternalRel of (Necklace 4) meets the InternalRel of (ComplRelStr (Necklace 4)) by XBOOLE_0:def 7;
hence contradiction by Th12; :: thesis: verum
end;
A66: [(f . 3),(f . 1)] in the InternalRel of G
proof
assume A67: not [(f . 3),(f . 1)] in the InternalRel of G ; :: thesis: contradiction
[(f . 3),(f . 1)] in the InternalRel of (ComplRelStr G)
proof
assume A68: not [(f . 3),(f . 1)] in the InternalRel of (ComplRelStr G) ; :: thesis: contradiction
( f . 1 in the carrier of (ComplRelStr G) & f . 3 in the carrier of (ComplRelStr G) ) by A44, FUNCT_2:7;
then [(f . 3),(f . 1)] in [:the carrier of G,the carrier of G:] by A3, ZFMISC_1:106;
then [(f . 3),(f . 1)] in ((id the carrier of G) \/ the InternalRel of G) \/ the InternalRel of (ComplRelStr G) by Th14;
then ( [(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;
then [(f . 3),(f . 1)] in id the carrier of G by A67, A68, XBOOLE_0:def 3;
then f . 1 = f . 3 by RELAT_1:def 10;
hence contradiction by A42, A43, A44, FUNCT_1:def 8; :: thesis: verum
end;
then A69: [3,1] in the InternalRel of (Necklace 4) by A42, A44;
[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 A69, XBOOLE_0:def 4;
then the InternalRel of (Necklace 4) meets the InternalRel of (ComplRelStr (Necklace 4)) by XBOOLE_0:def 7;
hence contradiction by Th12; :: thesis: verum
end;
A70: 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 )
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 A71: [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 A71, Th11, ENUMSET1:def 4;
suppose [x,y] = [0 ,2] ; :: thesis: [(f . x),(f . y)] in the InternalRel of G
then ( x = 0 & y = 2 ) by ZFMISC_1:33;
hence [(f . x),(f . y)] in the InternalRel of G by A46; :: thesis: verum
end;
suppose [x,y] = [2,0 ] ; :: thesis: [(f . x),(f . y)] in the InternalRel of G
then ( x = 2 & y = 0 ) by ZFMISC_1:33;
hence [(f . x),(f . y)] in the InternalRel of G by A50; :: thesis: verum
end;
suppose [x,y] = [0 ,3] ; :: thesis: [(f . x),(f . y)] in the InternalRel of G
then ( x = 0 & y = 3 ) by ZFMISC_1:33;
hence [(f . x),(f . y)] in the InternalRel of G by A54; :: thesis: verum
end;
suppose [x,y] = [3,0 ] ; :: thesis: [(f . x),(f . y)] in the InternalRel of G
then ( x = 3 & y = 0 ) by ZFMISC_1:33;
hence [(f . x),(f . y)] in the InternalRel of G by A58; :: thesis: verum
end;
suppose [x,y] = [1,3] ; :: thesis: [(f . x),(f . y)] in the InternalRel of G
then ( x = 1 & y = 3 ) by ZFMISC_1:33;
hence [(f . x),(f . y)] in the InternalRel of G by A62; :: thesis: verum
end;
suppose [x,y] = [3,1] ; :: thesis: [(f . x),(f . y)] in the InternalRel of G
then ( x = 3 & y = 1 ) by ZFMISC_1:33;
hence [(f . x),(f . y)] in the InternalRel of G by A66; :: thesis: verum
end;
end;
end;
assume A72: [(f . x),(f . y)] in the InternalRel of G ; :: thesis: [x,y] in the InternalRel of (ComplRelStr (Necklace 4))
A73: the carrier of (Necklace 4) = the carrier of (ComplRelStr (Necklace 4)) by NECKLACE:def 9;
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 A1, A73, ENUMSET1:def 2;
end;
end;
reconsider f = f as Function of (ComplRelStr (Necklace 4)),G by A2, A3;
consider g being Function of (Necklace 4),(ComplRelStr (Necklace 4)) such that
A78: g is isomorphic by NECKLACE:30, WAYBEL_1:def 8;
A79: ( g is one-to-one & g is monotone & ex g1 being Function of (ComplRelStr (Necklace 4)),(Necklace 4) st
( g1 = g " & g1 is monotone ) ) by A78, WAYBEL_0:def 38;
reconsider h = f * g as Function of (Necklace 4),G ;
A80: h is one-to-one by A42, A79;
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 9;
then g . x <= g . y by A79, WAYBEL_1:def 2;
then [(g . x),(g . y)] in the InternalRel of (ComplRelStr (Necklace 4)) by ORDERS_2:def 9;
then [(f . (g . x)),(f . (g . y))] in the InternalRel of G by A70;
then [((f * g) . x),(f . (g . y))] in the InternalRel of G by FUNCT_2:21;
hence [(h . x),(h . y)] in the InternalRel of G by FUNCT_2:21; :: 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:21;
then [(f . (g . x)),(f . (g . y))] in the InternalRel of G by FUNCT_2:21;
then [(g . x),(g . y)] in the InternalRel of (ComplRelStr (Necklace 4)) by A70;
then g . x <= g . y by ORDERS_2:def 9;
then x <= y by A78, WAYBEL_0:66;
hence [x,y] in the InternalRel of (Necklace 4) by ORDERS_2:def 9; :: thesis: verum
end;
hence G embeds Necklace 4 by A80, NECKLACE:def 2; :: thesis: verum