gpgprismgr4cycllem7

Description: Lemma 7 for gpgprismgr4cycl0 : the cycle <. P , F >. is proper, i.e., it has no overlapping vertices, except the first and the last one. (Contributed by AV, 1-Nov-2025)

		Ref	Expression
	Hypothesis	gpgprismgr4cycl.p	$⊢ P = ⟨“ ⟨0, 0⟩ ⟨0, 1⟩ ⟨1, 1⟩ ⟨1, 0⟩ ⟨0, 0⟩ ”⟩$
	Assertion	gpgprismgr4cycllem7	$⊢ (X \in (0 ..^\|P\|) \land Y \in (1 ..^4)) \to (X \neq Y \to P (X) \neq P (Y))$

Proof

Step	Hyp	Ref	Expression
1		gpgprismgr4cycl.p	$⊢ P = ⟨“ ⟨0, 0⟩ ⟨0, 1⟩ ⟨1, 1⟩ ⟨1, 0⟩ ⟨0, 0⟩ ”⟩$
2	1	gpgprismgr4cycllem4	$⊢ \|P\| = 5$
3		df-5	$⊢ 5 = 4 + 1$
4	2 3	eqtri	$⊢ \|P\| = 4 + 1$
5	4	oveq2i	$⊢ (0 ..^\|P\|) = (0 ..^4 + 1)$
6		4nn0	$⊢ 4 \in ℕ_{0}$
7		elnn0uz	$⊢ 4 \in ℕ_{0} \leftrightarrow 4 \in ℤ_{\geq 0}$
8	6 7	mpbi	$⊢ 4 \in ℤ_{\geq 0}$
9		fzosplitsn	$⊢ 4 \in ℤ_{\geq 0} \to (0 ..^4 + 1) = (0 ..^4) \cup \{4\}$
10	8 9	ax-mp	$⊢ (0 ..^4 + 1) = (0 ..^4) \cup \{4\}$
11		fzo0to42pr	$⊢ (0 ..^4) = \{0, 1\} \cup \{2, 3\}$
12	11	uneq1i	$⊢ (0 ..^4) \cup \{4\} = (\{0, 1\} \cup \{2, 3\}) \cup \{4\}$
13	5 10 12	3eqtri	$⊢ (0 ..^\|P\|) = (\{0, 1\} \cup \{2, 3\}) \cup \{4\}$
14	13	eleq2i	$⊢ X \in (0 ..^\|P\|) \leftrightarrow X \in ((\{0, 1\} \cup \{2, 3\}) \cup \{4\})$
15		fzo1to4tp	$⊢ (1 ..^4) = \{1, 2, 3\}$
16	15	eleq2i	$⊢ Y \in (1 ..^4) \leftrightarrow Y \in \{1, 2, 3\}$
17		elun	$⊢ X \in ((\{0, 1\} \cup \{2, 3\}) \cup \{4\}) \leftrightarrow (X \in (\{0, 1\} \cup \{2, 3\}) \lor X \in \{4\})$
18		elun	$⊢ X \in (\{0, 1\} \cup \{2, 3\}) \leftrightarrow (X \in \{0, 1\} \lor X \in \{2, 3\})$
19	18	orbi1i	$⊢ (X \in (\{0, 1\} \cup \{2, 3\}) \lor X \in \{4\}) \leftrightarrow ((X \in \{0, 1\} \lor X \in \{2, 3\}) \lor X \in \{4\})$
20	17 19	bitri	$⊢ X \in ((\{0, 1\} \cup \{2, 3\}) \cup \{4\}) \leftrightarrow ((X \in \{0, 1\} \lor X \in \{2, 3\}) \lor X \in \{4\})$
21		elpri	$⊢ X \in \{0, 1\} \to (X = 0 \lor X = 1)$
22		0ne1	$⊢ 0 \neq 1$
23	22	olci	$⊢ (0 \neq 0 \lor 0 \neq 1)$
24		c0ex	$⊢ 0 \in V$
25	24 24	opthne	$⊢ ⟨0, 0⟩ \neq ⟨0, 1⟩ \leftrightarrow (0 \neq 0 \lor 0 \neq 1)$
26	23 25	mpbir	$⊢ ⟨0, 0⟩ \neq ⟨0, 1⟩$
27	1	fveq1i	$⊢ P (0) = ⟨“ ⟨0, 0⟩ ⟨0, 1⟩ ⟨1, 1⟩ ⟨1, 0⟩ ⟨0, 0⟩ ”⟩ (0)$
28		opex	$⊢ ⟨0, 0⟩ \in V$
29		df-s5	$⊢ ⟨“ ⟨0, 0⟩ ⟨0, 1⟩ ⟨1, 1⟩ ⟨1, 0⟩ ⟨0, 0⟩ ”⟩ = ⟨“ ⟨0, 0⟩ ⟨0, 1⟩ ⟨1, 1⟩ ⟨1, 0⟩ ”⟩ ++ ⟨“ ⟨0, 0⟩ ”⟩$
30		s4cli	$⊢ ⟨“ ⟨0, 0⟩ ⟨0, 1⟩ ⟨1, 1⟩ ⟨1, 0⟩ ”⟩ \in Word V$
31		s4len	$⊢ \|⟨“ ⟨0, 0⟩ ⟨0, 1⟩ ⟨1, 1⟩ ⟨1, 0⟩ ”⟩\| = 4$
32		s4fv0	$⊢ ⟨0, 0⟩ \in V \to ⟨“ ⟨0, 0⟩ ⟨0, 1⟩ ⟨1, 1⟩ ⟨1, 0⟩ ”⟩ (0) = ⟨0, 0⟩$
33		0nn0	$⊢ 0 \in ℕ_{0}$
34		4pos	$⊢ 0 < 4$
35	29 30 31 32 33 34	cats1fv	$⊢ ⟨0, 0⟩ \in V \to ⟨“ ⟨0, 0⟩ ⟨0, 1⟩ ⟨1, 1⟩ ⟨1, 0⟩ ⟨0, 0⟩ ”⟩ (0) = ⟨0, 0⟩$
36	28 35	ax-mp	$⊢ ⟨“ ⟨0, 0⟩ ⟨0, 1⟩ ⟨1, 1⟩ ⟨1, 0⟩ ⟨0, 0⟩ ”⟩ (0) = ⟨0, 0⟩$
37	27 36	eqtri	$⊢ P (0) = ⟨0, 0⟩$
38	1	fveq1i	$⊢ P (1) = ⟨“ ⟨0, 0⟩ ⟨0, 1⟩ ⟨1, 1⟩ ⟨1, 0⟩ ⟨0, 0⟩ ”⟩ (1)$
39		opex	$⊢ ⟨0, 1⟩ \in V$
40		s4fv1	$⊢ ⟨0, 1⟩ \in V \to ⟨“ ⟨0, 0⟩ ⟨0, 1⟩ ⟨1, 1⟩ ⟨1, 0⟩ ”⟩ (1) = ⟨0, 1⟩$
41		1nn0	$⊢ 1 \in ℕ_{0}$
42		1lt4	$⊢ 1 < 4$
43	29 30 31 40 41 42	cats1fv	$⊢ ⟨0, 1⟩ \in V \to ⟨“ ⟨0, 0⟩ ⟨0, 1⟩ ⟨1, 1⟩ ⟨1, 0⟩ ⟨0, 0⟩ ”⟩ (1) = ⟨0, 1⟩$
44	39 43	ax-mp	$⊢ ⟨“ ⟨0, 0⟩ ⟨0, 1⟩ ⟨1, 1⟩ ⟨1, 0⟩ ⟨0, 0⟩ ”⟩ (1) = ⟨0, 1⟩$
45	38 44	eqtri	$⊢ P (1) = ⟨0, 1⟩$
46	37 45	neeq12i	$⊢ P (0) \neq P (1) \leftrightarrow ⟨0, 0⟩ \neq ⟨0, 1⟩$
47	26 46	mpbir	$⊢ P (0) \neq P (1)$
48	47	a1i	$⊢ (Y = 1 \land X = 0) \to P (0) \neq P (1)$
49		fveq2	$⊢ X = 0 \to P (X) = P (0)$
50	49	adantl	$⊢ (Y = 1 \land X = 0) \to P (X) = P (0)$
51		fveq2	$⊢ Y = 1 \to P (Y) = P (1)$
52	51	adantr	$⊢ (Y = 1 \land X = 0) \to P (Y) = P (1)$
53	48 50 52	3netr4d	$⊢ (Y = 1 \land X = 0) \to P (X) \neq P (Y)$
54	53	a1d	$⊢ (Y = 1 \land X = 0) \to (X \neq Y \to P (X) \neq P (Y))$
55	54	ex	$⊢ Y = 1 \to (X = 0 \to (X \neq Y \to P (X) \neq P (Y)))$
56	22	orci	$⊢ (0 \neq 1 \lor 0 \neq 1)$
57	24 24	opthne	$⊢ ⟨0, 0⟩ \neq ⟨1, 1⟩ \leftrightarrow (0 \neq 1 \lor 0 \neq 1)$
58	56 57	mpbir	$⊢ ⟨0, 0⟩ \neq ⟨1, 1⟩$
59	1	fveq1i	$⊢ P (2) = ⟨“ ⟨0, 0⟩ ⟨0, 1⟩ ⟨1, 1⟩ ⟨1, 0⟩ ⟨0, 0⟩ ”⟩ (2)$
60		opex	$⊢ ⟨1, 1⟩ \in V$
61		s4fv2	$⊢ ⟨1, 1⟩ \in V \to ⟨“ ⟨0, 0⟩ ⟨0, 1⟩ ⟨1, 1⟩ ⟨1, 0⟩ ”⟩ (2) = ⟨1, 1⟩$
62		2nn0	$⊢ 2 \in ℕ_{0}$
63		2lt4	$⊢ 2 < 4$
64	29 30 31 61 62 63	cats1fv	$⊢ ⟨1, 1⟩ \in V \to ⟨“ ⟨0, 0⟩ ⟨0, 1⟩ ⟨1, 1⟩ ⟨1, 0⟩ ⟨0, 0⟩ ”⟩ (2) = ⟨1, 1⟩$
65	60 64	ax-mp	$⊢ ⟨“ ⟨0, 0⟩ ⟨0, 1⟩ ⟨1, 1⟩ ⟨1, 0⟩ ⟨0, 0⟩ ”⟩ (2) = ⟨1, 1⟩$
66	59 65	eqtri	$⊢ P (2) = ⟨1, 1⟩$
67	37 66	neeq12i	$⊢ P (0) \neq P (2) \leftrightarrow ⟨0, 0⟩ \neq ⟨1, 1⟩$
68	58 67	mpbir	$⊢ P (0) \neq P (2)$
69	68	a1i	$⊢ (Y = 2 \land X = 0) \to P (0) \neq P (2)$
70	49	adantl	$⊢ (Y = 2 \land X = 0) \to P (X) = P (0)$
71		fveq2	$⊢ Y = 2 \to P (Y) = P (2)$
72	71	adantr	$⊢ (Y = 2 \land X = 0) \to P (Y) = P (2)$
73	69 70 72	3netr4d	$⊢ (Y = 2 \land X = 0) \to P (X) \neq P (Y)$
74	73	a1d	$⊢ (Y = 2 \land X = 0) \to (X \neq Y \to P (X) \neq P (Y))$
75	74	ex	$⊢ Y = 2 \to (X = 0 \to (X \neq Y \to P (X) \neq P (Y)))$
76	22	orci	$⊢ (0 \neq 1 \lor 0 \neq 0)$
77	24 24	opthne	$⊢ ⟨0, 0⟩ \neq ⟨1, 0⟩ \leftrightarrow (0 \neq 1 \lor 0 \neq 0)$
78	76 77	mpbir	$⊢ ⟨0, 0⟩ \neq ⟨1, 0⟩$
79	1	fveq1i	$⊢ P (3) = ⟨“ ⟨0, 0⟩ ⟨0, 1⟩ ⟨1, 1⟩ ⟨1, 0⟩ ⟨0, 0⟩ ”⟩ (3)$
80		opex	$⊢ ⟨1, 0⟩ \in V$
81		s4fv3	$⊢ ⟨1, 0⟩ \in V \to ⟨“ ⟨0, 0⟩ ⟨0, 1⟩ ⟨1, 1⟩ ⟨1, 0⟩ ”⟩ (3) = ⟨1, 0⟩$
82		3nn0	$⊢ 3 \in ℕ_{0}$
83		3lt4	$⊢ 3 < 4$
84	29 30 31 81 82 83	cats1fv	$⊢ ⟨1, 0⟩ \in V \to ⟨“ ⟨0, 0⟩ ⟨0, 1⟩ ⟨1, 1⟩ ⟨1, 0⟩ ⟨0, 0⟩ ”⟩ (3) = ⟨1, 0⟩$
85	80 84	ax-mp	$⊢ ⟨“ ⟨0, 0⟩ ⟨0, 1⟩ ⟨1, 1⟩ ⟨1, 0⟩ ⟨0, 0⟩ ”⟩ (3) = ⟨1, 0⟩$
86	79 85	eqtri	$⊢ P (3) = ⟨1, 0⟩$
87	37 86	neeq12i	$⊢ P (0) \neq P (3) \leftrightarrow ⟨0, 0⟩ \neq ⟨1, 0⟩$
88	78 87	mpbir	$⊢ P (0) \neq P (3)$
89	88	a1i	$⊢ (Y = 3 \land X = 0) \to P (0) \neq P (3)$
90	49	adantl	$⊢ (Y = 3 \land X = 0) \to P (X) = P (0)$
91		fveq2	$⊢ Y = 3 \to P (Y) = P (3)$
92	91	adantr	$⊢ (Y = 3 \land X = 0) \to P (Y) = P (3)$
93	89 90 92	3netr4d	$⊢ (Y = 3 \land X = 0) \to P (X) \neq P (Y)$
94	93	a1d	$⊢ (Y = 3 \land X = 0) \to (X \neq Y \to P (X) \neq P (Y))$
95	94	ex	$⊢ Y = 3 \to (X = 0 \to (X \neq Y \to P (X) \neq P (Y)))$
96	55 75 95	3jaoi	$⊢ (Y = 1 \lor Y = 2 \lor Y = 3) \to (X = 0 \to (X \neq Y \to P (X) \neq P (Y)))$
97		eltpi	$⊢ Y \in \{1, 2, 3\} \to (Y = 1 \lor Y = 2 \lor Y = 3)$
98	96 97	syl11	$⊢ X = 0 \to (Y \in \{1, 2, 3\} \to (X \neq Y \to P (X) \neq P (Y)))$
99		simpr	$⊢ (Y = 1 \land X = 1) \to X = 1$
100		simpl	$⊢ (Y = 1 \land X = 1) \to Y = 1$
101	99 100	neeq12d	$⊢ (Y = 1 \land X = 1) \to (X \neq Y \leftrightarrow 1 \neq 1)$
102		eqid	$⊢ 1 = 1$
103		eqneqall	$⊢ 1 = 1 \to (1 \neq 1 \to P (X) \neq P (Y))$
104	102 103	ax-mp	$⊢ 1 \neq 1 \to P (X) \neq P (Y)$
105	101 104	biimtrdi	$⊢ (Y = 1 \land X = 1) \to (X \neq Y \to P (X) \neq P (Y))$
106	105	ex	$⊢ Y = 1 \to (X = 1 \to (X \neq Y \to P (X) \neq P (Y)))$
107	22	orci	$⊢ (0 \neq 1 \lor 1 \neq 1)$
108		1ex	$⊢ 1 \in V$
109	24 108	opthne	$⊢ ⟨0, 1⟩ \neq ⟨1, 1⟩ \leftrightarrow (0 \neq 1 \lor 1 \neq 1)$
110	107 109	mpbir	$⊢ ⟨0, 1⟩ \neq ⟨1, 1⟩$
111	45 66	neeq12i	$⊢ P (1) \neq P (2) \leftrightarrow ⟨0, 1⟩ \neq ⟨1, 1⟩$
112	110 111	mpbir	$⊢ P (1) \neq P (2)$
113	112	a1i	$⊢ (Y = 2 \land X = 1) \to P (1) \neq P (2)$
114		fveq2	$⊢ X = 1 \to P (X) = P (1)$
115	114	adantl	$⊢ (Y = 2 \land X = 1) \to P (X) = P (1)$
116	71	adantr	$⊢ (Y = 2 \land X = 1) \to P (Y) = P (2)$
117	113 115 116	3netr4d	$⊢ (Y = 2 \land X = 1) \to P (X) \neq P (Y)$
118	117	a1d	$⊢ (Y = 2 \land X = 1) \to (X \neq Y \to P (X) \neq P (Y))$
119	118	ex	$⊢ Y = 2 \to (X = 1 \to (X \neq Y \to P (X) \neq P (Y)))$
120	22	orci	$⊢ (0 \neq 1 \lor 1 \neq 0)$
121	24 108	opthne	$⊢ ⟨0, 1⟩ \neq ⟨1, 0⟩ \leftrightarrow (0 \neq 1 \lor 1 \neq 0)$
122	120 121	mpbir	$⊢ ⟨0, 1⟩ \neq ⟨1, 0⟩$
123	45 86	neeq12i	$⊢ P (1) \neq P (3) \leftrightarrow ⟨0, 1⟩ \neq ⟨1, 0⟩$
124	122 123	mpbir	$⊢ P (1) \neq P (3)$
125	124	a1i	$⊢ (Y = 3 \land X = 1) \to P (1) \neq P (3)$
126	114	adantl	$⊢ (Y = 3 \land X = 1) \to P (X) = P (1)$
127	91	adantr	$⊢ (Y = 3 \land X = 1) \to P (Y) = P (3)$
128	125 126 127	3netr4d	$⊢ (Y = 3 \land X = 1) \to P (X) \neq P (Y)$
129	128	a1d	$⊢ (Y = 3 \land X = 1) \to (X \neq Y \to P (X) \neq P (Y))$
130	129	ex	$⊢ Y = 3 \to (X = 1 \to (X \neq Y \to P (X) \neq P (Y)))$
131	106 119 130	3jaoi	$⊢ (Y = 1 \lor Y = 2 \lor Y = 3) \to (X = 1 \to (X \neq Y \to P (X) \neq P (Y)))$
132	131 97	syl11	$⊢ X = 1 \to (Y \in \{1, 2, 3\} \to (X \neq Y \to P (X) \neq P (Y)))$
133	98 132	jaoi	$⊢ (X = 0 \lor X = 1) \to (Y \in \{1, 2, 3\} \to (X \neq Y \to P (X) \neq P (Y)))$
134	21 133	syl	$⊢ X \in \{0, 1\} \to (Y \in \{1, 2, 3\} \to (X \neq Y \to P (X) \neq P (Y)))$
135		elpri	$⊢ X \in \{2, 3\} \to (X = 2 \lor X = 3)$
136	112	necomi	$⊢ P (2) \neq P (1)$
137	136	a1i	$⊢ (Y = 1 \land X = 2) \to P (2) \neq P (1)$
138		fveq2	$⊢ X = 2 \to P (X) = P (2)$
139	138	adantl	$⊢ (Y = 1 \land X = 2) \to P (X) = P (2)$
140	51	adantr	$⊢ (Y = 1 \land X = 2) \to P (Y) = P (1)$
141	137 139 140	3netr4d	$⊢ (Y = 1 \land X = 2) \to P (X) \neq P (Y)$
142	141	a1d	$⊢ (Y = 1 \land X = 2) \to (X \neq Y \to P (X) \neq P (Y))$
143	142	ex	$⊢ Y = 1 \to (X = 2 \to (X \neq Y \to P (X) \neq P (Y)))$
144		simpr	$⊢ (Y = 2 \land X = 2) \to X = 2$
145		simpl	$⊢ (Y = 2 \land X = 2) \to Y = 2$
146	144 145	neeq12d	$⊢ (Y = 2 \land X = 2) \to (X \neq Y \leftrightarrow 2 \neq 2)$
147		eqid	$⊢ 2 = 2$
148		eqneqall	$⊢ 2 = 2 \to (2 \neq 2 \to P (X) \neq P (Y))$
149	147 148	ax-mp	$⊢ 2 \neq 2 \to P (X) \neq P (Y)$
150	146 149	biimtrdi	$⊢ (Y = 2 \land X = 2) \to (X \neq Y \to P (X) \neq P (Y))$
151	150	ex	$⊢ Y = 2 \to (X = 2 \to (X \neq Y \to P (X) \neq P (Y)))$
152	22	necomi	$⊢ 1 \neq 0$
153	152	olci	$⊢ (1 \neq 1 \lor 1 \neq 0)$
154	108 108	opthne	$⊢ ⟨1, 1⟩ \neq ⟨1, 0⟩ \leftrightarrow (1 \neq 1 \lor 1 \neq 0)$
155	153 154	mpbir	$⊢ ⟨1, 1⟩ \neq ⟨1, 0⟩$
156	66 86	neeq12i	$⊢ P (2) \neq P (3) \leftrightarrow ⟨1, 1⟩ \neq ⟨1, 0⟩$
157	155 156	mpbir	$⊢ P (2) \neq P (3)$
158	157	a1i	$⊢ (Y = 3 \land X = 2) \to P (2) \neq P (3)$
159	138	adantl	$⊢ (Y = 3 \land X = 2) \to P (X) = P (2)$
160	91	adantr	$⊢ (Y = 3 \land X = 2) \to P (Y) = P (3)$
161	158 159 160	3netr4d	$⊢ (Y = 3 \land X = 2) \to P (X) \neq P (Y)$
162	161	a1d	$⊢ (Y = 3 \land X = 2) \to (X \neq Y \to P (X) \neq P (Y))$
163	162	ex	$⊢ Y = 3 \to (X = 2 \to (X \neq Y \to P (X) \neq P (Y)))$
164	143 151 163	3jaoi	$⊢ (Y = 1 \lor Y = 2 \lor Y = 3) \to (X = 2 \to (X \neq Y \to P (X) \neq P (Y)))$
165	164 97	syl11	$⊢ X = 2 \to (Y \in \{1, 2, 3\} \to (X \neq Y \to P (X) \neq P (Y)))$
166	124	necomi	$⊢ P (3) \neq P (1)$
167	166	a1i	$⊢ (Y = 1 \land X = 3) \to P (3) \neq P (1)$
168		fveq2	$⊢ X = 3 \to P (X) = P (3)$
169	168	adantl	$⊢ (Y = 1 \land X = 3) \to P (X) = P (3)$
170	51	adantr	$⊢ (Y = 1 \land X = 3) \to P (Y) = P (1)$
171	167 169 170	3netr4d	$⊢ (Y = 1 \land X = 3) \to P (X) \neq P (Y)$
172	171	a1d	$⊢ (Y = 1 \land X = 3) \to (X \neq Y \to P (X) \neq P (Y))$
173	172	ex	$⊢ Y = 1 \to (X = 3 \to (X \neq Y \to P (X) \neq P (Y)))$
174	157	necomi	$⊢ P (3) \neq P (2)$
175	174	a1i	$⊢ (Y = 2 \land X = 3) \to P (3) \neq P (2)$
176	168	adantl	$⊢ (Y = 2 \land X = 3) \to P (X) = P (3)$
177	71	adantr	$⊢ (Y = 2 \land X = 3) \to P (Y) = P (2)$
178	175 176 177	3netr4d	$⊢ (Y = 2 \land X = 3) \to P (X) \neq P (Y)$
179	178	a1d	$⊢ (Y = 2 \land X = 3) \to (X \neq Y \to P (X) \neq P (Y))$
180	179	ex	$⊢ Y = 2 \to (X = 3 \to (X \neq Y \to P (X) \neq P (Y)))$
181		simpr	$⊢ (Y = 3 \land X = 3) \to X = 3$
182		simpl	$⊢ (Y = 3 \land X = 3) \to Y = 3$
183	181 182	neeq12d	$⊢ (Y = 3 \land X = 3) \to (X \neq Y \leftrightarrow 3 \neq 3)$
184		eqid	$⊢ 3 = 3$
185		eqneqall	$⊢ 3 = 3 \to (3 \neq 3 \to P (X) \neq P (Y))$
186	184 185	ax-mp	$⊢ 3 \neq 3 \to P (X) \neq P (Y)$
187	183 186	biimtrdi	$⊢ (Y = 3 \land X = 3) \to (X \neq Y \to P (X) \neq P (Y))$
188	187	ex	$⊢ Y = 3 \to (X = 3 \to (X \neq Y \to P (X) \neq P (Y)))$
189	173 180 188	3jaoi	$⊢ (Y = 1 \lor Y = 2 \lor Y = 3) \to (X = 3 \to (X \neq Y \to P (X) \neq P (Y)))$
190	189 97	syl11	$⊢ X = 3 \to (Y \in \{1, 2, 3\} \to (X \neq Y \to P (X) \neq P (Y)))$
191	165 190	jaoi	$⊢ (X = 2 \lor X = 3) \to (Y \in \{1, 2, 3\} \to (X \neq Y \to P (X) \neq P (Y)))$
192	135 191	syl	$⊢ X \in \{2, 3\} \to (Y \in \{1, 2, 3\} \to (X \neq Y \to P (X) \neq P (Y)))$
193	134 192	jaoi	$⊢ (X \in \{0, 1\} \lor X \in \{2, 3\}) \to (Y \in \{1, 2, 3\} \to (X \neq Y \to P (X) \neq P (Y)))$
194		elsni	$⊢ X \in \{4\} \to X = 4$
195	1	fveq1i	$⊢ P (4) = ⟨“ ⟨0, 0⟩ ⟨0, 1⟩ ⟨1, 1⟩ ⟨1, 0⟩ ⟨0, 0⟩ ”⟩ (4)$
196	29 30 31	cats1fvn	$⊢ ⟨0, 0⟩ \in V \to ⟨“ ⟨0, 0⟩ ⟨0, 1⟩ ⟨1, 1⟩ ⟨1, 0⟩ ⟨0, 0⟩ ”⟩ (4) = ⟨0, 0⟩$
197	28 196	ax-mp	$⊢ ⟨“ ⟨0, 0⟩ ⟨0, 1⟩ ⟨1, 1⟩ ⟨1, 0⟩ ⟨0, 0⟩ ”⟩ (4) = ⟨0, 0⟩$
198	195 197	eqtri	$⊢ P (4) = ⟨0, 0⟩$
199	198 45	neeq12i	$⊢ P (4) \neq P (1) \leftrightarrow ⟨0, 0⟩ \neq ⟨0, 1⟩$
200	26 199	mpbir	$⊢ P (4) \neq P (1)$
201	200	a1i	$⊢ (Y = 1 \land X = 4) \to P (4) \neq P (1)$
202		fveq2	$⊢ X = 4 \to P (X) = P (4)$
203	202	adantl	$⊢ (Y = 1 \land X = 4) \to P (X) = P (4)$
204	51	adantr	$⊢ (Y = 1 \land X = 4) \to P (Y) = P (1)$
205	201 203 204	3netr4d	$⊢ (Y = 1 \land X = 4) \to P (X) \neq P (Y)$
206	205	a1d	$⊢ (Y = 1 \land X = 4) \to (X \neq Y \to P (X) \neq P (Y))$
207	206	ex	$⊢ Y = 1 \to (X = 4 \to (X \neq Y \to P (X) \neq P (Y)))$
208	198 66	neeq12i	$⊢ P (4) \neq P (2) \leftrightarrow ⟨0, 0⟩ \neq ⟨1, 1⟩$
209	58 208	mpbir	$⊢ P (4) \neq P (2)$
210	209	a1i	$⊢ (Y = 2 \land X = 4) \to P (4) \neq P (2)$
211	202	adantl	$⊢ (Y = 2 \land X = 4) \to P (X) = P (4)$
212	71	adantr	$⊢ (Y = 2 \land X = 4) \to P (Y) = P (2)$
213	210 211 212	3netr4d	$⊢ (Y = 2 \land X = 4) \to P (X) \neq P (Y)$
214	213	a1d	$⊢ (Y = 2 \land X = 4) \to (X \neq Y \to P (X) \neq P (Y))$
215	214	ex	$⊢ Y = 2 \to (X = 4 \to (X \neq Y \to P (X) \neq P (Y)))$
216	198 86	neeq12i	$⊢ P (4) \neq P (3) \leftrightarrow ⟨0, 0⟩ \neq ⟨1, 0⟩$
217	78 216	mpbir	$⊢ P (4) \neq P (3)$
218	217	a1i	$⊢ (Y = 3 \land X = 4) \to P (4) \neq P (3)$
219	202	adantl	$⊢ (Y = 3 \land X = 4) \to P (X) = P (4)$
220	91	adantr	$⊢ (Y = 3 \land X = 4) \to P (Y) = P (3)$
221	218 219 220	3netr4d	$⊢ (Y = 3 \land X = 4) \to P (X) \neq P (Y)$
222	221	a1d	$⊢ (Y = 3 \land X = 4) \to (X \neq Y \to P (X) \neq P (Y))$
223	222	ex	$⊢ Y = 3 \to (X = 4 \to (X \neq Y \to P (X) \neq P (Y)))$
224	207 215 223	3jaoi	$⊢ (Y = 1 \lor Y = 2 \lor Y = 3) \to (X = 4 \to (X \neq Y \to P (X) \neq P (Y)))$
225	97 194 224	syl2imc	$⊢ X \in \{4\} \to (Y \in \{1, 2, 3\} \to (X \neq Y \to P (X) \neq P (Y)))$
226	193 225	jaoi	$⊢ ((X \in \{0, 1\} \lor X \in \{2, 3\}) \lor X \in \{4\}) \to (Y \in \{1, 2, 3\} \to (X \neq Y \to P (X) \neq P (Y)))$
227	20 226	sylbi	$⊢ X \in ((\{0, 1\} \cup \{2, 3\}) \cup \{4\}) \to (Y \in \{1, 2, 3\} \to (X \neq Y \to P (X) \neq P (Y)))$
228	227	imp	$⊢ (X \in ((\{0, 1\} \cup \{2, 3\}) \cup \{4\}) \land Y \in \{1, 2, 3\}) \to (X \neq Y \to P (X) \neq P (Y))$
229	14 16 228	syl2anb	$⊢ (X \in (0 ..^\|P\|) \land Y \in (1 ..^4)) \to (X \neq Y \to P (X) \neq P (Y))$

Metamath Proof Explorer

Theorem gpgprismgr4cycllem7

Proof