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_different & [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_different & [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_different & [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_different 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 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]};
A9: 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 set ; :: 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]} )
assume x in the InternalRel of (subrelstr Z) ; :: thesis: x in {[a,b],[b,a],[b,c],[c,b],[c,d],[d,c]}
then A10: x in the InternalRel of G |_2 the carrier of (subrelstr Z) by YELLOW_0:def 14;
then A11: ( x in the InternalRel of G & x in [:the carrier of (subrelstr Z),the carrier of (subrelstr Z):] ) by XBOOLE_0:def 4;
the carrier of (subrelstr Z) = Z by YELLOW_0:def 15;
then A12: 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, A11, 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 A12, XBOOLE_0:def 3;
suppose A13: 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 A13, ENUMSET1:def 6;
suppose A14: 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 6;
hence x in {[a,b],[b,a],[b,c],[c,b],[c,d],[d,c]} by A10, A14, 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 A15: 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 6;
hence x in {[a,b],[b,a],[b,c],[c,b],[c,d],[d,c]} by A10, A15, 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, A10, 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, A10, 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, A10, XBOOLE_0:def 4; :: thesis: verum
end;
end;
end;
end;
suppose A16: 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]}
A17: the InternalRel of G is_symmetric_in the carrier of G by NECKLACE:def 4;
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 A16, 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, A11, A17, RELAT_2:def 3; :: 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, A11, A17, RELAT_2:def 3; :: 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, A11, A17, RELAT_2:def 3; :: thesis: verum
end;
suppose A18: 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 6;
hence x in {[a,b],[b,a],[b,c],[c,b],[c,d],[d,c]} by A10, A18, 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 A19: 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 6;
hence x in {[a,b],[b,a],[b,c],[c,b],[c,d],[d,c]} by A10, A19, XBOOLE_0:def 4; :: thesis: verum
end;
end;
end;
end;
end;
end;
let x be set ; :: 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 A20: 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 A20, ENUMSET1:def 4;
end;
end;
A30: ( a <> b & a <> c & a <> d & b <> c & b <> d & c <> d ) by A2, ZFMISC_1:def 6;
set g = 0 ,1 --> a,b;
set h = 2,3 --> c,d;
set f = (0 ,1 --> a,b) +* (2,3 --> c,d);
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:65
.= {0 ,1} \/ {2,3} by FUNCT_4:65
.= {0 ,1,2,3} by ENUMSET1:45 ;
then A31: dom ((0 ,1 --> a,b) +* (2,3 --> c,d)) = the carrier of (Necklace 4) by NECKLACE:2, NECKLACE:21;
A32: rng (0 ,1 --> a,b) = {a,b} by FUNCT_4:67;
A33: rng (2,3 --> c,d) = {c,d} by FUNCT_4:67;
A34: not the carrier of (subrelstr Z) is empty by A1, YELLOW_0:def 15;
A35: 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 set such that
A36: ( x in dom (0 ,1 --> a,b) & x in dom (2,3 --> c,d) ) by XBOOLE_0:3;
( ( x = 0 or x = 1 ) & ( x = 2 or x = 3 ) ) by A36, TARSKI:def 2;
hence contradiction ; :: thesis: verum
end;
A37: rng ((0 ,1 --> a,b) +* (2,3 --> c,d)) = the carrier of (subrelstr Z)
proof
rng ((0 ,1 --> a,b) +* (2,3 --> c,d)) = (rng (0 ,1 --> a,b)) \/ (rng (2,3 --> c,d)) by A35, NECKLACE:7;
then rng ((0 ,1 --> a,b) +* (2,3 --> c,d)) = {a,b,c,d} by A32, A33, ENUMSET1:45;
hence rng ((0 ,1 --> a,b) +* (2,3 --> c,d)) = the carrier of (subrelstr Z) by A1, YELLOW_0:def 15; :: thesis: verum
end;
then reconsider f = (0 ,1 --> a,b) +* (2,3 --> c,d) as Function of (Necklace 4),(subrelstr Z) by A31, FUNCT_2:def 1, RELSET_1:11;
A38: 0 ,1 --> a,b is one-to-one
proof
A39: 0 ,1 --> a,b = (0 .--> a) +* (1 .--> b) by FUNCT_4:def 4;
rng (0 .--> a) misses rng (1 .--> b)
proof
assume rng (0 .--> a) meets rng (1 .--> b) ; :: thesis: contradiction
then consider x being set such that
A40: ( x in rng (0 .--> a) & x in rng (1 .--> b) ) by XBOOLE_0:3;
A41: rng (0 .--> a) = {a} by FUNCOP_1:14;
A42: rng (1 .--> b) = {b} by FUNCOP_1:14;
x = a by A40, A41, TARSKI:def 1;
hence contradiction by A30, A40, A42, TARSKI:def 1; :: thesis: verum
end;
hence 0 ,1 --> a,b is one-to-one by A39, FUNCT_4:98; :: thesis: verum
end;
A43: 2,3 --> c,d is one-to-one
proof
A44: 2,3 --> c,d = (2 .--> c) +* (3 .--> d) by FUNCT_4:def 4;
rng (2 .--> c) misses rng (3 .--> d)
proof
assume rng (2 .--> c) meets rng (3 .--> d) ; :: thesis: contradiction
then consider x being set such that
A45: ( x in rng (2 .--> c) & x in rng (3 .--> d) ) by XBOOLE_0:3;
A46: rng (2 .--> c) = {c} by FUNCOP_1:14;
A47: rng (3 .--> d) = {d} by FUNCOP_1:14;
x = c by A45, A46, TARSKI:def 1;
hence contradiction by A30, A45, A47, TARSKI:def 1; :: thesis: verum
end;
hence 2,3 --> c,d is one-to-one by A44, FUNCT_4:98; :: thesis: verum
end;
A48: 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 set such that
A49: ( x in rng (0 ,1 --> a,b) & x in rng (2,3 --> c,d) ) by XBOOLE_0:3;
( ( x = a or x = b ) & ( x = c or x = d ) ) by A32, A33, A49, TARSKI:def 2;
hence contradiction by A2, ZFMISC_1:def 6; :: thesis: verum
end;
then A50: f is one-to-one by A38, A43, FUNCT_4:98;
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 A51: [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 A51, ENUMSET1:def 4, NECKLA_2:2;
suppose [x,y] = [0 ,1] ; :: thesis: [(f . x),(f . y)] in the InternalRel of (subrelstr Z)
then A52: ( x = 0 & y = 1 ) by ZFMISC_1:33;
then ( x in {0 ,1} & y in {0 ,1} ) by TARSKI:def 2;
then A53: ( x in dom (0 ,1 --> a,b) & y in dom (0 ,1 --> a,b) ) by FUNCT_4:65;
then A54: f . x = (0 ,1 --> a,b) . 0 by A35, A52, FUNCT_4:17
.= a by FUNCT_4:66 ;
f . y = (0 ,1 --> a,b) . 1 by A35, A52, A53, FUNCT_4:17
.= b by FUNCT_4:66 ;
hence [(f . x),(f . y)] in the InternalRel of (subrelstr Z) by A9, A54, ENUMSET1:def 4; :: thesis: verum
end;
suppose [x,y] = [1,0 ] ; :: thesis: [(f . x),(f . y)] in the InternalRel of (subrelstr Z)
then A55: ( x = 1 & y = 0 ) by ZFMISC_1:33;
then ( x in {0 ,1} & y in {0 ,1} ) by TARSKI:def 2;
then A56: ( x in dom (0 ,1 --> a,b) & y in dom (0 ,1 --> a,b) ) by FUNCT_4:65;
then A57: f . x = (0 ,1 --> a,b) . 1 by A35, A55, FUNCT_4:17
.= b by FUNCT_4:66 ;
f . y = (0 ,1 --> a,b) . 0 by A35, A55, A56, FUNCT_4:17
.= a by FUNCT_4:66 ;
hence [(f . x),(f . y)] in the InternalRel of (subrelstr Z) by A9, A57, ENUMSET1:def 4; :: thesis: verum
end;
suppose [x,y] = [1,2] ; :: thesis: [(f . x),(f . y)] in the InternalRel of (subrelstr Z)
then A58: ( x = 1 & y = 2 ) by ZFMISC_1:33;
then ( x in {0 ,1} & y in {2,3} ) by TARSKI:def 2;
then A59: ( x in dom (0 ,1 --> a,b) & y in dom (2,3 --> c,d) ) by FUNCT_4:65;
then A60: f . x = (0 ,1 --> a,b) . 1 by A35, A58, FUNCT_4:17
.= b by FUNCT_4:66 ;
(0 ,1 --> a,b) +* (2,3 --> c,d) = (2,3 --> c,d) +* (0 ,1 --> a,b) by A35, FUNCT_4:36;
then f . y = (2,3 --> c,d) . 2 by A35, A58, A59, FUNCT_4:17
.= c by FUNCT_4:66 ;
hence [(f . x),(f . y)] in the InternalRel of (subrelstr Z) by A9, A60, ENUMSET1:def 4; :: thesis: verum
end;
suppose [x,y] = [2,1] ; :: thesis: [(f . x),(f . y)] in the InternalRel of (subrelstr Z)
then A61: ( x = 2 & y = 1 ) by ZFMISC_1:33;
then ( x in {2,3} & y in {0 ,1} ) by TARSKI:def 2;
then A62: ( x in dom (2,3 --> c,d) & y in dom (0 ,1 --> a,b) ) by FUNCT_4:65;
then A63: f . y = (0 ,1 --> a,b) . 1 by A35, A61, FUNCT_4:17
.= b by FUNCT_4:66 ;
(0 ,1 --> a,b) +* (2,3 --> c,d) = (2,3 --> c,d) +* (0 ,1 --> a,b) by A35, FUNCT_4:36;
then f . x = (2,3 --> c,d) . 2 by A35, A61, A62, FUNCT_4:17
.= c by FUNCT_4:66 ;
hence [(f . x),(f . y)] in the InternalRel of (subrelstr Z) by A9, A63, ENUMSET1:def 4; :: thesis: verum
end;
suppose [x,y] = [2,3] ; :: thesis: [(f . x),(f . y)] in the InternalRel of (subrelstr Z)
then A64: ( x = 2 & y = 3 ) by ZFMISC_1:33;
then ( x in {2,3} & y in {2,3} ) by TARSKI:def 2;
then A65: ( x in dom (2,3 --> c,d) & y in dom (2,3 --> c,d) ) by FUNCT_4:65;
A66: (0 ,1 --> a,b) +* (2,3 --> c,d) = (2,3 --> c,d) +* (0 ,1 --> a,b) by A35, FUNCT_4:36;
then A67: f . x = (2,3 --> c,d) . 2 by A35, A64, A65, FUNCT_4:17
.= c by FUNCT_4:66 ;
f . y = (2,3 --> c,d) . 3 by A35, A64, A65, A66, FUNCT_4:17
.= d by FUNCT_4:66 ;
hence [(f . x),(f . y)] in the InternalRel of (subrelstr Z) by A9, A67, ENUMSET1:def 4; :: thesis: verum
end;
suppose [x,y] = [3,2] ; :: thesis: [(f . x),(f . y)] in the InternalRel of (subrelstr Z)
then A68: ( x = 3 & y = 2 ) by ZFMISC_1:33;
then ( x in {3,2} & y in {3,2} ) by TARSKI:def 2;
then A69: ( x in dom (2,3 --> c,d) & y in dom (2,3 --> c,d) ) by FUNCT_4:65;
A70: (0 ,1 --> a,b) +* (2,3 --> c,d) = (2,3 --> c,d) +* (0 ,1 --> a,b) by A35, FUNCT_4:36;
then A71: f . x = (2,3 --> c,d) . 3 by A35, A68, A69, FUNCT_4:17
.= d by FUNCT_4:66 ;
f . y = (2,3 --> c,d) . 2 by A35, A68, A69, A70, FUNCT_4:17
.= c by FUNCT_4:66 ;
hence [(f . x),(f . y)] in the InternalRel of (subrelstr Z) by A9, A71, 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
assume A72: [(f . x),(f . y)] in the InternalRel of (subrelstr Z) ; :: thesis: [x,y] in the InternalRel of (Necklace 4)
A73: ( dom (0 ,1 --> a,b) = {0 ,1} & rng (0 ,1 --> a,b) = {a,b} ) by FUNCT_4:65, FUNCT_4:67;
then reconsider g = 0 ,1 --> a,b as Function of {0 ,1},{a,b} by FUNCT_2:def 1, RELSET_1:11;
reconsider G = g " as Function of {a,b},{0 ,1} by A32, A38, FUNCT_2:31;
A74: ( dom (2,3 --> c,d) = {2,3} & rng (2,3 --> c,d) = {c,d} ) by FUNCT_4:65, FUNCT_4:67;
then reconsider h = 2,3 --> c,d as Function of {2,3},{c,d} by FUNCT_2:def 1, RELSET_1:11;
reconsider Hh = h " as Function of {c,d},{2,3} by A33, A43, FUNCT_2:31;
reconsider F = f " as Function of the carrier of (subrelstr Z),the carrier of (Necklace 4) by A37, A50, FUNCT_2:31;
A75: ( dom G = {a,b} & rng G = {0 ,1} ) by A38, A73, FUNCT_1:55;
A76: ( dom Hh = {c,d} & rng Hh = {2,3} ) by A43, A74, FUNCT_1:55;
then G +* Hh = Hh +* G by A32, A33, A48, A75, FUNCT_4:36;
then A77: ( F = G +* Hh & F = Hh +* G ) by A35, A38, A43, A48, NECKLACE:8;
A78: ( G = a,b --> 0 ,1 & Hh = c,d --> 2,3 ) by A30, NECKLACE:11;
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 A9, A72, ENUMSET1:def 4;
suppose [(f . x),(f . y)] = [a,b] ; :: thesis: [x,y] in the InternalRel of (Necklace 4)
then A79: ( f . x = a & f . y = b ) by ZFMISC_1:33;
then A80: ( f . x in {a,b} & f . y in {a,b} ) by TARSKI:def 2;
A81: ( f . x in dom G & f . y in dom G ) by A75, A79, TARSKI:def 2;
F . (f . x) = G . a by A32, A33, A48, A75, A76, A77, A79, A80, FUNCT_4:17
.= 0 by A30, A78, FUNCT_4:66 ;
then A82: x = 0 by A34, A50, FUNCT_2:32;
A83: F . (f . y) = G . b by A32, A33, A48, A75, A76, A77, A79, A81, FUNCT_4:17
.= 1 by A78, FUNCT_4:66 ;
F . (f . y) = y by A34, A50, FUNCT_2:32;
hence [x,y] in the InternalRel of (Necklace 4) by A82, A83, ENUMSET1:def 4, NECKLA_2:2; :: thesis: verum
end;
suppose [(f . x),(f . y)] = [b,a] ; :: thesis: [x,y] in the InternalRel of (Necklace 4)
then A84: ( f . x = b & f . y = a ) by ZFMISC_1:33;
then A85: ( f . x in {a,b} & f . y in {a,b} ) by TARSKI:def 2;
A86: ( f . x in dom G & f . y in dom G ) by A75, A84, TARSKI:def 2;
F . (f . y) = G . a by A32, A33, A48, A75, A76, A77, A84, A85, FUNCT_4:17
.= 0 by A30, A78, FUNCT_4:66 ;
then A87: y = 0 by A34, A50, FUNCT_2:32;
A88: F . (f . x) = G . b by A32, A33, A48, A75, A76, A77, A84, A86, FUNCT_4:17
.= 1 by A78, FUNCT_4:66 ;
F . (f . x) = x by A34, A50, FUNCT_2:32;
hence [x,y] in the InternalRel of (Necklace 4) by A87, A88, ENUMSET1:def 4, NECKLA_2:2; :: thesis: verum
end;
suppose [(f . x),(f . y)] = [b,c] ; :: thesis: [x,y] in the InternalRel of (Necklace 4)
then A89: ( f . x = b & f . y = c ) by ZFMISC_1:33;
then A90: ( f . x in dom G & f . y in dom Hh ) by A75, A76, TARSKI:def 2;
then F . (f . x) = G . b by A32, A33, A48, A75, A76, A77, A89, FUNCT_4:17
.= 1 by A78, FUNCT_4:66 ;
then A91: x = 1 by A34, A50, FUNCT_2:32;
A92: F . (f . y) = Hh . c by A32, A33, A48, A75, A76, A77, A89, A90, FUNCT_4:17
.= 2 by A30, A78, FUNCT_4:66 ;
F . (f . y) = y by A34, A50, FUNCT_2:32;
hence [x,y] in the InternalRel of (Necklace 4) by A91, A92, ENUMSET1:def 4, NECKLA_2:2; :: thesis: verum
end;
suppose [(f . x),(f . y)] = [c,b] ; :: thesis: [x,y] in the InternalRel of (Necklace 4)
then A93: ( f . x = c & f . y = b ) by ZFMISC_1:33;
then A94: ( f . x in dom Hh & f . y in dom G ) by A75, A76, TARSKI:def 2;
then F . (f . y) = G . b by A32, A33, A48, A75, A76, A77, A93, FUNCT_4:17
.= 1 by A78, FUNCT_4:66 ;
then A95: y = 1 by A34, A50, FUNCT_2:32;
A96: F . (f . x) = Hh . c by A32, A33, A48, A75, A76, A77, A93, A94, FUNCT_4:17
.= 2 by A30, A78, FUNCT_4:66 ;
F . (f . x) = x by A34, A50, FUNCT_2:32;
hence [x,y] in the InternalRel of (Necklace 4) by A95, A96, ENUMSET1:def 4, NECKLA_2:2; :: thesis: verum
end;
suppose [(f . x),(f . y)] = [c,d] ; :: thesis: [x,y] in the InternalRel of (Necklace 4)
then A97: ( f . x = c & f . y = d ) by ZFMISC_1:33;
then A98: ( f . x in {c,d} & f . y in {c,d} ) by TARSKI:def 2;
A99: ( f . x in dom Hh & f . y in dom Hh ) by A76, A97, TARSKI:def 2;
F . (f . x) = Hh . c by A32, A33, A48, A75, A76, A77, A97, A98, FUNCT_4:17
.= 2 by A30, A78, FUNCT_4:66 ;
then A100: x = 2 by A34, A50, FUNCT_2:32;
A101: F . (f . y) = Hh . d by A32, A33, A48, A75, A76, A77, A97, A99, FUNCT_4:17
.= 3 by A78, FUNCT_4:66 ;
F . (f . y) = y by A34, A50, FUNCT_2:32;
hence [x,y] in the InternalRel of (Necklace 4) by A100, A101, ENUMSET1:def 4, NECKLA_2:2; :: thesis: verum
end;
suppose [(f . x),(f . y)] = [d,c] ; :: thesis: [x,y] in the InternalRel of (Necklace 4)
then A102: ( f . x = d & f . y = c ) by ZFMISC_1:33;
then A103: ( f . x in {c,d} & f . y in {c,d} ) by TARSKI:def 2;
A104: ( f . x in dom Hh & f . y in dom Hh ) by A76, A102, TARSKI:def 2;
F . (f . y) = Hh . c by A32, A33, A48, A75, A76, A77, A102, A103, FUNCT_4:17
.= 2 by A30, A78, FUNCT_4:66 ;
then A105: y = 2 by A34, A50, FUNCT_2:32;
A106: F . (f . x) = Hh . d by A32, A33, A48, A75, A76, A77, A102, A104, FUNCT_4:17
.= 3 by A78, FUNCT_4:66 ;
F . (f . x) = x by A34, A50, FUNCT_2:32;
hence [x,y] in the InternalRel of (Necklace 4) by A105, A106, ENUMSET1:def 4, NECKLA_2:2; :: thesis: verum
end;
end;
end;
end;
hence subrelstr Z embeds Necklace 4 by A50, NECKLACE:def 2; :: thesis: verum