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 ();
set CmpG = ComplRelStr G;
A1: the carrier of () = the carrier of G by NECKLACE:def 8;
A2: the carrier of () = {0,1,2,3} by ;
then A3: 0 in the carrier of () by ENUMSET1:def 2;
A4: the carrier of () = the carrier of () 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 are_isomorphic by ;
then consider g being Function of (),() such that
A5: g is isomorphic by WAYBEL_1:def 8;
assume G embeds Necklace 4 ; :: thesis:
then consider f being Function of (),G such that
A6: f is V24() and
A7: for x, y being Element of () holds
( [x,y] in the InternalRel of () iff [(f . x),(f . y)] in the InternalRel of G ) ;
reconsider h = f * g as Function of (),G ;
A8: ( g is V24() & g is monotone ) by ;
A9: for x, y being Element of () holds
( [x,y] in the InternalRel of () iff [(h . x),(h . y)] in the InternalRel of G )
proof
let x, y be Element of (); :: thesis: ( [x,y] in the InternalRel of () iff [(h . x),(h . y)] in the InternalRel of G )
thus ( [x,y] in the InternalRel of () 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 () )
proof
assume [x,y] in the InternalRel of () ; :: thesis: [(h . x),(h . y)] in the InternalRel of G
then x <= y by ORDERS_2:def 5;
then g . x <= g . y by ;
then [(g . x),(g . y)] in the InternalRel of () 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 ()
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 () by A7;
then g . x <= g . y by ORDERS_2:def 5;
then x <= y by ;
hence [x,y] in the InternalRel of () by ORDERS_2:def 5; :: thesis: verum
end;
A10: 0 in the carrier of () by ;
A11: 1 in the carrier of () by ;
A12: dom h = the carrier of () by FUNCT_2:def 1;
A13: [(h . 0),(h . 1)] in the InternalRel of ()
proof
assume A14: not [(h . 0),(h . 1)] in the InternalRel of () ; :: 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 ;
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 () 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 () ) 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 ;
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 () by A9, A10, A11;
[0,1] in the InternalRel of () by ;
then [0,1] in the InternalRel of () /\ the InternalRel of () by ;
then the InternalRel of () meets the InternalRel of () ;
hence contradiction by Th12; :: thesis: verum
end;
A17: 2 in the carrier of () by ;
A18: [(h . 1),(h . 2)] in the InternalRel of ()
proof
assume A19: not [(h . 1),(h . 2)] in the InternalRel of () ; :: 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 ;
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 () 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 () ) 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 ;
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 () by A9, A11, A17;
[1,2] in the InternalRel of () by ;
then [1,2] in the InternalRel of () /\ the InternalRel of () by ;
then the InternalRel of () meets the InternalRel of () ;
hence contradiction by Th12; :: thesis: verum
end;
A22: 3 in the carrier of () by ;
A23: [(h . 2),(h . 3)] in the InternalRel of ()
proof
assume A24: not [(h . 2),(h . 3)] in the InternalRel of () ; :: 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 ;
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 () 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 () ) 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 ;
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 () by A9, A17, A22;
[2,3] in the InternalRel of () by ;
then [2,3] in the InternalRel of () /\ the InternalRel of () by ;
then the InternalRel of () meets the InternalRel of () ;
hence contradiction by Th12; :: thesis: verum
end;
[3,1] in the InternalRel of () by ;
then A27: [(h . 3),(h . 1)] in the InternalRel of G by A9, A11, A22;
[1,3] in the InternalRel of () by ;
then A28: [(h . 1),(h . 3)] in the InternalRel of G by A9, A11, A22;
[3,0] in the InternalRel of () by ;
then A29: [(h . 3),(h . 0)] in the InternalRel of G by A9, A10, A22;
[0,3] in the InternalRel of () by ;
then A30: [(h . 0),(h . 3)] in the InternalRel of G by A9, A10, A22;
A31: [(h . 1),(h . 0)] in the InternalRel of ()
proof
assume A32: not [(h . 1),(h . 0)] in the InternalRel of () ; :: 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 ;
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 () 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 () ) 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 ;
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 () by A9, A10, A11;
[1,0] in the InternalRel of () by ;
then [1,0] in the InternalRel of () /\ the InternalRel of () by ;
then the InternalRel of () meets the InternalRel of () ;
hence contradiction by Th12; :: thesis: verum
end;
A35: [(h . 2),(h . 1)] in the InternalRel of ()
proof
assume A36: not [(h . 2),(h . 1)] in the InternalRel of () ; :: 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 ;
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 () 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 () ) 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 ;
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 () by A9, A11, A17;
[2,1] in the InternalRel of () by ;
then [2,1] in the InternalRel of () /\ the InternalRel of () by ;
then the InternalRel of () meets the InternalRel of () ;
hence contradiction by Th12; :: thesis: verum
end;
A39: [(h . 3),(h . 2)] in the InternalRel of ()
proof
assume A40: not [(h . 3),(h . 2)] in the InternalRel of () ; :: 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 ;
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 () 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 () ) 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 ;
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 () by A9, A17, A22;
[3,2] in the InternalRel of () by ;
then [3,2] in the InternalRel of () /\ the InternalRel of () by ;
then the InternalRel of () meets the InternalRel of () ;
hence contradiction by Th12; :: thesis: verum
end;
[2,0] in the InternalRel of () by ;
then A43: [(h . 2),(h . 0)] in the InternalRel of G by A9, A10, A17;
[0,2] in the InternalRel of () by ;
then A44: [(h . 0),(h . 2)] in the InternalRel of G by A9, A10, A17;
for x, y being Element of () holds
( [x,y] in the InternalRel of () iff [(h . x),(h . y)] in the InternalRel of () )
proof
let x, y be Element of (); :: thesis: ( [x,y] in the InternalRel of () iff [(h . x),(h . y)] in the InternalRel of () )
thus ( [x,y] in the InternalRel of () implies [(h . x),(h . y)] in the InternalRel of () ) :: thesis: ( [(h . x),(h . y)] in the InternalRel of () implies [x,y] in the InternalRel of () )
proof
assume A45: [x,y] in the InternalRel of () ; :: thesis: [(h . x),(h . y)] in the InternalRel of ()
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 ;
suppose A46: [x,y] = [0,1] ; :: thesis: [(h . x),(h . y)] in the InternalRel of ()
then x = 0 by XTUPLE_0:1;
hence [(h . x),(h . y)] in the InternalRel of () by ; :: thesis: verum
end;
suppose A47: [x,y] = [1,0] ; :: thesis: [(h . x),(h . y)] in the InternalRel of ()
then x = 1 by XTUPLE_0:1;
hence [(h . x),(h . y)] in the InternalRel of () by ; :: thesis: verum
end;
suppose A48: [x,y] = [1,2] ; :: thesis: [(h . x),(h . y)] in the InternalRel of ()
then x = 1 by XTUPLE_0:1;
hence [(h . x),(h . y)] in the InternalRel of () by ; :: thesis: verum
end;
suppose A49: [x,y] = [2,1] ; :: thesis: [(h . x),(h . y)] in the InternalRel of ()
then x = 2 by XTUPLE_0:1;
hence [(h . x),(h . y)] in the InternalRel of () by ; :: thesis: verum
end;
suppose A50: [x,y] = [2,3] ; :: thesis: [(h . x),(h . y)] in the InternalRel of ()
then x = 2 by XTUPLE_0:1;
hence [(h . x),(h . y)] in the InternalRel of () by ; :: thesis: verum
end;
suppose A51: [x,y] = [3,2] ; :: thesis: [(h . x),(h . y)] in the InternalRel of ()
then x = 3 by XTUPLE_0:1;
hence [(h . x),(h . y)] in the InternalRel of () by ; :: thesis: verum
end;
end;
end;
assume A52: [(h . x),(h . y)] in the InternalRel of () ; :: thesis: [x,y] in the InternalRel of ()
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 ;
suppose A53: ( x = 0 & y = 0 ) ; :: thesis: [x,y] in the InternalRel of ()
then h . 0 in the carrier of () by ;
hence [x,y] in the InternalRel of () by ; :: thesis: verum
end;
suppose ( x = 0 & y = 1 ) ; :: thesis: [x,y] in the InternalRel of ()
hence [x,y] in the InternalRel of () by ; :: thesis: verum
end;
suppose ( x = 0 & y = 2 ) ; :: thesis: [x,y] in the InternalRel of ()
then [(h . 0),(h . 2)] in the InternalRel of G /\ the InternalRel of () by ;
then the InternalRel of G meets the InternalRel of () ;
hence [x,y] in the InternalRel of () by Th12; :: thesis: verum
end;
suppose ( x = 0 & y = 3 ) ; :: thesis: [x,y] in the InternalRel of ()
then [(h . 0),(h . 3)] in the InternalRel of G /\ the InternalRel of () by ;
then the InternalRel of G meets the InternalRel of () ;
hence [x,y] in the InternalRel of () by Th12; :: thesis: verum
end;
suppose ( x = 1 & y = 0 ) ; :: thesis: [x,y] in the InternalRel of ()
hence [x,y] in the InternalRel of () by ; :: thesis: verum
end;
suppose A54: ( x = 1 & y = 1 ) ; :: thesis: [x,y] in the InternalRel of ()
then h . 1 in the carrier of () by ;
hence [x,y] in the InternalRel of () by ; :: thesis: verum
end;
suppose ( x = 1 & y = 2 ) ; :: thesis: [x,y] in the InternalRel of ()
hence [x,y] in the InternalRel of () by ; :: thesis: verum
end;
suppose ( x = 1 & y = 3 ) ; :: thesis: [x,y] in the InternalRel of ()
then [(h . 1),(h . 3)] in the InternalRel of G /\ the InternalRel of () by ;
then the InternalRel of G meets the InternalRel of () ;
hence [x,y] in the InternalRel of () by Th12; :: thesis: verum
end;
suppose ( x = 2 & y = 0 ) ; :: thesis: [x,y] in the InternalRel of ()
then [(h . 2),(h . 0)] in the InternalRel of G /\ the InternalRel of () by ;
then the InternalRel of G meets the InternalRel of () ;
hence [x,y] in the InternalRel of () by Th12; :: thesis: verum
end;
suppose ( x = 2 & y = 1 ) ; :: thesis: [x,y] in the InternalRel of ()
hence [x,y] in the InternalRel of () by ; :: thesis: verum
end;
suppose A55: ( x = 2 & y = 2 ) ; :: thesis: [x,y] in the InternalRel of ()
then h . 2 in the carrier of () by ;
hence [x,y] in the InternalRel of () by ; :: thesis: verum
end;
suppose ( x = 2 & y = 3 ) ; :: thesis: [x,y] in the InternalRel of ()
hence [x,y] in the InternalRel of () by ; :: thesis: verum
end;
suppose ( x = 3 & y = 0 ) ; :: thesis: [x,y] in the InternalRel of ()
then [(h . 3),(h . 0)] in the InternalRel of G /\ the InternalRel of () by ;
then the InternalRel of G meets the InternalRel of () ;
hence [x,y] in the InternalRel of () by Th12; :: thesis: verum
end;
suppose ( x = 3 & y = 1 ) ; :: thesis: [x,y] in the InternalRel of ()
then [(h . 3),(h . 1)] in the InternalRel of G /\ the InternalRel of () by ;
then the InternalRel of G meets the InternalRel of () ;
hence [x,y] in the InternalRel of () by Th12; :: thesis: verum
end;
suppose ( x = 3 & y = 2 ) ; :: thesis: [x,y] in the InternalRel of ()
hence [x,y] in the InternalRel of () by ; :: thesis: verum
end;
suppose A56: ( x = 3 & y = 3 ) ; :: thesis: [x,y] in the InternalRel of ()
then h . 3 in the carrier of () by ;
hence [x,y] in the InternalRel of () by ; :: 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:
then consider f being Function of (),() such that
A57: f is V24() and
A58: for x, y being Element of () holds
( [x,y] in the InternalRel of () iff [(f . x),(f . y)] in the InternalRel of () ) ;
consider g being Function of (),() such that
A59: g is isomorphic by ;
A60: 2 in the carrier of () by ;
A61: dom f = the carrier of () 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 ()
proof
( f . 0 in the carrier of () & f . 2 in the carrier of () ) by ;
then [(f . 0),(f . 2)] in [: the carrier of G, the carrier of G:] by ;
then [(f . 0),(f . 2)] in ((id the carrier of G) \/ the InternalRel of G) \/ the InternalRel of () 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 () ) by XBOOLE_0:def 3;
assume not [(f . 0),(f . 2)] in the InternalRel of () ; :: thesis: contradiction
then [(f . 0),(f . 2)] in id the carrier of G by ;
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 () by A58, A3, A60;
[0,2] in the InternalRel of () by ;
then [0,2] in the InternalRel of () /\ the InternalRel of () by ;
then the InternalRel of () meets the InternalRel of () ;
hence contradiction by Th12; :: thesis: verum
end;
A66: 3 in the carrier of () by ;
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 ()
proof
( f . 0 in the carrier of () & f . 3 in the carrier of () ) by ;
then [(f . 0),(f . 3)] in [: the carrier of G, the carrier of G:] by ;
then [(f . 0),(f . 3)] in ((id the carrier of G) \/ the InternalRel of G) \/ the InternalRel of () 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 () ) by XBOOLE_0:def 3;
assume not [(f . 0),(f . 3)] in the InternalRel of () ; :: thesis: contradiction
then [(f . 0),(f . 3)] in id the carrier of G by ;
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 () by A58, A3, A66;
[0,3] in the InternalRel of () by ;
then [0,3] in the InternalRel of () /\ the InternalRel of () by ;
then the InternalRel of () meets the InternalRel of () ;
hence contradiction by Th12; :: thesis: verum
end;
A71: 1 in the carrier of () by ;
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 ()
proof
( f . 1 in the carrier of () & f . 3 in the carrier of () ) by ;
then [(f . 1),(f . 3)] in [: the carrier of G, the carrier of G:] by ;
then [(f . 1),(f . 3)] in ((id the carrier of G) \/ the InternalRel of G) \/ the InternalRel of () 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 () ) by XBOOLE_0:def 3;
assume not [(f . 1),(f . 3)] in the InternalRel of () ; :: thesis: contradiction
then [(f . 1),(f . 3)] in id the carrier of G by ;
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 () by ;
[1,3] in the InternalRel of () by ;
then [1,3] in the InternalRel of () /\ the InternalRel of () by ;
then the InternalRel of () meets the InternalRel of () ;
hence contradiction by Th12; :: thesis: verum
end;
[3,2] in the InternalRel of () by ;
then A76: [(f . 3),(f . 2)] in the InternalRel of () by ;
[2,3] in the InternalRel of () by ;
then A77: [(f . 2),(f . 3)] in the InternalRel of () by ;
[1,2] in the InternalRel of () by ;
then A78: [(f . 1),(f . 2)] in the InternalRel of () by ;
[1,0] in the InternalRel of () by ;
then A79: [(f . 1),(f . 0)] in the InternalRel of () 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 ()
proof
( f . 0 in the carrier of () & f . 2 in the carrier of () ) by ;
then [(f . 2),(f . 0)] in [: the carrier of G, the carrier of G:] by ;
then [(f . 2),(f . 0)] in ((id the carrier of G) \/ the InternalRel of G) \/ the InternalRel of () 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 () ) by XBOOLE_0:def 3;
assume not [(f . 2),(f . 0)] in the InternalRel of () ; :: thesis: contradiction
then [(f . 2),(f . 0)] in id the carrier of G by ;
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 () by A58, A3, A60;
[2,0] in the InternalRel of () by ;
then [2,0] in the InternalRel of () /\ the InternalRel of () by ;
then the InternalRel of () meets the InternalRel of () ;
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 ()
proof
( f . 0 in the carrier of () & f . 3 in the carrier of () ) by ;
then [(f . 3),(f . 0)] in [: the carrier of G, the carrier of G:] by ;
then [(f . 3),(f . 0)] in ((id the carrier of G) \/ the InternalRel of G) \/ the InternalRel of () 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 () ) by XBOOLE_0:def 3;
assume not [(f . 3),(f . 0)] in the InternalRel of () ; :: thesis: contradiction
then [(f . 3),(f . 0)] in id the carrier of G by ;
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 () by A58, A3, A66;
[3,0] in the InternalRel of () by ;
then [3,0] in the InternalRel of () /\ the InternalRel of () by ;
then the InternalRel of () meets the InternalRel of () ;
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 ()
proof
( f . 1 in the carrier of () & f . 3 in the carrier of () ) by ;
then [(f . 3),(f . 1)] in [: the carrier of G, the carrier of G:] by ;
then [(f . 3),(f . 1)] in ((id the carrier of G) \/ the InternalRel of G) \/ the InternalRel of () 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 () ) by XBOOLE_0:def 3;
assume not [(f . 3),(f . 1)] in the InternalRel of () ; :: thesis: contradiction
then [(f . 3),(f . 1)] in id the carrier of G by ;
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 () by ;
[3,1] in the InternalRel of () by ;
then [3,1] in the InternalRel of () /\ the InternalRel of () by ;
then the InternalRel of () meets the InternalRel of () ;
hence contradiction by Th12; :: thesis: verum
end;
[2,1] in the InternalRel of () by ;
then A92: [(f . 2),(f . 1)] in the InternalRel of () by ;
[0,1] in the InternalRel of () by ;
then A93: [(f . 0),(f . 1)] in the InternalRel of () by A58, A3, A71;
A94: for x, y being Element of () holds
( [x,y] in the InternalRel of () iff [(f . x),(f . y)] in the InternalRel of G )
proof
let x, y be Element of (); :: thesis: ( [x,y] in the InternalRel of () iff [(f . x),(f . y)] in the InternalRel of G )
A95: the carrier of () = the carrier of () by NECKLACE:def 8;
thus ( [x,y] in the InternalRel of () 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 () )
proof
assume A96: [x,y] in the InternalRel of () ; :: 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 ;
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 ; :: 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 ; :: 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 ; :: 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 ; :: 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 ; :: 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 ; :: thesis: verum
end;
end;
end;
assume A103: [(f . x),(f . y)] in the InternalRel of G ; :: thesis: [x,y] in the InternalRel of ()
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 ;
suppose A104: ( x = 0 & y = 0 ) ; :: thesis: [x,y] in the InternalRel of ()
then f . 0 in the carrier of G by ;
hence [x,y] in the InternalRel of () by ; :: thesis: verum
end;
suppose ( x = 0 & y = 1 ) ; :: thesis: [x,y] in the InternalRel of ()
then [(f . 0),(f . 1)] in the InternalRel of G /\ the InternalRel of () by ;
then the InternalRel of G meets the InternalRel of () ;
hence [x,y] in the InternalRel of () by Th12; :: thesis: verum
end;
suppose ( x = 0 & y = 2 ) ; :: thesis: [x,y] in the InternalRel of ()
hence [x,y] in the InternalRel of () by ; :: thesis: verum
end;
suppose ( x = 0 & y = 3 ) ; :: thesis: [x,y] in the InternalRel of ()
hence [x,y] in the InternalRel of () by ; :: thesis: verum
end;
suppose ( x = 1 & y = 0 ) ; :: thesis: [x,y] in the InternalRel of ()
then [(f . 1),(f . 0)] in the InternalRel of G /\ the InternalRel of () by ;
then the InternalRel of G meets the InternalRel of () ;
hence [x,y] in the InternalRel of () by Th12; :: thesis: verum
end;
suppose ( x = 2 & y = 0 ) ; :: thesis: [x,y] in the InternalRel of ()
hence [x,y] in the InternalRel of () by ; :: thesis: verum
end;
suppose ( x = 3 & y = 0 ) ; :: thesis: [x,y] in the InternalRel of ()
hence [x,y] in the InternalRel of () by ; :: thesis: verum
end;
suppose A105: ( x = 1 & y = 1 ) ; :: thesis: [x,y] in the InternalRel of ()
then f . 1 in the carrier of G by ;
hence [x,y] in the InternalRel of () by ; :: thesis: verum
end;
suppose ( x = 1 & y = 2 ) ; :: thesis: [x,y] in the InternalRel of ()
then [(f . 1),(f . 2)] in the InternalRel of G /\ the InternalRel of () by ;
then the InternalRel of G meets the InternalRel of () ;
hence [x,y] in the InternalRel of () by Th12; :: thesis: verum
end;
suppose ( x = 1 & y = 3 ) ; :: thesis: [x,y] in the InternalRel of ()
hence [x,y] in the InternalRel of () by ; :: thesis: verum
end;
suppose ( x = 2 & y = 1 ) ; :: thesis: [x,y] in the InternalRel of ()
then [(f . 2),(f . 1)] in the InternalRel of G /\ the InternalRel of () by ;
then the InternalRel of G meets the InternalRel of () ;
hence [x,y] in the InternalRel of () by Th12; :: thesis: verum
end;
suppose A106: ( x = 2 & y = 2 ) ; :: thesis: [x,y] in the InternalRel of ()
then f . 2 in the carrier of G by ;
hence [x,y] in the InternalRel of () by ; :: thesis: verum
end;
suppose ( x = 2 & y = 3 ) ; :: thesis: [x,y] in the InternalRel of ()
then [(f . 2),(f . 3)] in the InternalRel of G /\ the InternalRel of () by ;
then the InternalRel of G meets the InternalRel of () ;
hence [x,y] in the InternalRel of () by Th12; :: thesis: verum
end;
suppose ( x = 3 & y = 1 ) ; :: thesis: [x,y] in the InternalRel of ()
hence [x,y] in the InternalRel of () by ; :: thesis: verum
end;
suppose ( x = 3 & y = 2 ) ; :: thesis: [x,y] in the InternalRel of ()
then [(f . 3),(f . 2)] in the InternalRel of G /\ the InternalRel of () by ;
then the InternalRel of G meets the InternalRel of () ;
hence [x,y] in the InternalRel of () by Th12; :: thesis: verum
end;
suppose A107: ( x = 3 & y = 3 ) ; :: thesis: [x,y] in the InternalRel of ()
then f . 3 in the carrier of G by ;
hence [x,y] in the InternalRel of () by ; :: thesis: verum
end;
end;
end;
reconsider f = f as Function of (),G by ;
reconsider h = f * g as Function of (),G ;
A108: ( g is V24() & g is monotone ) by ;
for x, y being Element of () holds
( [x,y] in the InternalRel of () iff [(h . x),(h . y)] in the InternalRel of G )
proof
let x, y be Element of (); :: thesis: ( [x,y] in the InternalRel of () iff [(h . x),(h . y)] in the InternalRel of G )
thus ( [x,y] in the InternalRel of () 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 () )
proof
assume [x,y] in the InternalRel of () ; :: thesis: [(h . x),(h . y)] in the InternalRel of G
then x <= y by ORDERS_2:def 5;
then g . x <= g . y by ;
then [(g . x),(g . y)] in the InternalRel of () 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 ()
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 () by A94;
then g . x <= g . y by ORDERS_2:def 5;
then x <= y by ;
hence [x,y] in the InternalRel of () by ORDERS_2:def 5; :: thesis: verum
end;
hence G embeds Necklace 4 by ; :: thesis: verum