gpgprismgr4cycllem7 - Mathbox for Alexander van der Vekens

	Mathbox for Alexander van der Vekens		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > gpgprismgr4cycllem7		Structured version Visualization version GIF version

Theorem gpgprismgr4cycllem7 48289

Description: Lemma 7 for gpgprismgr4cycl0 48294: the cycle ⟨𝑃, 𝐹⟩ is proper, i.e., it has no overlapping vertices, except the first and the last one. (Contributed by AV, 1-Nov-2025.)

**Hypothesis**
Ref	Expression
gpgprismgr4cycl.p	⊢ 𝑃 = ⟨“⟨0, 0⟩⟨0, 1⟩⟨1, 1⟩⟨1, 0⟩⟨0, 0⟩”⟩

**Assertion**
Ref	Expression
gpgprismgr4cycllem7	⊢ ((𝑋 ∈ (0..^(♯‘𝑃)) ∧ 𝑌 ∈ (1..^4)) → (𝑋 ≠ 𝑌 → (𝑃‘𝑋) ≠ (𝑃‘𝑌)))

**Proof of Theorem gpgprismgr4cycllem7**
Step	Hyp	Ref	Expression
1		gpgprismgr4cycl.p	. . . . . . 7 ⊢ 𝑃 = ⟨“⟨0, 0⟩⟨0, 1⟩⟨1, 1⟩⟨1, 0⟩⟨0, 0⟩”⟩
2	1	gpgprismgr4cycllem4 48286	. . . . . 6 ⊢ (♯‘𝑃) = 5
3		df-5 12209	. . . . . 6 ⊢ 5 = (4 + 1)
4	2, 3	eqtri 2757	. . . . 5 ⊢ (♯‘𝑃) = (4 + 1)
5	4	oveq2i 7367	. . . 4 ⊢ (0..^(♯‘𝑃)) = (0..^(4 + 1))
6		4nn0 12418	. . . . . 6 ⊢ 4 ∈ ℕ₀
7		elnn0uz 12790	. . . . . 6 ⊢ (4 ∈ ℕ₀ ↔ 4 ∈ (ℤ_≥‘0))
8	6, 7	mpbi 230	. . . . 5 ⊢ 4 ∈ (ℤ_≥‘0)
9		fzosplitsn 13690	. . . . 5 ⊢ (4 ∈ (ℤ_≥‘0) → (0..^(4 + 1)) = ((0..^4) ∪ {4}))
10	8, 9	ax-mp 5	. . . 4 ⊢ (0..^(4 + 1)) = ((0..^4) ∪ {4})
11		fzo0to42pr 13667	. . . . 5 ⊢ (0..^4) = ({0, 1} ∪ {2, 3})
12	11	uneq1i 4114	. . . 4 ⊢ ((0..^4) ∪ {4}) = (({0, 1} ∪ {2, 3}) ∪ {4})
13	5, 10, 12	3eqtri 2761	. . 3 ⊢ (0..^(♯‘𝑃)) = (({0, 1} ∪ {2, 3}) ∪ {4})
14	13	eleq2i 2826	. 2 ⊢ (𝑋 ∈ (0..^(♯‘𝑃)) ↔ 𝑋 ∈ (({0, 1} ∪ {2, 3}) ∪ {4}))
15		fzo1to4tp 13668	. . 3 ⊢ (1..^4) = {1, 2, 3}
16	15	eleq2i 2826	. 2 ⊢ (𝑌 ∈ (1..^4) ↔ 𝑌 ∈ {1, 2, 3})
17		elun 4103	. . . . 5 ⊢ (𝑋 ∈ (({0, 1} ∪ {2, 3}) ∪ {4}) ↔ (𝑋 ∈ ({0, 1} ∪ {2, 3}) ∨ 𝑋 ∈ {4}))
18		elun 4103	. . . . . 6 ⊢ (𝑋 ∈ ({0, 1} ∪ {2, 3}) ↔ (𝑋 ∈ {0, 1} ∨ 𝑋 ∈ {2, 3}))
19	18	orbi1i 913	. . . . 5 ⊢ ((𝑋 ∈ ({0, 1} ∪ {2, 3}) ∨ 𝑋 ∈ {4}) ↔ ((𝑋 ∈ {0, 1} ∨ 𝑋 ∈ {2, 3}) ∨ 𝑋 ∈ {4}))
20	17, 19	bitri 275	. . . 4 ⊢ (𝑋 ∈ (({0, 1} ∪ {2, 3}) ∪ {4}) ↔ ((𝑋 ∈ {0, 1} ∨ 𝑋 ∈ {2, 3}) ∨ 𝑋 ∈ {4}))
21		elpri 4602	. . . . . . 7 ⊢ (𝑋 ∈ {0, 1} → (𝑋 = 0 ∨ 𝑋 = 1))
22		0ne1 12214	. . . . . . . . . . . . . . . . 17 ⊢ 0 ≠ 1
23	22	olci 866	. . . . . . . . . . . . . . . 16 ⊢ (0 ≠ 0 ∨ 0 ≠ 1)
24		c0ex 11124	. . . . . . . . . . . . . . . . 17 ⊢ 0 ∈ V
25	24, 24	opthne 5428	. . . . . . . . . . . . . . . 16 ⊢ (⟨0, 0⟩ ≠ ⟨0, 1⟩ ↔ (0 ≠ 0 ∨ 0 ≠ 1))
26	23, 25	mpbir 231	. . . . . . . . . . . . . . 15 ⊢ ⟨0, 0⟩ ≠ ⟨0, 1⟩
27	1	fveq1i 6833	. . . . . . . . . . . . . . . . 17 ⊢ (𝑃‘0) = (⟨“⟨0, 0⟩⟨0, 1⟩⟨1, 1⟩⟨1, 0⟩⟨0, 0⟩”⟩‘0)
28		opex 5410	. . . . . . . . . . . . . . . . . 18 ⊢ ⟨0, 0⟩ ∈ V
29		df-s5 14772	. . . . . . . . . . . . . . . . . . 19 ⊢ ⟨“⟨0, 0⟩⟨0, 1⟩⟨1, 1⟩⟨1, 0⟩⟨0, 0⟩”⟩ = (⟨“⟨0, 0⟩⟨0, 1⟩⟨1, 1⟩⟨1, 0⟩”⟩ ++ ⟨“⟨0, 0⟩”⟩)
30		s4cli 14803	. . . . . . . . . . . . . . . . . . 19 ⊢ ⟨“⟨0, 0⟩⟨0, 1⟩⟨1, 1⟩⟨1, 0⟩”⟩ ∈ Word V
31		s4len 14820	. . . . . . . . . . . . . . . . . . 19 ⊢ (♯‘⟨“⟨0, 0⟩⟨0, 1⟩⟨1, 1⟩⟨1, 0⟩”⟩) = 4
32		s4fv0 14816	. . . . . . . . . . . . . . . . . . 19 ⊢ (⟨0, 0⟩ ∈ V → (⟨“⟨0, 0⟩⟨0, 1⟩⟨1, 1⟩⟨1, 0⟩”⟩‘0) = ⟨0, 0⟩)
33		0nn0 12414	. . . . . . . . . . . . . . . . . . 19 ⊢ 0 ∈ ℕ₀
34		4pos 12250	. . . . . . . . . . . . . . . . . . 19 ⊢ 0 < 4
35	29, 30, 31, 32, 33, 34	cats1fv 14780	. . . . . . . . . . . . . . . . . 18 ⊢ (⟨0, 0⟩ ∈ V → (⟨“⟨0, 0⟩⟨0, 1⟩⟨1, 1⟩⟨1, 0⟩⟨0, 0⟩”⟩‘0) = ⟨0, 0⟩)
36	28, 35	ax-mp 5	. . . . . . . . . . . . . . . . 17 ⊢ (⟨“⟨0, 0⟩⟨0, 1⟩⟨1, 1⟩⟨1, 0⟩⟨0, 0⟩”⟩‘0) = ⟨0, 0⟩
37	27, 36	eqtri 2757	. . . . . . . . . . . . . . . 16 ⊢ (𝑃‘0) = ⟨0, 0⟩
38	1	fveq1i 6833	. . . . . . . . . . . . . . . . 17 ⊢ (𝑃‘1) = (⟨“⟨0, 0⟩⟨0, 1⟩⟨1, 1⟩⟨1, 0⟩⟨0, 0⟩”⟩‘1)
39		opex 5410	. . . . . . . . . . . . . . . . . 18 ⊢ ⟨0, 1⟩ ∈ V
40		s4fv1 14817	. . . . . . . . . . . . . . . . . . 19 ⊢ (⟨0, 1⟩ ∈ V → (⟨“⟨0, 0⟩⟨0, 1⟩⟨1, 1⟩⟨1, 0⟩”⟩‘1) = ⟨0, 1⟩)
41		1nn0 12415	. . . . . . . . . . . . . . . . . . 19 ⊢ 1 ∈ ℕ₀
42		1lt4 12314	. . . . . . . . . . . . . . . . . . 19 ⊢ 1 < 4
43	29, 30, 31, 40, 41, 42	cats1fv 14780	. . . . . . . . . . . . . . . . . 18 ⊢ (⟨0, 1⟩ ∈ V → (⟨“⟨0, 0⟩⟨0, 1⟩⟨1, 1⟩⟨1, 0⟩⟨0, 0⟩”⟩‘1) = ⟨0, 1⟩)
44	39, 43	ax-mp 5	. . . . . . . . . . . . . . . . 17 ⊢ (⟨“⟨0, 0⟩⟨0, 1⟩⟨1, 1⟩⟨1, 0⟩⟨0, 0⟩”⟩‘1) = ⟨0, 1⟩
45	38, 44	eqtri 2757	. . . . . . . . . . . . . . . 16 ⊢ (𝑃‘1) = ⟨0, 1⟩
46	37, 45	neeq12i 2996	. . . . . . . . . . . . . . 15 ⊢ ((𝑃‘0) ≠ (𝑃‘1) ↔ ⟨0, 0⟩ ≠ ⟨0, 1⟩)
47	26, 46	mpbir 231	. . . . . . . . . . . . . 14 ⊢ (𝑃‘0) ≠ (𝑃‘1)
48	47	a1i 11	. . . . . . . . . . . . 13 ⊢ ((𝑌 = 1 ∧ 𝑋 = 0) → (𝑃‘0) ≠ (𝑃‘1))
49		fveq2 6832	. . . . . . . . . . . . . 14 ⊢ (𝑋 = 0 → (𝑃‘𝑋) = (𝑃‘0))
50	49	adantl 481	. . . . . . . . . . . . 13 ⊢ ((𝑌 = 1 ∧ 𝑋 = 0) → (𝑃‘𝑋) = (𝑃‘0))
51		fveq2 6832	. . . . . . . . . . . . . 14 ⊢ (𝑌 = 1 → (𝑃‘𝑌) = (𝑃‘1))
52	51	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝑌 = 1 ∧ 𝑋 = 0) → (𝑃‘𝑌) = (𝑃‘1))
53	48, 50, 52	3netr4d 3007	. . . . . . . . . . . 12 ⊢ ((𝑌 = 1 ∧ 𝑋 = 0) → (𝑃‘𝑋) ≠ (𝑃‘𝑌))
54	53	a1d 25	. . . . . . . . . . 11 ⊢ ((𝑌 = 1 ∧ 𝑋 = 0) → (𝑋 ≠ 𝑌 → (𝑃‘𝑋) ≠ (𝑃‘𝑌)))
55	54	ex 412	. . . . . . . . . 10 ⊢ (𝑌 = 1 → (𝑋 = 0 → (𝑋 ≠ 𝑌 → (𝑃‘𝑋) ≠ (𝑃‘𝑌))))
56	22	orci 865	. . . . . . . . . . . . . . . 16 ⊢ (0 ≠ 1 ∨ 0 ≠ 1)
57	24, 24	opthne 5428	. . . . . . . . . . . . . . . 16 ⊢ (⟨0, 0⟩ ≠ ⟨1, 1⟩ ↔ (0 ≠ 1 ∨ 0 ≠ 1))
58	56, 57	mpbir 231	. . . . . . . . . . . . . . 15 ⊢ ⟨0, 0⟩ ≠ ⟨1, 1⟩
59	1	fveq1i 6833	. . . . . . . . . . . . . . . . 17 ⊢ (𝑃‘2) = (⟨“⟨0, 0⟩⟨0, 1⟩⟨1, 1⟩⟨1, 0⟩⟨0, 0⟩”⟩‘2)
60		opex 5410	. . . . . . . . . . . . . . . . . 18 ⊢ ⟨1, 1⟩ ∈ V
61		s4fv2 14818	. . . . . . . . . . . . . . . . . . 19 ⊢ (⟨1, 1⟩ ∈ V → (⟨“⟨0, 0⟩⟨0, 1⟩⟨1, 1⟩⟨1, 0⟩”⟩‘2) = ⟨1, 1⟩)
62		2nn0 12416	. . . . . . . . . . . . . . . . . . 19 ⊢ 2 ∈ ℕ₀
63		2lt4 12313	. . . . . . . . . . . . . . . . . . 19 ⊢ 2 < 4
64	29, 30, 31, 61, 62, 63	cats1fv 14780	. . . . . . . . . . . . . . . . . 18 ⊢ (⟨1, 1⟩ ∈ V → (⟨“⟨0, 0⟩⟨0, 1⟩⟨1, 1⟩⟨1, 0⟩⟨0, 0⟩”⟩‘2) = ⟨1, 1⟩)
65	60, 64	ax-mp 5	. . . . . . . . . . . . . . . . 17 ⊢ (⟨“⟨0, 0⟩⟨0, 1⟩⟨1, 1⟩⟨1, 0⟩⟨0, 0⟩”⟩‘2) = ⟨1, 1⟩
66	59, 65	eqtri 2757	. . . . . . . . . . . . . . . 16 ⊢ (𝑃‘2) = ⟨1, 1⟩
67	37, 66	neeq12i 2996	. . . . . . . . . . . . . . 15 ⊢ ((𝑃‘0) ≠ (𝑃‘2) ↔ ⟨0, 0⟩ ≠ ⟨1, 1⟩)
68	58, 67	mpbir 231	. . . . . . . . . . . . . 14 ⊢ (𝑃‘0) ≠ (𝑃‘2)
69	68	a1i 11	. . . . . . . . . . . . 13 ⊢ ((𝑌 = 2 ∧ 𝑋 = 0) → (𝑃‘0) ≠ (𝑃‘2))
70	49	adantl 481	. . . . . . . . . . . . 13 ⊢ ((𝑌 = 2 ∧ 𝑋 = 0) → (𝑃‘𝑋) = (𝑃‘0))
71		fveq2 6832	. . . . . . . . . . . . . 14 ⊢ (𝑌 = 2 → (𝑃‘𝑌) = (𝑃‘2))
72	71	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝑌 = 2 ∧ 𝑋 = 0) → (𝑃‘𝑌) = (𝑃‘2))
73	69, 70, 72	3netr4d 3007	. . . . . . . . . . . 12 ⊢ ((𝑌 = 2 ∧ 𝑋 = 0) → (𝑃‘𝑋) ≠ (𝑃‘𝑌))
74	73	a1d 25	. . . . . . . . . . 11 ⊢ ((𝑌 = 2 ∧ 𝑋 = 0) → (𝑋 ≠ 𝑌 → (𝑃‘𝑋) ≠ (𝑃‘𝑌)))
75	74	ex 412	. . . . . . . . . 10 ⊢ (𝑌 = 2 → (𝑋 = 0 → (𝑋 ≠ 𝑌 → (𝑃‘𝑋) ≠ (𝑃‘𝑌))))
76	22	orci 865	. . . . . . . . . . . . . . . 16 ⊢ (0 ≠ 1 ∨ 0 ≠ 0)
77	24, 24	opthne 5428	. . . . . . . . . . . . . . . 16 ⊢ (⟨0, 0⟩ ≠ ⟨1, 0⟩ ↔ (0 ≠ 1 ∨ 0 ≠ 0))
78	76, 77	mpbir 231	. . . . . . . . . . . . . . 15 ⊢ ⟨0, 0⟩ ≠ ⟨1, 0⟩
79	1	fveq1i 6833	. . . . . . . . . . . . . . . . 17 ⊢ (𝑃‘3) = (⟨“⟨0, 0⟩⟨0, 1⟩⟨1, 1⟩⟨1, 0⟩⟨0, 0⟩”⟩‘3)
80		opex 5410	. . . . . . . . . . . . . . . . . 18 ⊢ ⟨1, 0⟩ ∈ V
81		s4fv3 14819	. . . . . . . . . . . . . . . . . . 19 ⊢ (⟨1, 0⟩ ∈ V → (⟨“⟨0, 0⟩⟨0, 1⟩⟨1, 1⟩⟨1, 0⟩”⟩‘3) = ⟨1, 0⟩)
82		3nn0 12417	. . . . . . . . . . . . . . . . . . 19 ⊢ 3 ∈ ℕ₀
83		3lt4 12312	. . . . . . . . . . . . . . . . . . 19 ⊢ 3 < 4
84	29, 30, 31, 81, 82, 83	cats1fv 14780	. . . . . . . . . . . . . . . . . 18 ⊢ (⟨1, 0⟩ ∈ V → (⟨“⟨0, 0⟩⟨0, 1⟩⟨1, 1⟩⟨1, 0⟩⟨0, 0⟩”⟩‘3) = ⟨1, 0⟩)
85	80, 84	ax-mp 5	. . . . . . . . . . . . . . . . 17 ⊢ (⟨“⟨0, 0⟩⟨0, 1⟩⟨1, 1⟩⟨1, 0⟩⟨0, 0⟩”⟩‘3) = ⟨1, 0⟩
86	79, 85	eqtri 2757	. . . . . . . . . . . . . . . 16 ⊢ (𝑃‘3) = ⟨1, 0⟩
87	37, 86	neeq12i 2996	. . . . . . . . . . . . . . 15 ⊢ ((𝑃‘0) ≠ (𝑃‘3) ↔ ⟨0, 0⟩ ≠ ⟨1, 0⟩)
88	78, 87	mpbir 231	. . . . . . . . . . . . . 14 ⊢ (𝑃‘0) ≠ (𝑃‘3)
89	88	a1i 11	. . . . . . . . . . . . 13 ⊢ ((𝑌 = 3 ∧ 𝑋 = 0) → (𝑃‘0) ≠ (𝑃‘3))
90	49	adantl 481	. . . . . . . . . . . . 13 ⊢ ((𝑌 = 3 ∧ 𝑋 = 0) → (𝑃‘𝑋) = (𝑃‘0))
91		fveq2 6832	. . . . . . . . . . . . . 14 ⊢ (𝑌 = 3 → (𝑃‘𝑌) = (𝑃‘3))
92	91	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝑌 = 3 ∧ 𝑋 = 0) → (𝑃‘𝑌) = (𝑃‘3))
93	89, 90, 92	3netr4d 3007	. . . . . . . . . . . 12 ⊢ ((𝑌 = 3 ∧ 𝑋 = 0) → (𝑃‘𝑋) ≠ (𝑃‘𝑌))
94	93	a1d 25	. . . . . . . . . . 11 ⊢ ((𝑌 = 3 ∧ 𝑋 = 0) → (𝑋 ≠ 𝑌 → (𝑃‘𝑋) ≠ (𝑃‘𝑌)))
95	94	ex 412	. . . . . . . . . 10 ⊢ (𝑌 = 3 → (𝑋 = 0 → (𝑋 ≠ 𝑌 → (𝑃‘𝑋) ≠ (𝑃‘𝑌))))
96	55, 75, 95	3jaoi 1430	. . . . . . . . 9 ⊢ ((𝑌 = 1 ∨ 𝑌 = 2 ∨ 𝑌 = 3) → (𝑋 = 0 → (𝑋 ≠ 𝑌 → (𝑃‘𝑋) ≠ (𝑃‘𝑌))))
97		eltpi 4643	. . . . . . . . 9 ⊢ (𝑌 ∈ {1, 2, 3} → (𝑌 = 1 ∨ 𝑌 = 2 ∨ 𝑌 = 3))
98	96, 97	syl11 33	. . . . . . . 8 ⊢ (𝑋 = 0 → (𝑌 ∈ {1, 2, 3} → (𝑋 ≠ 𝑌 → (𝑃‘𝑋) ≠ (𝑃‘𝑌))))
99		simpr 484	. . . . . . . . . . . . 13 ⊢ ((𝑌 = 1 ∧ 𝑋 = 1) → 𝑋 = 1)
100		simpl 482	. . . . . . . . . . . . 13 ⊢ ((𝑌 = 1 ∧ 𝑋 = 1) → 𝑌 = 1)
101	99, 100	neeq12d 2991	. . . . . . . . . . . 12 ⊢ ((𝑌 = 1 ∧ 𝑋 = 1) → (𝑋 ≠ 𝑌 ↔ 1 ≠ 1))
102		eqid 2734	. . . . . . . . . . . . 13 ⊢ 1 = 1
103		eqneqall 2941	. . . . . . . . . . . . 13 ⊢ (1 = 1 → (1 ≠ 1 → (𝑃‘𝑋) ≠ (𝑃‘𝑌)))
104	102, 103	ax-mp 5	. . . . . . . . . . . 12 ⊢ (1 ≠ 1 → (𝑃‘𝑋) ≠ (𝑃‘𝑌))
105	101, 104	biimtrdi 253	. . . . . . . . . . 11 ⊢ ((𝑌 = 1 ∧ 𝑋 = 1) → (𝑋 ≠ 𝑌 → (𝑃‘𝑋) ≠ (𝑃‘𝑌)))
106	105	ex 412	. . . . . . . . . 10 ⊢ (𝑌 = 1 → (𝑋 = 1 → (𝑋 ≠ 𝑌 → (𝑃‘𝑋) ≠ (𝑃‘𝑌))))
107	22	orci 865	. . . . . . . . . . . . . . . 16 ⊢ (0 ≠ 1 ∨ 1 ≠ 1)
108		1ex 11126	. . . . . . . . . . . . . . . . 17 ⊢ 1 ∈ V
109	24, 108	opthne 5428	. . . . . . . . . . . . . . . 16 ⊢ (⟨0, 1⟩ ≠ ⟨1, 1⟩ ↔ (0 ≠ 1 ∨ 1 ≠ 1))
110	107, 109	mpbir 231	. . . . . . . . . . . . . . 15 ⊢ ⟨0, 1⟩ ≠ ⟨1, 1⟩
111	45, 66	neeq12i 2996	. . . . . . . . . . . . . . 15 ⊢ ((𝑃‘1) ≠ (𝑃‘2) ↔ ⟨0, 1⟩ ≠ ⟨1, 1⟩)
112	110, 111	mpbir 231	. . . . . . . . . . . . . 14 ⊢ (𝑃‘1) ≠ (𝑃‘2)
113	112	a1i 11	. . . . . . . . . . . . 13 ⊢ ((𝑌 = 2 ∧ 𝑋 = 1) → (𝑃‘1) ≠ (𝑃‘2))
114		fveq2 6832	. . . . . . . . . . . . . 14 ⊢ (𝑋 = 1 → (𝑃‘𝑋) = (𝑃‘1))
115	114	adantl 481	. . . . . . . . . . . . 13 ⊢ ((𝑌 = 2 ∧ 𝑋 = 1) → (𝑃‘𝑋) = (𝑃‘1))
116	71	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝑌 = 2 ∧ 𝑋 = 1) → (𝑃‘𝑌) = (𝑃‘2))
117	113, 115, 116	3netr4d 3007	. . . . . . . . . . . 12 ⊢ ((𝑌 = 2 ∧ 𝑋 = 1) → (𝑃‘𝑋) ≠ (𝑃‘𝑌))
118	117	a1d 25	. . . . . . . . . . 11 ⊢ ((𝑌 = 2 ∧ 𝑋 = 1) → (𝑋 ≠ 𝑌 → (𝑃‘𝑋) ≠ (𝑃‘𝑌)))
119	118	ex 412	. . . . . . . . . 10 ⊢ (𝑌 = 2 → (𝑋 = 1 → (𝑋 ≠ 𝑌 → (𝑃‘𝑋) ≠ (𝑃‘𝑌))))
120	22	orci 865	. . . . . . . . . . . . . . . 16 ⊢ (0 ≠ 1 ∨ 1 ≠ 0)
121	24, 108	opthne 5428	. . . . . . . . . . . . . . . 16 ⊢ (⟨0, 1⟩ ≠ ⟨1, 0⟩ ↔ (0 ≠ 1 ∨ 1 ≠ 0))
122	120, 121	mpbir 231	. . . . . . . . . . . . . . 15 ⊢ ⟨0, 1⟩ ≠ ⟨1, 0⟩
123	45, 86	neeq12i 2996	. . . . . . . . . . . . . . 15 ⊢ ((𝑃‘1) ≠ (𝑃‘3) ↔ ⟨0, 1⟩ ≠ ⟨1, 0⟩)
124	122, 123	mpbir 231	. . . . . . . . . . . . . 14 ⊢ (𝑃‘1) ≠ (𝑃‘3)
125	124	a1i 11	. . . . . . . . . . . . 13 ⊢ ((𝑌 = 3 ∧ 𝑋 = 1) → (𝑃‘1) ≠ (𝑃‘3))
126	114	adantl 481	. . . . . . . . . . . . 13 ⊢ ((𝑌 = 3 ∧ 𝑋 = 1) → (𝑃‘𝑋) = (𝑃‘1))
127	91	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝑌 = 3 ∧ 𝑋 = 1) → (𝑃‘𝑌) = (𝑃‘3))
128	125, 126, 127	3netr4d 3007	. . . . . . . . . . . 12 ⊢ ((𝑌 = 3 ∧ 𝑋 = 1) → (𝑃‘𝑋) ≠ (𝑃‘𝑌))
129	128	a1d 25	. . . . . . . . . . 11 ⊢ ((𝑌 = 3 ∧ 𝑋 = 1) → (𝑋 ≠ 𝑌 → (𝑃‘𝑋) ≠ (𝑃‘𝑌)))
130	129	ex 412	. . . . . . . . . 10 ⊢ (𝑌 = 3 → (𝑋 = 1 → (𝑋 ≠ 𝑌 → (𝑃‘𝑋) ≠ (𝑃‘𝑌))))
131	106, 119, 130	3jaoi 1430	. . . . . . . . 9 ⊢ ((𝑌 = 1 ∨ 𝑌 = 2 ∨ 𝑌 = 3) → (𝑋 = 1 → (𝑋 ≠ 𝑌 → (𝑃‘𝑋) ≠ (𝑃‘𝑌))))
132	131, 97	syl11 33	. . . . . . . 8 ⊢ (𝑋 = 1 → (𝑌 ∈ {1, 2, 3} → (𝑋 ≠ 𝑌 → (𝑃‘𝑋) ≠ (𝑃‘𝑌))))
133	98, 132	jaoi 857	. . . . . . 7 ⊢ ((𝑋 = 0 ∨ 𝑋 = 1) → (𝑌 ∈ {1, 2, 3} → (𝑋 ≠ 𝑌 → (𝑃‘𝑋) ≠ (𝑃‘𝑌))))
134	21, 133	syl 17	. . . . . 6 ⊢ (𝑋 ∈ {0, 1} → (𝑌 ∈ {1, 2, 3} → (𝑋 ≠ 𝑌 → (𝑃‘𝑋) ≠ (𝑃‘𝑌))))
135		elpri 4602	. . . . . . 7 ⊢ (𝑋 ∈ {2, 3} → (𝑋 = 2 ∨ 𝑋 = 3))
136	112	necomi 2984	. . . . . . . . . . . . . 14 ⊢ (𝑃‘2) ≠ (𝑃‘1)
137	136	a1i 11	. . . . . . . . . . . . 13 ⊢ ((𝑌 = 1 ∧ 𝑋 = 2) → (𝑃‘2) ≠ (𝑃‘1))
138		fveq2 6832	. . . . . . . . . . . . . 14 ⊢ (𝑋 = 2 → (𝑃‘𝑋) = (𝑃‘2))
139	138	adantl 481	. . . . . . . . . . . . 13 ⊢ ((𝑌 = 1 ∧ 𝑋 = 2) → (𝑃‘𝑋) = (𝑃‘2))
140	51	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝑌 = 1 ∧ 𝑋 = 2) → (𝑃‘𝑌) = (𝑃‘1))
141	137, 139, 140	3netr4d 3007	. . . . . . . . . . . 12 ⊢ ((𝑌 = 1 ∧ 𝑋 = 2) → (𝑃‘𝑋) ≠ (𝑃‘𝑌))
142	141	a1d 25	. . . . . . . . . . 11 ⊢ ((𝑌 = 1 ∧ 𝑋 = 2) → (𝑋 ≠ 𝑌 → (𝑃‘𝑋) ≠ (𝑃‘𝑌)))
143	142	ex 412	. . . . . . . . . 10 ⊢ (𝑌 = 1 → (𝑋 = 2 → (𝑋 ≠ 𝑌 → (𝑃‘𝑋) ≠ (𝑃‘𝑌))))
144		simpr 484	. . . . . . . . . . . . 13 ⊢ ((𝑌 = 2 ∧ 𝑋 = 2) → 𝑋 = 2)
145		simpl 482	. . . . . . . . . . . . 13 ⊢ ((𝑌 = 2 ∧ 𝑋 = 2) → 𝑌 = 2)
146	144, 145	neeq12d 2991	. . . . . . . . . . . 12 ⊢ ((𝑌 = 2 ∧ 𝑋 = 2) → (𝑋 ≠ 𝑌 ↔ 2 ≠ 2))
147		eqid 2734	. . . . . . . . . . . . 13 ⊢ 2 = 2
148		eqneqall 2941	. . . . . . . . . . . . 13 ⊢ (2 = 2 → (2 ≠ 2 → (𝑃‘𝑋) ≠ (𝑃‘𝑌)))
149	147, 148	ax-mp 5	. . . . . . . . . . . 12 ⊢ (2 ≠ 2 → (𝑃‘𝑋) ≠ (𝑃‘𝑌))
150	146, 149	biimtrdi 253	. . . . . . . . . . 11 ⊢ ((𝑌 = 2 ∧ 𝑋 = 2) → (𝑋 ≠ 𝑌 → (𝑃‘𝑋) ≠ (𝑃‘𝑌)))
151	150	ex 412	. . . . . . . . . 10 ⊢ (𝑌 = 2 → (𝑋 = 2 → (𝑋 ≠ 𝑌 → (𝑃‘𝑋) ≠ (𝑃‘𝑌))))
152	22	necomi 2984	. . . . . . . . . . . . . . . . 17 ⊢ 1 ≠ 0
153	152	olci 866	. . . . . . . . . . . . . . . 16 ⊢ (1 ≠ 1 ∨ 1 ≠ 0)
154	108, 108	opthne 5428	. . . . . . . . . . . . . . . 16 ⊢ (⟨1, 1⟩ ≠ ⟨1, 0⟩ ↔ (1 ≠ 1 ∨ 1 ≠ 0))
155	153, 154	mpbir 231	. . . . . . . . . . . . . . 15 ⊢ ⟨1, 1⟩ ≠ ⟨1, 0⟩
156	66, 86	neeq12i 2996	. . . . . . . . . . . . . . 15 ⊢ ((𝑃‘2) ≠ (𝑃‘3) ↔ ⟨1, 1⟩ ≠ ⟨1, 0⟩)
157	155, 156	mpbir 231	. . . . . . . . . . . . . 14 ⊢ (𝑃‘2) ≠ (𝑃‘3)
158	157	a1i 11	. . . . . . . . . . . . 13 ⊢ ((𝑌 = 3 ∧ 𝑋 = 2) → (𝑃‘2) ≠ (𝑃‘3))
159	138	adantl 481	. . . . . . . . . . . . 13 ⊢ ((𝑌 = 3 ∧ 𝑋 = 2) → (𝑃‘𝑋) = (𝑃‘2))
160	91	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝑌 = 3 ∧ 𝑋 = 2) → (𝑃‘𝑌) = (𝑃‘3))
161	158, 159, 160	3netr4d 3007	. . . . . . . . . . . 12 ⊢ ((𝑌 = 3 ∧ 𝑋 = 2) → (𝑃‘𝑋) ≠ (𝑃‘𝑌))
162	161	a1d 25	. . . . . . . . . . 11 ⊢ ((𝑌 = 3 ∧ 𝑋 = 2) → (𝑋 ≠ 𝑌 → (𝑃‘𝑋) ≠ (𝑃‘𝑌)))
163	162	ex 412	. . . . . . . . . 10 ⊢ (𝑌 = 3 → (𝑋 = 2 → (𝑋 ≠ 𝑌 → (𝑃‘𝑋) ≠ (𝑃‘𝑌))))
164	143, 151, 163	3jaoi 1430	. . . . . . . . 9 ⊢ ((𝑌 = 1 ∨ 𝑌 = 2 ∨ 𝑌 = 3) → (𝑋 = 2 → (𝑋 ≠ 𝑌 → (𝑃‘𝑋) ≠ (𝑃‘𝑌))))
165	164, 97	syl11 33	. . . . . . . 8 ⊢ (𝑋 = 2 → (𝑌 ∈ {1, 2, 3} → (𝑋 ≠ 𝑌 → (𝑃‘𝑋) ≠ (𝑃‘𝑌))))
166	124	necomi 2984	. . . . . . . . . . . . . 14 ⊢ (𝑃‘3) ≠ (𝑃‘1)
167	166	a1i 11	. . . . . . . . . . . . 13 ⊢ ((𝑌 = 1 ∧ 𝑋 = 3) → (𝑃‘3) ≠ (𝑃‘1))
168		fveq2 6832	. . . . . . . . . . . . . 14 ⊢ (𝑋 = 3 → (𝑃‘𝑋) = (𝑃‘3))
169	168	adantl 481	. . . . . . . . . . . . 13 ⊢ ((𝑌 = 1 ∧ 𝑋 = 3) → (𝑃‘𝑋) = (𝑃‘3))
170	51	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝑌 = 1 ∧ 𝑋 = 3) → (𝑃‘𝑌) = (𝑃‘1))
171	167, 169, 170	3netr4d 3007	. . . . . . . . . . . 12 ⊢ ((𝑌 = 1 ∧ 𝑋 = 3) → (𝑃‘𝑋) ≠ (𝑃‘𝑌))
172	171	a1d 25	. . . . . . . . . . 11 ⊢ ((𝑌 = 1 ∧ 𝑋 = 3) → (𝑋 ≠ 𝑌 → (𝑃‘𝑋) ≠ (𝑃‘𝑌)))
173	172	ex 412	. . . . . . . . . 10 ⊢ (𝑌 = 1 → (𝑋 = 3 → (𝑋 ≠ 𝑌 → (𝑃‘𝑋) ≠ (𝑃‘𝑌))))
174	157	necomi 2984	. . . . . . . . . . . . . 14 ⊢ (𝑃‘3) ≠ (𝑃‘2)
175	174	a1i 11	. . . . . . . . . . . . 13 ⊢ ((𝑌 = 2 ∧ 𝑋 = 3) → (𝑃‘3) ≠ (𝑃‘2))
176	168	adantl 481	. . . . . . . . . . . . 13 ⊢ ((𝑌 = 2 ∧ 𝑋 = 3) → (𝑃‘𝑋) = (𝑃‘3))
177	71	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝑌 = 2 ∧ 𝑋 = 3) → (𝑃‘𝑌) = (𝑃‘2))
178	175, 176, 177	3netr4d 3007	. . . . . . . . . . . 12 ⊢ ((𝑌 = 2 ∧ 𝑋 = 3) → (𝑃‘𝑋) ≠ (𝑃‘𝑌))
179	178	a1d 25	. . . . . . . . . . 11 ⊢ ((𝑌 = 2 ∧ 𝑋 = 3) → (𝑋 ≠ 𝑌 → (𝑃‘𝑋) ≠ (𝑃‘𝑌)))
180	179	ex 412	. . . . . . . . . 10 ⊢ (𝑌 = 2 → (𝑋 = 3 → (𝑋 ≠ 𝑌 → (𝑃‘𝑋) ≠ (𝑃‘𝑌))))
181		simpr 484	. . . . . . . . . . . . 13 ⊢ ((𝑌 = 3 ∧ 𝑋 = 3) → 𝑋 = 3)
182		simpl 482	. . . . . . . . . . . . 13 ⊢ ((𝑌 = 3 ∧ 𝑋 = 3) → 𝑌 = 3)
183	181, 182	neeq12d 2991	. . . . . . . . . . . 12 ⊢ ((𝑌 = 3 ∧ 𝑋 = 3) → (𝑋 ≠ 𝑌 ↔ 3 ≠ 3))
184		eqid 2734	. . . . . . . . . . . . 13 ⊢ 3 = 3
185		eqneqall 2941	. . . . . . . . . . . . 13 ⊢ (3 = 3 → (3 ≠ 3 → (𝑃‘𝑋) ≠ (𝑃‘𝑌)))
186	184, 185	ax-mp 5	. . . . . . . . . . . 12 ⊢ (3 ≠ 3 → (𝑃‘𝑋) ≠ (𝑃‘𝑌))
187	183, 186	biimtrdi 253	. . . . . . . . . . 11 ⊢ ((𝑌 = 3 ∧ 𝑋 = 3) → (𝑋 ≠ 𝑌 → (𝑃‘𝑋) ≠ (𝑃‘𝑌)))
188	187	ex 412	. . . . . . . . . 10 ⊢ (𝑌 = 3 → (𝑋 = 3 → (𝑋 ≠ 𝑌 → (𝑃‘𝑋) ≠ (𝑃‘𝑌))))
189	173, 180, 188	3jaoi 1430	. . . . . . . . 9 ⊢ ((𝑌 = 1 ∨ 𝑌 = 2 ∨ 𝑌 = 3) → (𝑋 = 3 → (𝑋 ≠ 𝑌 → (𝑃‘𝑋) ≠ (𝑃‘𝑌))))
190	189, 97	syl11 33	. . . . . . . 8 ⊢ (𝑋 = 3 → (𝑌 ∈ {1, 2, 3} → (𝑋 ≠ 𝑌 → (𝑃‘𝑋) ≠ (𝑃‘𝑌))))
191	165, 190	jaoi 857	. . . . . . 7 ⊢ ((𝑋 = 2 ∨ 𝑋 = 3) → (𝑌 ∈ {1, 2, 3} → (𝑋 ≠ 𝑌 → (𝑃‘𝑋) ≠ (𝑃‘𝑌))))
192	135, 191	syl 17	. . . . . 6 ⊢ (𝑋 ∈ {2, 3} → (𝑌 ∈ {1, 2, 3} → (𝑋 ≠ 𝑌 → (𝑃‘𝑋) ≠ (𝑃‘𝑌))))
193	134, 192	jaoi 857	. . . . 5 ⊢ ((𝑋 ∈ {0, 1} ∨ 𝑋 ∈ {2, 3}) → (𝑌 ∈ {1, 2, 3} → (𝑋 ≠ 𝑌 → (𝑃‘𝑋) ≠ (𝑃‘𝑌))))
194		elsni 4595	. . . . . 6 ⊢ (𝑋 ∈ {4} → 𝑋 = 4)
195	1	fveq1i 6833	. . . . . . . . . . . . . 14 ⊢ (𝑃‘4) = (⟨“⟨0, 0⟩⟨0, 1⟩⟨1, 1⟩⟨1, 0⟩⟨0, 0⟩”⟩‘4)
196	29, 30, 31	cats1fvn 14779	. . . . . . . . . . . . . . 15 ⊢ (⟨0, 0⟩ ∈ V → (⟨“⟨0, 0⟩⟨0, 1⟩⟨1, 1⟩⟨1, 0⟩⟨0, 0⟩”⟩‘4) = ⟨0, 0⟩)
197	28, 196	ax-mp 5	. . . . . . . . . . . . . 14 ⊢ (⟨“⟨0, 0⟩⟨0, 1⟩⟨1, 1⟩⟨1, 0⟩⟨0, 0⟩”⟩‘4) = ⟨0, 0⟩
198	195, 197	eqtri 2757	. . . . . . . . . . . . 13 ⊢ (𝑃‘4) = ⟨0, 0⟩
199	198, 45	neeq12i 2996	. . . . . . . . . . . 12 ⊢ ((𝑃‘4) ≠ (𝑃‘1) ↔ ⟨0, 0⟩ ≠ ⟨0, 1⟩)
200	26, 199	mpbir 231	. . . . . . . . . . 11 ⊢ (𝑃‘4) ≠ (𝑃‘1)
201	200	a1i 11	. . . . . . . . . 10 ⊢ ((𝑌 = 1 ∧ 𝑋 = 4) → (𝑃‘4) ≠ (𝑃‘1))
202		fveq2 6832	. . . . . . . . . . 11 ⊢ (𝑋 = 4 → (𝑃‘𝑋) = (𝑃‘4))
203	202	adantl 481	. . . . . . . . . 10 ⊢ ((𝑌 = 1 ∧ 𝑋 = 4) → (𝑃‘𝑋) = (𝑃‘4))
204	51	adantr 480	. . . . . . . . . 10 ⊢ ((𝑌 = 1 ∧ 𝑋 = 4) → (𝑃‘𝑌) = (𝑃‘1))
205	201, 203, 204	3netr4d 3007	. . . . . . . . 9 ⊢ ((𝑌 = 1 ∧ 𝑋 = 4) → (𝑃‘𝑋) ≠ (𝑃‘𝑌))
206	205	a1d 25	. . . . . . . 8 ⊢ ((𝑌 = 1 ∧ 𝑋 = 4) → (𝑋 ≠ 𝑌 → (𝑃‘𝑋) ≠ (𝑃‘𝑌)))
207	206	ex 412	. . . . . . 7 ⊢ (𝑌 = 1 → (𝑋 = 4 → (𝑋 ≠ 𝑌 → (𝑃‘𝑋) ≠ (𝑃‘𝑌))))
208	198, 66	neeq12i 2996	. . . . . . . . . . . 12 ⊢ ((𝑃‘4) ≠ (𝑃‘2) ↔ ⟨0, 0⟩ ≠ ⟨1, 1⟩)
209	58, 208	mpbir 231	. . . . . . . . . . 11 ⊢ (𝑃‘4) ≠ (𝑃‘2)
210	209	a1i 11	. . . . . . . . . 10 ⊢ ((𝑌 = 2 ∧ 𝑋 = 4) → (𝑃‘4) ≠ (𝑃‘2))
211	202	adantl 481	. . . . . . . . . 10 ⊢ ((𝑌 = 2 ∧ 𝑋 = 4) → (𝑃‘𝑋) = (𝑃‘4))
212	71	adantr 480	. . . . . . . . . 10 ⊢ ((𝑌 = 2 ∧ 𝑋 = 4) → (𝑃‘𝑌) = (𝑃‘2))
213	210, 211, 212	3netr4d 3007	. . . . . . . . 9 ⊢ ((𝑌 = 2 ∧ 𝑋 = 4) → (𝑃‘𝑋) ≠ (𝑃‘𝑌))
214	213	a1d 25	. . . . . . . 8 ⊢ ((𝑌 = 2 ∧ 𝑋 = 4) → (𝑋 ≠ 𝑌 → (𝑃‘𝑋) ≠ (𝑃‘𝑌)))
215	214	ex 412	. . . . . . 7 ⊢ (𝑌 = 2 → (𝑋 = 4 → (𝑋 ≠ 𝑌 → (𝑃‘𝑋) ≠ (𝑃‘𝑌))))
216	198, 86	neeq12i 2996	. . . . . . . . . . . 12 ⊢ ((𝑃‘4) ≠ (𝑃‘3) ↔ ⟨0, 0⟩ ≠ ⟨1, 0⟩)
217	78, 216	mpbir 231	. . . . . . . . . . 11 ⊢ (𝑃‘4) ≠ (𝑃‘3)
218	217	a1i 11	. . . . . . . . . 10 ⊢ ((𝑌 = 3 ∧ 𝑋 = 4) → (𝑃‘4) ≠ (𝑃‘3))
219	202	adantl 481	. . . . . . . . . 10 ⊢ ((𝑌 = 3 ∧ 𝑋 = 4) → (𝑃‘𝑋) = (𝑃‘4))
220	91	adantr 480	. . . . . . . . . 10 ⊢ ((𝑌 = 3 ∧ 𝑋 = 4) → (𝑃‘𝑌) = (𝑃‘3))
221	218, 219, 220	3netr4d 3007	. . . . . . . . 9 ⊢ ((𝑌 = 3 ∧ 𝑋 = 4) → (𝑃‘𝑋) ≠ (𝑃‘𝑌))
222	221	a1d 25	. . . . . . . 8 ⊢ ((𝑌 = 3 ∧ 𝑋 = 4) → (𝑋 ≠ 𝑌 → (𝑃‘𝑋) ≠ (𝑃‘𝑌)))
223	222	ex 412	. . . . . . 7 ⊢ (𝑌 = 3 → (𝑋 = 4 → (𝑋 ≠ 𝑌 → (𝑃‘𝑋) ≠ (𝑃‘𝑌))))
224	207, 215, 223	3jaoi 1430	. . . . . 6 ⊢ ((𝑌 = 1 ∨ 𝑌 = 2 ∨ 𝑌 = 3) → (𝑋 = 4 → (𝑋 ≠ 𝑌 → (𝑃‘𝑋) ≠ (𝑃‘𝑌))))
225	97, 194, 224	syl2imc 41	. . . . 5 ⊢ (𝑋 ∈ {4} → (𝑌 ∈ {1, 2, 3} → (𝑋 ≠ 𝑌 → (𝑃‘𝑋) ≠ (𝑃‘𝑌))))
226	193, 225	jaoi 857	. . . 4 ⊢ (((𝑋 ∈ {0, 1} ∨ 𝑋 ∈ {2, 3}) ∨ 𝑋 ∈ {4}) → (𝑌 ∈ {1, 2, 3} → (𝑋 ≠ 𝑌 → (𝑃‘𝑋) ≠ (𝑃‘𝑌))))
227	20, 226	sylbi 217	. . 3 ⊢ (𝑋 ∈ (({0, 1} ∪ {2, 3}) ∪ {4}) → (𝑌 ∈ {1, 2, 3} → (𝑋 ≠ 𝑌 → (𝑃‘𝑋) ≠ (𝑃‘𝑌))))
228	227	imp 406	. 2 ⊢ ((𝑋 ∈ (({0, 1} ∪ {2, 3}) ∪ {4}) ∧ 𝑌 ∈ {1, 2, 3}) → (𝑋 ≠ 𝑌 → (𝑃‘𝑋) ≠ (𝑃‘𝑌)))
229	14, 16, 228	syl2anb 598	1 ⊢ ((𝑋 ∈ (0..^(♯‘𝑃)) ∧ 𝑌 ∈ (1..^4)) → (𝑋 ≠ 𝑌 → (𝑃‘𝑋) ≠ (𝑃‘𝑌)))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 395 ∨ wo 847 ∨ w3o 1085 = wceq 1541 ∈ wcel 2113 ≠ wne 2930 Vcvv 3438 ∪ cun 3897 {csn 4578 {cpr 4580 {ctp 4582 ⟨cop 4584 ‘cfv 6490 (class class class)co 7356 0cc0 11024 1c1 11025 + caddc 11027 2c2 12198 3c3 12199 4c4 12200 5c5 12201 ℕ₀cn0 12399 ℤ_≥cuz 12749 ..^cfzo 13568 ♯chash 14251 ⟨“cs4 14764 ⟨“cs5 14765

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1968 ax-7 2009 ax-8 2115 ax-9 2123 ax-10 2146 ax-11 2162 ax-12 2182 ax-ext 2706 ax-rep 5222 ax-sep 5239 ax-nul 5249 ax-pow 5308 ax-pr 5375 ax-un 7678 ax-cnex 11080 ax-resscn 11081 ax-1cn 11082 ax-icn 11083 ax-addcl 11084 ax-addrcl 11085 ax-mulcl 11086 ax-mulrcl 11087 ax-mulcom 11088 ax-addass 11089 ax-mulass 11090 ax-distr 11091 ax-i2m1 11092 ax-1ne0 11093 ax-1rid 11094 ax-rnegex 11095 ax-rrecex 11096 ax-cnre 11097 ax-pre-lttri 11098 ax-pre-lttrn 11099 ax-pre-ltadd 11100 ax-pre-mulgt0 11101

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1544 df-fal 1554 df-ex 1781 df-nf 1785 df-sb 2068 df-mo 2537 df-eu 2567 df-clab 2713 df-cleq 2726 df-clel 2809 df-nfc 2883 df-ne 2931 df-nel 3035 df-ral 3050 df-rex 3059 df-reu 3349 df-rab 3398 df-v 3440 df-sbc 3739 df-csb 3848 df-dif 3902 df-un 3904 df-in 3906 df-ss 3916 df-pss 3919 df-nul 4284 df-if 4478 df-pw 4554 df-sn 4579 df-pr 4581 df-tp 4583 df-op 4585 df-uni 4862 df-int 4901 df-iun 4946 df-br 5097 df-opab 5159 df-mpt 5178 df-tr 5204 df-id 5517 df-eprel 5522 df-po 5530 df-so 5531 df-fr 5575 df-we 5577 df-xp 5628 df-rel 5629 df-cnv 5630 df-co 5631 df-dm 5632 df-rn 5633 df-res 5634 df-ima 5635 df-pred 6257 df-ord 6318 df-on 6319 df-lim 6320 df-suc 6321 df-iota 6446 df-fun 6492 df-fn 6493 df-f 6494 df-f1 6495 df-fo 6496 df-f1o 6497 df-fv 6498 df-riota 7313 df-ov 7359 df-oprab 7360 df-mpo 7361 df-om 7807 df-1st 7931 df-2nd 7932 df-frecs 8221 df-wrecs 8252 df-recs 8301 df-rdg 8339 df-1o 8395 df-er 8633 df-en 8882 df-dom 8883 df-sdom 8884 df-fin 8885 df-card 9849 df-pnf 11166 df-mnf 11167 df-xr 11168 df-ltxr 11169 df-le 11170 df-sub 11364 df-neg 11365 df-nn 12144 df-2 12206 df-3 12207 df-4 12208 df-5 12209 df-n0 12400 df-z 12487 df-uz 12750 df-fz 13422 df-fzo 13569 df-hash 14252 df-word 14435 df-concat 14492 df-s1 14518 df-s2 14769 df-s3 14770 df-s4 14771 df-s5 14772

This theorem is referenced by: gpgprismgr4cycllem11 48293

W3C validator