let G be non empty symmetric irreflexive RelStr ; :: thesis: for a, b, c, d being Element of G
for Z being Subset of G st Z = {a,b,c,d} & a,b,c,d are_mutually_distinct & [a,b] in the InternalRel of G & [b,c] in the InternalRel of G & [c,d] in the InternalRel of G & not [a,c] in the InternalRel of G & not [a,d] in the InternalRel of G & not [b,d] in the InternalRel of G holds
subrelstr Z embeds Necklace 4
let a, b, c, d be Element of G; :: thesis: for Z being Subset of G st Z = {a,b,c,d} & a,b,c,d are_mutually_distinct & [a,b] in the InternalRel of G & [b,c] in the InternalRel of G & [c,d] in the InternalRel of G & not [a,c] in the InternalRel of G & not [a,d] in the InternalRel of G & not [b,d] in the InternalRel of G holds
subrelstr Z embeds Necklace 4
let Z be Subset of G; :: thesis: ( Z = {a,b,c,d} & a,b,c,d are_mutually_distinct & [a,b] in the InternalRel of G & [b,c] in the InternalRel of G & [c,d] in the InternalRel of G & not [a,c] in the InternalRel of G & not [a,d] in the InternalRel of G & not [b,d] in the InternalRel of G implies subrelstr Z embeds Necklace 4 )
assume that
A1: Z = {a,b,c,d} and
A2: a,b,c,d are_mutually_distinct and
A3: [a,b] in the InternalRel of G and
A4: [b,c] in the InternalRel of G and
A5: [c,d] in the InternalRel of G and
A6: not [a,c] in the InternalRel of G and
A7: not [a,d] in the InternalRel of G and
A8: not [b,d] in the InternalRel of G ; :: thesis: subrelstr Z embeds Necklace 4
set g = (0,1) --> (a,b);
set h = (2,3) --> (c,d);
set f = ((0,1) --> (a,b)) +* ((2,3) --> (c,d));
A9: rng ((2,3) --> (c,d)) = {c,d} by FUNCT_4:64;
A10: a <> b by A2, ZFMISC_1:def 6;
A11: rng (0 .--> a) misses rng (1 .--> b)
proof
assume rng (0 .--> a) meets rng (1 .--> b) ; :: thesis: contradiction
then consider x being object such that
A12: x in rng (0 .--> a) and
A13: x in rng (1 .--> b) by XBOOLE_0:3;
rng (0 .--> a) = {a} by FUNCOP_1:8;
then ( rng (1 .--> b) = {b} & x = a ) by A12, FUNCOP_1:8, TARSKI:def 1;
hence contradiction by A10, A13, TARSKI:def 1; :: thesis: verum
end;
set H = subrelstr Z;
set N4 = Necklace 4;
set IH = the InternalRel of (subrelstr Z);
set cH = the carrier of (subrelstr Z);
set IG = the InternalRel of G;
set X = {[a,a],[a,b],[b,a],[b,b],[a,c],[a,d],[b,c],[b,d]};
set Y = {[c,a],[c,b],[d,a],[d,b],[c,c],[c,d],[d,c],[d,d]};
A14: not the carrier of (subrelstr Z) is empty by A1, YELLOW_0:def 15;
A15: (2,3) --> (c,d) = (2 .--> c) +* (3 .--> d) by FUNCT_4:def 4;
A16: c <> d by A2, ZFMISC_1:def 6;
rng (2 .--> c) misses rng (3 .--> d)
proof
assume rng (2 .--> c) meets rng (3 .--> d) ; :: thesis: contradiction
then consider x being object such that
A17: x in rng (2 .--> c) and
A18: x in rng (3 .--> d) by XBOOLE_0:3;
rng (2 .--> c) = {c} by FUNCOP_1:8;
then ( rng (3 .--> d) = {d} & x = c ) by A17, FUNCOP_1:8, TARSKI:def 1;
hence contradiction by A16, A18, TARSKI:def 1; :: thesis: verum
end;
then A19: (2,3) --> (c,d) is one-to-one by A15, FUNCT_4:92;
A20: rng ((0,1) --> (a,b)) = {a,b} by FUNCT_4:64;
A21: rng ((0,1) --> (a,b)) misses rng ((2,3) --> (c,d))
proof
assume not rng ((0,1) --> (a,b)) misses rng ((2,3) --> (c,d)) ; :: thesis: contradiction
then consider x being object such that
A22: x in rng ((0,1) --> (a,b)) and
A23: x in rng ((2,3) --> (c,d)) by XBOOLE_0:3;
A24: ( x = c or x = d ) by A9, A23, TARSKI:def 2;
( x = a or x = b ) by A20, A22, TARSKI:def 2;
hence contradiction by A2, A24, ZFMISC_1:def 6; :: thesis: verum
end;
dom (((0,1) --> (a,b)) +* ((2,3) --> (c,d))) = (dom ((0,1) --> (a,b))) \/ (dom ((2,3) --> (c,d))) by FUNCT_4:def 1
.= {0,1} \/ (dom ((2,3) --> (c,d))) by FUNCT_4:62
.= {0,1} \/ {2,3} by FUNCT_4:62
.= {0,1,2,3} by ENUMSET1:5 ;
then A25: dom (((0,1) --> (a,b)) +* ((2,3) --> (c,d))) = the carrier of (Necklace 4) by NECKLACE:1, NECKLACE:20;
A26: dom ((0,1) --> (a,b)) misses dom ((2,3) --> (c,d))
proof
assume not dom ((0,1) --> (a,b)) misses dom ((2,3) --> (c,d)) ; :: thesis: contradiction
then consider x being object such that
A27: x in dom ((0,1) --> (a,b)) and
A28: x in dom ((2,3) --> (c,d)) by XBOOLE_0:3;
( x = 0 or x = 1 ) by A27, TARSKI:def 2;
hence contradiction by A28, TARSKI:def 2; :: thesis: verum
end;
then rng (((0,1) --> (a,b)) +* ((2,3) --> (c,d))) = (rng ((0,1) --> (a,b))) \/ (rng ((2,3) --> (c,d))) by NECKLACE:6;
then rng (((0,1) --> (a,b)) +* ((2,3) --> (c,d))) = {a,b,c,d} by A20, A9, ENUMSET1:5;
then A29: rng (((0,1) --> (a,b)) +* ((2,3) --> (c,d))) = the carrier of (subrelstr Z) by A1, YELLOW_0:def 15;
then reconsider f = ((0,1) --> (a,b)) +* ((2,3) --> (c,d)) as Function of (Necklace 4),(subrelstr Z) by A25, FUNCT_2:def 1, RELSET_1:4;
(0,1) --> (a,b) = (0 .--> a) +* (1 .--> b) by FUNCT_4:def 4;
then A30: (0,1) --> (a,b) is one-to-one by A11, FUNCT_4:92;
then A31: f is one-to-one by A19, A21, FUNCT_4:92;
A32: the InternalRel of (subrelstr Z) = {[a,b],[b,a],[b,c],[c,b],[c,d],[d,c]}
proof
thus the InternalRel of (subrelstr Z) c= {[a,b],[b,a],[b,c],[c,b],[c,d],[d,c]} :: according to XBOOLE_0:def 10 :: thesis: {[a,b],[b,a],[b,c],[c,b],[c,d],[d,c]} c= the InternalRel of (subrelstr Z)
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in the InternalRel of (subrelstr Z) or x in {[a,b],[b,a],[b,c],[c,b],[c,d],[d,c]} )
A33: the carrier of (subrelstr Z) = Z by YELLOW_0:def 15;
assume A34: x in the InternalRel of (subrelstr Z) ; :: thesis: x in {[a,b],[b,a],[b,c],[c,b],[c,d],[d,c]}
then A35: x in the InternalRel of G |_2 the carrier of (subrelstr Z) by YELLOW_0:def 14;
then A36: x in the InternalRel of G by XBOOLE_0:def 4;
x in [: the carrier of (subrelstr Z), the carrier of (subrelstr Z):] by A34;
then A37: x in {[a,a],[a,b],[b,a],[b,b],[a,c],[a,d],[b,c],[b,d]} \/ {[c,a],[c,b],[d,a],[d,b],[c,c],[c,d],[d,c],[d,d]} by A1, A33, Th3;
per cases ( x in {[a,a],[a,b],[b,a],[b,b],[a,c],[a,d],[b,c],[b,d]} or x in {[c,a],[c,b],[d,a],[d,b],[c,c],[c,d],[d,c],[d,d]} ) by A37, XBOOLE_0:def 3;
suppose A38: x in {[a,a],[a,b],[b,a],[b,b],[a,c],[a,d],[b,c],[b,d]} ; :: thesis: x in {[a,b],[b,a],[b,c],[c,b],[c,d],[d,c]}
thus x in {[a,b],[b,a],[b,c],[c,b],[c,d],[d,c]} :: thesis: verum
proof
per cases ( x = [a,a] or x = [a,b] or x = [b,a] or x = [b,b] or x = [a,c] or x = [a,d] or x = [b,c] or x = [b,d] ) by A38, ENUMSET1:def 6;
suppose A39: x = [a,a] ; :: thesis: x in {[a,b],[b,a],[b,c],[c,b],[c,d],[d,c]}
not [a,a] in the InternalRel of G by NECKLACE:def 5;
hence x in {[a,b],[b,a],[b,c],[c,b],[c,d],[d,c]} by A35, A39, XBOOLE_0:def 4; :: thesis: verum
end;
suppose x = [a,b] ; :: thesis: x in {[a,b],[b,a],[b,c],[c,b],[c,d],[d,c]}
hence x in {[a,b],[b,a],[b,c],[c,b],[c,d],[d,c]} by ENUMSET1:def 4; :: thesis: verum
end;
suppose x = [b,a] ; :: thesis: x in {[a,b],[b,a],[b,c],[c,b],[c,d],[d,c]}
hence x in {[a,b],[b,a],[b,c],[c,b],[c,d],[d,c]} by ENUMSET1:def 4; :: thesis: verum
end;
suppose A40: x = [b,b] ; :: thesis: x in {[a,b],[b,a],[b,c],[c,b],[c,d],[d,c]}
not [b,b] in the InternalRel of G by NECKLACE:def 5;
hence x in {[a,b],[b,a],[b,c],[c,b],[c,d],[d,c]} by A35, A40, XBOOLE_0:def 4; :: thesis: verum
end;
suppose x = [a,c] ; :: thesis: x in {[a,b],[b,a],[b,c],[c,b],[c,d],[d,c]}
hence x in {[a,b],[b,a],[b,c],[c,b],[c,d],[d,c]} by A6, A35, XBOOLE_0:def 4; :: thesis: verum
end;
suppose x = [a,d] ; :: thesis: x in {[a,b],[b,a],[b,c],[c,b],[c,d],[d,c]}
hence x in {[a,b],[b,a],[b,c],[c,b],[c,d],[d,c]} by A7, A35, XBOOLE_0:def 4; :: thesis: verum
end;
suppose x = [b,c] ; :: thesis: x in {[a,b],[b,a],[b,c],[c,b],[c,d],[d,c]}
hence x in {[a,b],[b,a],[b,c],[c,b],[c,d],[d,c]} by ENUMSET1:def 4; :: thesis: verum
end;
suppose x = [b,d] ; :: thesis: x in {[a,b],[b,a],[b,c],[c,b],[c,d],[d,c]}
hence x in {[a,b],[b,a],[b,c],[c,b],[c,d],[d,c]} by A8, A35, XBOOLE_0:def 4; :: thesis: verum
end;
end;
end;
end;
suppose A41: x in {[c,a],[c,b],[d,a],[d,b],[c,c],[c,d],[d,c],[d,d]} ; :: thesis: x in {[a,b],[b,a],[b,c],[c,b],[c,d],[d,c]}
A42: the InternalRel of G is_symmetric_in the carrier of G by NECKLACE:def 3;
thus x in {[a,b],[b,a],[b,c],[c,b],[c,d],[d,c]} :: thesis: verum
proof
per cases ( x = [c,a] or x = [c,b] or x = [d,a] or x = [d,b] or x = [c,c] or x = [c,d] or x = [d,c] or x = [d,d] ) by A41, ENUMSET1:def 6;
suppose x = [c,a] ; :: thesis: x in {[a,b],[b,a],[b,c],[c,b],[c,d],[d,c]}
hence x in {[a,b],[b,a],[b,c],[c,b],[c,d],[d,c]} by A6, A36, A42; :: thesis: verum
end;
suppose x = [c,b] ; :: thesis: x in {[a,b],[b,a],[b,c],[c,b],[c,d],[d,c]}
hence x in {[a,b],[b,a],[b,c],[c,b],[c,d],[d,c]} by ENUMSET1:def 4; :: thesis: verum
end;
suppose x = [d,a] ; :: thesis: x in {[a,b],[b,a],[b,c],[c,b],[c,d],[d,c]}
hence x in {[a,b],[b,a],[b,c],[c,b],[c,d],[d,c]} by A7, A36, A42; :: thesis: verum
end;
suppose x = [d,b] ; :: thesis: x in {[a,b],[b,a],[b,c],[c,b],[c,d],[d,c]}
hence x in {[a,b],[b,a],[b,c],[c,b],[c,d],[d,c]} by A8, A36, A42; :: thesis: verum
end;
suppose A43: x = [c,c] ; :: thesis: x in {[a,b],[b,a],[b,c],[c,b],[c,d],[d,c]}
not [c,c] in the InternalRel of G by NECKLACE:def 5;
hence x in {[a,b],[b,a],[b,c],[c,b],[c,d],[d,c]} by A35, A43, XBOOLE_0:def 4; :: thesis: verum
end;
suppose x = [c,d] ; :: thesis: x in {[a,b],[b,a],[b,c],[c,b],[c,d],[d,c]}
hence x in {[a,b],[b,a],[b,c],[c,b],[c,d],[d,c]} by ENUMSET1:def 4; :: thesis: verum
end;
suppose x = [d,c] ; :: thesis: x in {[a,b],[b,a],[b,c],[c,b],[c,d],[d,c]}
hence x in {[a,b],[b,a],[b,c],[c,b],[c,d],[d,c]} by ENUMSET1:def 4; :: thesis: verum
end;
suppose A44: x = [d,d] ; :: thesis: x in {[a,b],[b,a],[b,c],[c,b],[c,d],[d,c]}
not [d,d] in the InternalRel of G by NECKLACE:def 5;
hence x in {[a,b],[b,a],[b,c],[c,b],[c,d],[d,c]} by A35, A44, XBOOLE_0:def 4; :: thesis: verum
end;
end;
end;
end;
end;
end;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in {[a,b],[b,a],[b,c],[c,b],[c,d],[d,c]} or x in the InternalRel of (subrelstr Z) )
assume A45: x in {[a,b],[b,a],[b,c],[c,b],[c,d],[d,c]} ; :: thesis: x in the InternalRel of (subrelstr Z)
per cases ( x = [a,b] or x = [b,a] or x = [b,c] or x = [c,b] or x = [c,d] or x = [d,c] ) by A45, ENUMSET1:def 4;
end;
end;
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 (subrelstr Z) )
proof
let x, y be Element of (Necklace 4); :: thesis: ( [x,y] in the InternalRel of (Necklace 4) iff [(f . x),(f . y)] in the InternalRel of (subrelstr Z) )
thus ( [x,y] in the InternalRel of (Necklace 4) implies [(f . x),(f . y)] in the InternalRel of (subrelstr Z) ) :: thesis: ( [(f . x),(f . y)] in the InternalRel of (subrelstr Z) implies [x,y] in the InternalRel of (Necklace 4) )
proof
assume A61: [x,y] in the InternalRel of (Necklace 4) ; :: thesis: [(f . x),(f . y)] in the InternalRel of (subrelstr Z)
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 A61, ENUMSET1:def 4, NECKLA_2:2;
suppose A62: [x,y] = [0,1] ; :: thesis: [(f . x),(f . y)] in the InternalRel of (subrelstr Z)
then A63: y = 1 by XTUPLE_0:1;
then y in {0,1} by TARSKI:def 2;
then y in dom ((0,1) --> (a,b)) by FUNCT_4:62;
then A64: f . y = ((0,1) --> (a,b)) . 1 by A26, A63, FUNCT_4:16
.= b by FUNCT_4:63 ;
A65: x = 0 by A62, XTUPLE_0:1;
then x in {0,1} by TARSKI:def 2;
then x in dom ((0,1) --> (a,b)) by FUNCT_4:62;
then f . x = ((0,1) --> (a,b)) . 0 by A26, A65, FUNCT_4:16
.= a by FUNCT_4:63 ;
hence [(f . x),(f . y)] in the InternalRel of (subrelstr Z) by A32, A64, ENUMSET1:def 4; :: thesis: verum
end;
suppose A66: [x,y] = [1,0] ; :: thesis: [(f . x),(f . y)] in the InternalRel of (subrelstr Z)
then A67: y = 0 by XTUPLE_0:1;
then y in {0,1} by TARSKI:def 2;
then y in dom ((0,1) --> (a,b)) by FUNCT_4:62;
then A68: f . y = ((0,1) --> (a,b)) . 0 by A26, A67, FUNCT_4:16
.= a by FUNCT_4:63 ;
A69: x = 1 by A66, XTUPLE_0:1;
then x in {0,1} by TARSKI:def 2;
then x in dom ((0,1) --> (a,b)) by FUNCT_4:62;
then f . x = ((0,1) --> (a,b)) . 1 by A26, A69, FUNCT_4:16
.= b by FUNCT_4:63 ;
hence [(f . x),(f . y)] in the InternalRel of (subrelstr Z) by A32, A68, ENUMSET1:def 4; :: thesis: verum
end;
suppose A70: [x,y] = [1,2] ; :: thesis: [(f . x),(f . y)] in the InternalRel of (subrelstr Z)
then A71: x = 1 by XTUPLE_0:1;
then x in {0,1} by TARSKI:def 2;
then x in dom ((0,1) --> (a,b)) by FUNCT_4:62;
then A72: f . x = ((0,1) --> (a,b)) . 1 by A26, A71, FUNCT_4:16
.= b by FUNCT_4:63 ;
A73: y = 2 by A70, XTUPLE_0:1;
then y in {2,3} by TARSKI:def 2;
then A74: y in dom ((2,3) --> (c,d)) by FUNCT_4:62;
((0,1) --> (a,b)) +* ((2,3) --> (c,d)) = ((2,3) --> (c,d)) +* ((0,1) --> (a,b)) by A26, FUNCT_4:35;
then f . y = ((2,3) --> (c,d)) . 2 by A26, A73, A74, FUNCT_4:16
.= c by FUNCT_4:63 ;
hence [(f . x),(f . y)] in the InternalRel of (subrelstr Z) by A32, A72, ENUMSET1:def 4; :: thesis: verum
end;
suppose A75: [x,y] = [2,1] ; :: thesis: [(f . x),(f . y)] in the InternalRel of (subrelstr Z)
then A76: y = 1 by XTUPLE_0:1;
then y in {0,1} by TARSKI:def 2;
then y in dom ((0,1) --> (a,b)) by FUNCT_4:62;
then A77: f . y = ((0,1) --> (a,b)) . 1 by A26, A76, FUNCT_4:16
.= b by FUNCT_4:63 ;
A78: x = 2 by A75, XTUPLE_0:1;
then x in {2,3} by TARSKI:def 2;
then A79: x in dom ((2,3) --> (c,d)) by FUNCT_4:62;
((0,1) --> (a,b)) +* ((2,3) --> (c,d)) = ((2,3) --> (c,d)) +* ((0,1) --> (a,b)) by A26, FUNCT_4:35;
then f . x = ((2,3) --> (c,d)) . 2 by A26, A78, A79, FUNCT_4:16
.= c by FUNCT_4:63 ;
hence [(f . x),(f . y)] in the InternalRel of (subrelstr Z) by A32, A77, ENUMSET1:def 4; :: thesis: verum
end;
suppose A80: [x,y] = [2,3] ; :: thesis: [(f . x),(f . y)] in the InternalRel of (subrelstr Z)
A81: ((0,1) --> (a,b)) +* ((2,3) --> (c,d)) = ((2,3) --> (c,d)) +* ((0,1) --> (a,b)) by A26, FUNCT_4:35;
A82: y = 3 by A80, XTUPLE_0:1;
then y in {2,3} by TARSKI:def 2;
then y in dom ((2,3) --> (c,d)) by FUNCT_4:62;
then A83: f . y = ((2,3) --> (c,d)) . 3 by A26, A82, A81, FUNCT_4:16
.= d by FUNCT_4:63 ;
A84: x = 2 by A80, XTUPLE_0:1;
then x in {2,3} by TARSKI:def 2;
then x in dom ((2,3) --> (c,d)) by FUNCT_4:62;
then f . x = ((2,3) --> (c,d)) . 2 by A26, A84, A81, FUNCT_4:16
.= c by FUNCT_4:63 ;
hence [(f . x),(f . y)] in the InternalRel of (subrelstr Z) by A32, A83, ENUMSET1:def 4; :: thesis: verum
end;
suppose A85: [x,y] = [3,2] ; :: thesis: [(f . x),(f . y)] in the InternalRel of (subrelstr Z)
A86: ((0,1) --> (a,b)) +* ((2,3) --> (c,d)) = ((2,3) --> (c,d)) +* ((0,1) --> (a,b)) by A26, FUNCT_4:35;
A87: y = 2 by A85, XTUPLE_0:1;
then y in {3,2} by TARSKI:def 2;
then y in dom ((2,3) --> (c,d)) by FUNCT_4:62;
then A88: f . y = ((2,3) --> (c,d)) . 2 by A26, A87, A86, FUNCT_4:16
.= c by FUNCT_4:63 ;
A89: x = 3 by A85, XTUPLE_0:1;
then x in {3,2} by TARSKI:def 2;
then x in dom ((2,3) --> (c,d)) by FUNCT_4:62;
then f . x = ((2,3) --> (c,d)) . 3 by A26, A89, A86, FUNCT_4:16
.= d by FUNCT_4:63 ;
hence [(f . x),(f . y)] in the InternalRel of (subrelstr Z) by A32, A88, ENUMSET1:def 4; :: thesis: verum
end;
end;
end;
thus ( [(f . x),(f . y)] in the InternalRel of (subrelstr Z) implies [x,y] in the InternalRel of (Necklace 4) ) :: thesis: verum
proof
reconsider F = f " as Function of the carrier of (subrelstr Z), the carrier of (Necklace 4) by A29, A31, FUNCT_2:25;
A90: dom ((0,1) --> (a,b)) = {0,1} by FUNCT_4:62;
A91: rng ((0,1) --> (a,b)) = {a,b} by FUNCT_4:64;
then reconsider g = (0,1) --> (a,b) as Function of {0,1},{a,b} by A90, RELSET_1:4;
reconsider G = g " as Function of {a,b},{0,1} by A20, A30, FUNCT_2:25;
A92: dom ((2,3) --> (c,d)) = {2,3} by FUNCT_4:62;
A93: rng ((2,3) --> (c,d)) = {c,d} by FUNCT_4:64;
then reconsider h = (2,3) --> (c,d) as Function of {2,3},{c,d} by A92, RELSET_1:4;
reconsider Hh = h " as Function of {c,d},{2,3} by A9, A19, FUNCT_2:25;
A94: dom Hh = {c,d} by A19, A93, FUNCT_1:33;
A95: Hh = (c,d) --> (2,3) by A16, NECKLACE:10;
A96: F = G +* Hh by A26, A30, A19, A21, NECKLACE:7;
A97: G = (a,b) --> (0,1) by A10, NECKLACE:10;
A98: dom G = {a,b} by A30, A91, FUNCT_1:33;
then G +* Hh = Hh +* G by A20, A9, A21, A94, FUNCT_4:35;
then A99: F = Hh +* G by A26, A30, A19, A21, NECKLACE:7;
assume A100: [(f . x),(f . y)] in the InternalRel of (subrelstr Z) ; :: thesis: [x,y] in the InternalRel of (Necklace 4)
per cases ( [(f . x),(f . y)] = [a,b] or [(f . x),(f . y)] = [b,a] or [(f . x),(f . y)] = [b,c] or [(f . x),(f . y)] = [c,b] or [(f . x),(f . y)] = [c,d] or [(f . x),(f . y)] = [d,c] ) by A32, A100, ENUMSET1:def 4;
suppose A101: [(f . x),(f . y)] = [a,b] ; :: thesis: [x,y] in the InternalRel of (Necklace 4)
then A102: f . x = a by XTUPLE_0:1;
then f . x in {a,b} by TARSKI:def 2;
then F . (f . x) = G . a by A20, A9, A21, A98, A94, A96, A102, FUNCT_4:16
.= 0 by A10, A97, FUNCT_4:63 ;
then A103: x = 0 by A14, A31, FUNCT_2:26;
A104: f . y = b by A101, XTUPLE_0:1;
then f . y in dom G by A98, TARSKI:def 2;
then A105: F . (f . y) = G . b by A20, A9, A21, A98, A94, A96, A104, FUNCT_4:16
.= 1 by A97, FUNCT_4:63 ;
F . (f . y) = y by A14, A31, FUNCT_2:26;
hence [x,y] in the InternalRel of (Necklace 4) by A103, A105, ENUMSET1:def 4, NECKLA_2:2; :: thesis: verum
end;
suppose A106: [(f . x),(f . y)] = [b,a] ; :: thesis: [x,y] in the InternalRel of (Necklace 4)
then A107: f . y = a by XTUPLE_0:1;
then f . y in {a,b} by TARSKI:def 2;
then F . (f . y) = G . a by A20, A9, A21, A98, A94, A96, A107, FUNCT_4:16
.= 0 by A10, A97, FUNCT_4:63 ;
then A108: y = 0 by A14, A31, FUNCT_2:26;
A109: f . x = b by A106, XTUPLE_0:1;
then f . x in dom G by A98, TARSKI:def 2;
then A110: F . (f . x) = G . b by A20, A9, A21, A98, A94, A96, A109, FUNCT_4:16
.= 1 by A97, FUNCT_4:63 ;
F . (f . x) = x by A14, A31, FUNCT_2:26;
hence [x,y] in the InternalRel of (Necklace 4) by A108, A110, ENUMSET1:def 4, NECKLA_2:2; :: thesis: verum
end;
suppose A111: [(f . x),(f . y)] = [b,c] ; :: thesis: [x,y] in the InternalRel of (Necklace 4)
then A112: f . x = b by XTUPLE_0:1;
then f . x in dom G by A98, TARSKI:def 2;
then F . (f . x) = G . b by A20, A9, A21, A98, A94, A96, A112, FUNCT_4:16
.= 1 by A97, FUNCT_4:63 ;
then A113: x = 1 by A14, A31, FUNCT_2:26;
A114: f . y = c by A111, XTUPLE_0:1;
then f . y in dom Hh by A94, TARSKI:def 2;
then A115: F . (f . y) = Hh . c by A20, A9, A21, A98, A94, A99, A114, FUNCT_4:16
.= 2 by A16, A95, FUNCT_4:63 ;
F . (f . y) = y by A14, A31, FUNCT_2:26;
hence [x,y] in the InternalRel of (Necklace 4) by A113, A115, ENUMSET1:def 4, NECKLA_2:2; :: thesis: verum
end;
suppose A116: [(f . x),(f . y)] = [c,b] ; :: thesis: [x,y] in the InternalRel of (Necklace 4)
then A117: f . y = b by XTUPLE_0:1;
then f . y in dom G by A98, TARSKI:def 2;
then F . (f . y) = G . b by A20, A9, A21, A98, A94, A96, A117, FUNCT_4:16
.= 1 by A97, FUNCT_4:63 ;
then A118: y = 1 by A14, A31, FUNCT_2:26;
A119: f . x = c by A116, XTUPLE_0:1;
then f . x in dom Hh by A94, TARSKI:def 2;
then A120: F . (f . x) = Hh . c by A20, A9, A21, A98, A94, A99, A119, FUNCT_4:16
.= 2 by A16, A95, FUNCT_4:63 ;
F . (f . x) = x by A14, A31, FUNCT_2:26;
hence [x,y] in the InternalRel of (Necklace 4) by A118, A120, ENUMSET1:def 4, NECKLA_2:2; :: thesis: verum
end;
suppose A121: [(f . x),(f . y)] = [c,d] ; :: thesis: [x,y] in the InternalRel of (Necklace 4)
then A122: f . x = c by XTUPLE_0:1;
then f . x in {c,d} by TARSKI:def 2;
then F . (f . x) = Hh . c by A20, A9, A21, A98, A94, A99, A122, FUNCT_4:16
.= 2 by A16, A95, FUNCT_4:63 ;
then A123: x = 2 by A14, A31, FUNCT_2:26;
A124: f . y = d by A121, XTUPLE_0:1;
then f . y in dom Hh by A94, TARSKI:def 2;
then A125: F . (f . y) = Hh . d by A20, A9, A21, A98, A94, A99, A124, FUNCT_4:16
.= 3 by A95, FUNCT_4:63 ;
F . (f . y) = y by A14, A31, FUNCT_2:26;
hence [x,y] in the InternalRel of (Necklace 4) by A123, A125, ENUMSET1:def 4, NECKLA_2:2; :: thesis: verum
end;
suppose A126: [(f . x),(f . y)] = [d,c] ; :: thesis: [x,y] in the InternalRel of (Necklace 4)
then A127: f . y = c by XTUPLE_0:1;
then f . y in {c,d} by TARSKI:def 2;
then F . (f . y) = Hh . c by A20, A9, A21, A98, A94, A99, A127, FUNCT_4:16
.= 2 by A16, A95, FUNCT_4:63 ;
then A128: y = 2 by A14, A31, FUNCT_2:26;
A129: f . x = d by A126, XTUPLE_0:1;
then f . x in dom Hh by A94, TARSKI:def 2;
then A130: F . (f . x) = Hh . d by A20, A9, A21, A98, A94, A99, A129, FUNCT_4:16
.= 3 by A95, FUNCT_4:63 ;
F . (f . x) = x by A14, A31, FUNCT_2:26;
hence [x,y] in the InternalRel of (Necklace 4) by A128, A130, ENUMSET1:def 4, NECKLA_2:2; :: thesis: verum
end;
end;
end;
end;
hence subrelstr Z embeds Necklace 4 by A31; :: thesis: verum