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 49031

Description: Lemma 7 for gpgprismgr4cycl0 49036: 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 49028	. . . . . 6 ⊢ (♯‘𝑃) = 5
3		df-5 12352	. . . . . 6 ⊢ 5 = (4 + 1)
4	2, 3	eqtri 2783	. . . . 5 ⊢ (♯‘𝑃) = (4 + 1)
5	4	oveq2i 7426	. . . 4 ⊢ (0..^(♯‘𝑃)) = (0..^(4 + 1))
6		4nn0 12569	. . . . . 6 ⊢ 4 ∈ ℕ₀
7		elnn0uz 12950	. . . . . 6 ⊢ (4 ∈ ℕ₀ ↔ 4 ∈ (ℤ_≥‘0))
8	6, 7	mpbi 233	. . . . 5 ⊢ 4 ∈ (ℤ_≥‘0)
9		fzosplitsn 13854	. . . . 5 ⊢ (4 ∈ (ℤ_≥‘0) → (0..^(4 + 1)) = ((0..^4) ∪ {4}))
10	8, 9	ax-mp 5	. . . 4 ⊢ (0..^(4 + 1)) = ((0..^4) ∪ {4})
11		fzo0to42pr 13831	. . . . 5 ⊢ (0..^4) = ({0, 1} ∪ {2, 3})
12	11	uneq1i 4111	. . . 4 ⊢ ((0..^4) ∪ {4}) = (({0, 1} ∪ {2, 3}) ∪ {4})
13	5, 10, 12	3eqtri 2787	. . 3 ⊢ (0..^(♯‘𝑃)) = (({0, 1} ∪ {2, 3}) ∪ {4})
14	13	eleq2i 2852	. 2 ⊢ (𝑋 ∈ (0..^(♯‘𝑃)) ↔ 𝑋 ∈ (({0, 1} ∪ {2, 3}) ∪ {4}))
15		fzo1to4tp 13832	. . 3 ⊢ (1..^4) = {1, 2, 3}
16	15	eleq2i 2852	. 2 ⊢ (𝑌 ∈ (1..^4) ↔ 𝑌 ∈ {1, 2, 3})
17		elun 4100	. . . . 5 ⊢ (𝑋 ∈ (({0, 1} ∪ {2, 3}) ∪ {4}) ↔ (𝑋 ∈ ({0, 1} ∪ {2, 3}) ∨ 𝑋 ∈ {4}))
18		elun 4100	. . . . . 6 ⊢ (𝑋 ∈ ({0, 1} ∪ {2, 3}) ↔ (𝑋 ∈ {0, 1} ∨ 𝑋 ∈ {2, 3}))
19	18	orbi1i 927	. . . . 5 ⊢ ((𝑋 ∈ ({0, 1} ∪ {2, 3}) ∨ 𝑋 ∈ {4}) ↔ ((𝑋 ∈ {0, 1} ∨ 𝑋 ∈ {2, 3}) ∨ 𝑋 ∈ {4}))
20	17, 19	bitri 278	. . . 4 ⊢ (𝑋 ∈ (({0, 1} ∪ {2, 3}) ∪ {4}) ↔ ((𝑋 ∈ {0, 1} ∨ 𝑋 ∈ {2, 3}) ∨ 𝑋 ∈ {4}))
21		elpri 4608	. . . . . . 7 ⊢ (𝑋 ∈ {0, 1} → (𝑋 = 0 ∨ 𝑋 = 1))
22		0ne1 12358	. . . . . . . . . . . . . . . . 17 ⊢ 0 ≠ 1
23	22	olci 880	. . . . . . . . . . . . . . . 16 ⊢ (0 ≠ 0 ∨ 0 ≠ 1)
24		c0ex 11246	. . . . . . . . . . . . . . . . 17 ⊢ 0 ∈ V
25	24, 24	opthne 5458	. . . . . . . . . . . . . . . 16 ⊢ (⟨0, 0⟩ ≠ ⟨0, 1⟩ ↔ (0 ≠ 0 ∨ 0 ≠ 1))
26	23, 25	mpbir 234	. . . . . . . . . . . . . . 15 ⊢ ⟨0, 0⟩ ≠ ⟨0, 1⟩
27	1	fveq1i 6881	. . . . . . . . . . . . . . . . 17 ⊢ (𝑃‘0) = (⟨“⟨0, 0⟩⟨0, 1⟩⟨1, 1⟩⟨1, 0⟩⟨0, 0⟩”⟩‘0)
28		opex 5439	. . . . . . . . . . . . . . . . . 18 ⊢ ⟨0, 0⟩ ∈ V
29		df-s5 14944	. . . . . . . . . . . . . . . . . . 19 ⊢ ⟨“⟨0, 0⟩⟨0, 1⟩⟨1, 1⟩⟨1, 0⟩⟨0, 0⟩”⟩ = (⟨“⟨0, 0⟩⟨0, 1⟩⟨1, 1⟩⟨1, 0⟩”⟩ ++ ⟨“⟨0, 0⟩”⟩)
30		s4cli 14975	. . . . . . . . . . . . . . . . . . 19 ⊢ ⟨“⟨0, 0⟩⟨0, 1⟩⟨1, 1⟩⟨1, 0⟩”⟩ ∈ Word V
31		s4len 14992	. . . . . . . . . . . . . . . . . . 19 ⊢ (♯‘⟨“⟨0, 0⟩⟨0, 1⟩⟨1, 1⟩⟨1, 0⟩”⟩) = 4
32		s4fv0 14988	. . . . . . . . . . . . . . . . . . 19 ⊢ (⟨0, 0⟩ ∈ V → (⟨“⟨0, 0⟩⟨0, 1⟩⟨1, 1⟩⟨1, 0⟩”⟩‘0) = ⟨0, 0⟩)
33		0nn0 12565	. . . . . . . . . . . . . . . . . . 19 ⊢ 0 ∈ ℕ₀
34		4pos 12397	. . . . . . . . . . . . . . . . . . 19 ⊢ 0 < 4
35	29, 30, 31, 32, 33, 34	cats1fv 14952	. . . . . . . . . . . . . . . . . 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 2783	. . . . . . . . . . . . . . . 16 ⊢ (𝑃‘0) = ⟨0, 0⟩
38	1	fveq1i 6881	. . . . . . . . . . . . . . . . 17 ⊢ (𝑃‘1) = (⟨“⟨0, 0⟩⟨0, 1⟩⟨1, 1⟩⟨1, 0⟩⟨0, 0⟩”⟩‘1)
39		opex 5439	. . . . . . . . . . . . . . . . . 18 ⊢ ⟨0, 1⟩ ∈ V
40		s4fv1 14989	. . . . . . . . . . . . . . . . . . 19 ⊢ (⟨0, 1⟩ ∈ V → (⟨“⟨0, 0⟩⟨0, 1⟩⟨1, 1⟩⟨1, 0⟩”⟩‘1) = ⟨0, 1⟩)
41		1nn0 12566	. . . . . . . . . . . . . . . . . . 19 ⊢ 1 ∈ ℕ₀
42		1lt4 12465	. . . . . . . . . . . . . . . . . . 19 ⊢ 1 < 4
43	29, 30, 31, 40, 41, 42	cats1fv 14952	. . . . . . . . . . . . . . . . . 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 2783	. . . . . . . . . . . . . . . 16 ⊢ (𝑃‘1) = ⟨0, 1⟩
46	37, 45	neeq12i 3021	. . . . . . . . . . . . . . 15 ⊢ ((𝑃‘0) ≠ (𝑃‘1) ↔ ⟨0, 0⟩ ≠ ⟨0, 1⟩)
47	26, 46	mpbir 234	. . . . . . . . . . . . . 14 ⊢ (𝑃‘0) ≠ (𝑃‘1)
48	47	a1i 11	. . . . . . . . . . . . 13 ⊢ ((𝑌 = 1 ∧ 𝑋 = 0) → (𝑃‘0) ≠ (𝑃‘1))
49		fveq2 6880	. . . . . . . . . . . . . 14 ⊢ (𝑋 = 0 → (𝑃‘𝑋) = (𝑃‘0))
50	49	adantl 487	. . . . . . . . . . . . 13 ⊢ ((𝑌 = 1 ∧ 𝑋 = 0) → (𝑃‘𝑋) = (𝑃‘0))
51		fveq2 6880	. . . . . . . . . . . . . 14 ⊢ (𝑌 = 1 → (𝑃‘𝑌) = (𝑃‘1))
52	51	adantr 486	. . . . . . . . . . . . 13 ⊢ ((𝑌 = 1 ∧ 𝑋 = 0) → (𝑃‘𝑌) = (𝑃‘1))
53	48, 50, 52	3netr4d 3032	. . . . . . . . . . . 12 ⊢ ((𝑌 = 1 ∧ 𝑋 = 0) → (𝑃‘𝑋) ≠ (𝑃‘𝑌))
54	53	a1d 26	. . . . . . . . . . 11 ⊢ ((𝑌 = 1 ∧ 𝑋 = 0) → (𝑋 ≠ 𝑌 → (𝑃‘𝑋) ≠ (𝑃‘𝑌)))
55	54	ex 418	. . . . . . . . . 10 ⊢ (𝑌 = 1 → (𝑋 = 0 → (𝑋 ≠ 𝑌 → (𝑃‘𝑋) ≠ (𝑃‘𝑌))))
56	22	orci 879	. . . . . . . . . . . . . . . 16 ⊢ (0 ≠ 1 ∨ 0 ≠ 1)
57	24, 24	opthne 5458	. . . . . . . . . . . . . . . 16 ⊢ (⟨0, 0⟩ ≠ ⟨1, 1⟩ ↔ (0 ≠ 1 ∨ 0 ≠ 1))
58	56, 57	mpbir 234	. . . . . . . . . . . . . . 15 ⊢ ⟨0, 0⟩ ≠ ⟨1, 1⟩
59	1	fveq1i 6881	. . . . . . . . . . . . . . . . 17 ⊢ (𝑃‘2) = (⟨“⟨0, 0⟩⟨0, 1⟩⟨1, 1⟩⟨1, 0⟩⟨0, 0⟩”⟩‘2)
60		opex 5439	. . . . . . . . . . . . . . . . . 18 ⊢ ⟨1, 1⟩ ∈ V
61		s4fv2 14990	. . . . . . . . . . . . . . . . . . 19 ⊢ (⟨1, 1⟩ ∈ V → (⟨“⟨0, 0⟩⟨0, 1⟩⟨1, 1⟩⟨1, 0⟩”⟩‘2) = ⟨1, 1⟩)
62		2nn0 12567	. . . . . . . . . . . . . . . . . . 19 ⊢ 2 ∈ ℕ₀
63		2lt4 12464	. . . . . . . . . . . . . . . . . . 19 ⊢ 2 < 4
64	29, 30, 31, 61, 62, 63	cats1fv 14952	. . . . . . . . . . . . . . . . . 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 2783	. . . . . . . . . . . . . . . 16 ⊢ (𝑃‘2) = ⟨1, 1⟩
67	37, 66	neeq12i 3021	. . . . . . . . . . . . . . 15 ⊢ ((𝑃‘0) ≠ (𝑃‘2) ↔ ⟨0, 0⟩ ≠ ⟨1, 1⟩)
68	58, 67	mpbir 234	. . . . . . . . . . . . . 14 ⊢ (𝑃‘0) ≠ (𝑃‘2)
69	68	a1i 11	. . . . . . . . . . . . 13 ⊢ ((𝑌 = 2 ∧ 𝑋 = 0) → (𝑃‘0) ≠ (𝑃‘2))
70	49	adantl 487	. . . . . . . . . . . . 13 ⊢ ((𝑌 = 2 ∧ 𝑋 = 0) → (𝑃‘𝑋) = (𝑃‘0))
71		fveq2 6880	. . . . . . . . . . . . . 14 ⊢ (𝑌 = 2 → (𝑃‘𝑌) = (𝑃‘2))
72	71	adantr 486	. . . . . . . . . . . . 13 ⊢ ((𝑌 = 2 ∧ 𝑋 = 0) → (𝑃‘𝑌) = (𝑃‘2))
73	69, 70, 72	3netr4d 3032	. . . . . . . . . . . 12 ⊢ ((𝑌 = 2 ∧ 𝑋 = 0) → (𝑃‘𝑋) ≠ (𝑃‘𝑌))
74	73	a1d 26	. . . . . . . . . . 11 ⊢ ((𝑌 = 2 ∧ 𝑋 = 0) → (𝑋 ≠ 𝑌 → (𝑃‘𝑋) ≠ (𝑃‘𝑌)))
75	74	ex 418	. . . . . . . . . 10 ⊢ (𝑌 = 2 → (𝑋 = 0 → (𝑋 ≠ 𝑌 → (𝑃‘𝑋) ≠ (𝑃‘𝑌))))
76	22	orci 879	. . . . . . . . . . . . . . . 16 ⊢ (0 ≠ 1 ∨ 0 ≠ 0)
77	24, 24	opthne 5458	. . . . . . . . . . . . . . . 16 ⊢ (⟨0, 0⟩ ≠ ⟨1, 0⟩ ↔ (0 ≠ 1 ∨ 0 ≠ 0))
78	76, 77	mpbir 234	. . . . . . . . . . . . . . 15 ⊢ ⟨0, 0⟩ ≠ ⟨1, 0⟩
79	1	fveq1i 6881	. . . . . . . . . . . . . . . . 17 ⊢ (𝑃‘3) = (⟨“⟨0, 0⟩⟨0, 1⟩⟨1, 1⟩⟨1, 0⟩⟨0, 0⟩”⟩‘3)
80		opex 5439	. . . . . . . . . . . . . . . . . 18 ⊢ ⟨1, 0⟩ ∈ V
81		s4fv3 14991	. . . . . . . . . . . . . . . . . . 19 ⊢ (⟨1, 0⟩ ∈ V → (⟨“⟨0, 0⟩⟨0, 1⟩⟨1, 1⟩⟨1, 0⟩”⟩‘3) = ⟨1, 0⟩)
82		3nn0 12568	. . . . . . . . . . . . . . . . . . 19 ⊢ 3 ∈ ℕ₀
83		3lt4 12463	. . . . . . . . . . . . . . . . . . 19 ⊢ 3 < 4
84	29, 30, 31, 81, 82, 83	cats1fv 14952	. . . . . . . . . . . . . . . . . 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 2783	. . . . . . . . . . . . . . . 16 ⊢ (𝑃‘3) = ⟨1, 0⟩
87	37, 86	neeq12i 3021	. . . . . . . . . . . . . . 15 ⊢ ((𝑃‘0) ≠ (𝑃‘3) ↔ ⟨0, 0⟩ ≠ ⟨1, 0⟩)
88	78, 87	mpbir 234	. . . . . . . . . . . . . 14 ⊢ (𝑃‘0) ≠ (𝑃‘3)
89	88	a1i 11	. . . . . . . . . . . . 13 ⊢ ((𝑌 = 3 ∧ 𝑋 = 0) → (𝑃‘0) ≠ (𝑃‘3))
90	49	adantl 487	. . . . . . . . . . . . 13 ⊢ ((𝑌 = 3 ∧ 𝑋 = 0) → (𝑃‘𝑋) = (𝑃‘0))
91		fveq2 6880	. . . . . . . . . . . . . 14 ⊢ (𝑌 = 3 → (𝑃‘𝑌) = (𝑃‘3))
92	91	adantr 486	. . . . . . . . . . . . 13 ⊢ ((𝑌 = 3 ∧ 𝑋 = 0) → (𝑃‘𝑌) = (𝑃‘3))
93	89, 90, 92	3netr4d 3032	. . . . . . . . . . . 12 ⊢ ((𝑌 = 3 ∧ 𝑋 = 0) → (𝑃‘𝑋) ≠ (𝑃‘𝑌))
94	93	a1d 26	. . . . . . . . . . 11 ⊢ ((𝑌 = 3 ∧ 𝑋 = 0) → (𝑋 ≠ 𝑌 → (𝑃‘𝑋) ≠ (𝑃‘𝑌)))
95	94	ex 418	. . . . . . . . . 10 ⊢ (𝑌 = 3 → (𝑋 = 0 → (𝑋 ≠ 𝑌 → (𝑃‘𝑋) ≠ (𝑃‘𝑌))))
96	55, 75, 95	3jaoi 1454	. . . . . . . . 9 ⊢ ((𝑌 = 1 ∨ 𝑌 = 2 ∨ 𝑌 = 3) → (𝑋 = 0 → (𝑋 ≠ 𝑌 → (𝑃‘𝑋) ≠ (𝑃‘𝑌))))
97		eltpi 4649	. . . . . . . . 9 ⊢ (𝑌 ∈ {1, 2, 3} → (𝑌 = 1 ∨ 𝑌 = 2 ∨ 𝑌 = 3))
98	96, 97	syl11 34	. . . . . . . 8 ⊢ (𝑋 = 0 → (𝑌 ∈ {1, 2, 3} → (𝑋 ≠ 𝑌 → (𝑃‘𝑋) ≠ (𝑃‘𝑌))))
99		simpr 490	. . . . . . . . . . . . 13 ⊢ ((𝑌 = 1 ∧ 𝑋 = 1) → 𝑋 = 1)
100		simpl 488	. . . . . . . . . . . . 13 ⊢ ((𝑌 = 1 ∧ 𝑋 = 1) → 𝑌 = 1)
101	99, 100	neeq12d 3016	. . . . . . . . . . . 12 ⊢ ((𝑌 = 1 ∧ 𝑋 = 1) → (𝑋 ≠ 𝑌 ↔ 1 ≠ 1))
102		eqid 2760	. . . . . . . . . . . . 13 ⊢ 1 = 1
103		eqneqall 2966	. . . . . . . . . . . . 13 ⊢ (1 = 1 → (1 ≠ 1 → (𝑃‘𝑋) ≠ (𝑃‘𝑌)))
104	102, 103	ax-mp 5	. . . . . . . . . . . 12 ⊢ (1 ≠ 1 → (𝑃‘𝑋) ≠ (𝑃‘𝑌))
105	101, 104	biimtrdi 256	. . . . . . . . . . 11 ⊢ ((𝑌 = 1 ∧ 𝑋 = 1) → (𝑋 ≠ 𝑌 → (𝑃‘𝑋) ≠ (𝑃‘𝑌)))
106	105	ex 418	. . . . . . . . . 10 ⊢ (𝑌 = 1 → (𝑋 = 1 → (𝑋 ≠ 𝑌 → (𝑃‘𝑋) ≠ (𝑃‘𝑌))))
107	22	orci 879	. . . . . . . . . . . . . . . 16 ⊢ (0 ≠ 1 ∨ 1 ≠ 1)
108		1ex 11249	. . . . . . . . . . . . . . . . 17 ⊢ 1 ∈ V
109	24, 108	opthne 5458	. . . . . . . . . . . . . . . 16 ⊢ (⟨0, 1⟩ ≠ ⟨1, 1⟩ ↔ (0 ≠ 1 ∨ 1 ≠ 1))
110	107, 109	mpbir 234	. . . . . . . . . . . . . . 15 ⊢ ⟨0, 1⟩ ≠ ⟨1, 1⟩
111	45, 66	neeq12i 3021	. . . . . . . . . . . . . . 15 ⊢ ((𝑃‘1) ≠ (𝑃‘2) ↔ ⟨0, 1⟩ ≠ ⟨1, 1⟩)
112	110, 111	mpbir 234	. . . . . . . . . . . . . 14 ⊢ (𝑃‘1) ≠ (𝑃‘2)
113	112	a1i 11	. . . . . . . . . . . . 13 ⊢ ((𝑌 = 2 ∧ 𝑋 = 1) → (𝑃‘1) ≠ (𝑃‘2))
114		fveq2 6880	. . . . . . . . . . . . . 14 ⊢ (𝑋 = 1 → (𝑃‘𝑋) = (𝑃‘1))
115	114	adantl 487	. . . . . . . . . . . . 13 ⊢ ((𝑌 = 2 ∧ 𝑋 = 1) → (𝑃‘𝑋) = (𝑃‘1))
116	71	adantr 486	. . . . . . . . . . . . 13 ⊢ ((𝑌 = 2 ∧ 𝑋 = 1) → (𝑃‘𝑌) = (𝑃‘2))
117	113, 115, 116	3netr4d 3032	. . . . . . . . . . . 12 ⊢ ((𝑌 = 2 ∧ 𝑋 = 1) → (𝑃‘𝑋) ≠ (𝑃‘𝑌))
118	117	a1d 26	. . . . . . . . . . 11 ⊢ ((𝑌 = 2 ∧ 𝑋 = 1) → (𝑋 ≠ 𝑌 → (𝑃‘𝑋) ≠ (𝑃‘𝑌)))
119	118	ex 418	. . . . . . . . . 10 ⊢ (𝑌 = 2 → (𝑋 = 1 → (𝑋 ≠ 𝑌 → (𝑃‘𝑋) ≠ (𝑃‘𝑌))))
120	22	orci 879	. . . . . . . . . . . . . . . 16 ⊢ (0 ≠ 1 ∨ 1 ≠ 0)
121	24, 108	opthne 5458	. . . . . . . . . . . . . . . 16 ⊢ (⟨0, 1⟩ ≠ ⟨1, 0⟩ ↔ (0 ≠ 1 ∨ 1 ≠ 0))
122	120, 121	mpbir 234	. . . . . . . . . . . . . . 15 ⊢ ⟨0, 1⟩ ≠ ⟨1, 0⟩
123	45, 86	neeq12i 3021	. . . . . . . . . . . . . . 15 ⊢ ((𝑃‘1) ≠ (𝑃‘3) ↔ ⟨0, 1⟩ ≠ ⟨1, 0⟩)
124	122, 123	mpbir 234	. . . . . . . . . . . . . 14 ⊢ (𝑃‘1) ≠ (𝑃‘3)
125	124	a1i 11	. . . . . . . . . . . . 13 ⊢ ((𝑌 = 3 ∧ 𝑋 = 1) → (𝑃‘1) ≠ (𝑃‘3))
126	114	adantl 487	. . . . . . . . . . . . 13 ⊢ ((𝑌 = 3 ∧ 𝑋 = 1) → (𝑃‘𝑋) = (𝑃‘1))
127	91	adantr 486	. . . . . . . . . . . . 13 ⊢ ((𝑌 = 3 ∧ 𝑋 = 1) → (𝑃‘𝑌) = (𝑃‘3))
128	125, 126, 127	3netr4d 3032	. . . . . . . . . . . 12 ⊢ ((𝑌 = 3 ∧ 𝑋 = 1) → (𝑃‘𝑋) ≠ (𝑃‘𝑌))
129	128	a1d 26	. . . . . . . . . . 11 ⊢ ((𝑌 = 3 ∧ 𝑋 = 1) → (𝑋 ≠ 𝑌 → (𝑃‘𝑋) ≠ (𝑃‘𝑌)))
130	129	ex 418	. . . . . . . . . 10 ⊢ (𝑌 = 3 → (𝑋 = 1 → (𝑋 ≠ 𝑌 → (𝑃‘𝑋) ≠ (𝑃‘𝑌))))
131	106, 119, 130	3jaoi 1454	. . . . . . . . 9 ⊢ ((𝑌 = 1 ∨ 𝑌 = 2 ∨ 𝑌 = 3) → (𝑋 = 1 → (𝑋 ≠ 𝑌 → (𝑃‘𝑋) ≠ (𝑃‘𝑌))))
132	131, 97	syl11 34	. . . . . . . 8 ⊢ (𝑋 = 1 → (𝑌 ∈ {1, 2, 3} → (𝑋 ≠ 𝑌 → (𝑃‘𝑋) ≠ (𝑃‘𝑌))))
133	98, 132	jaoi 871	. . . . . . 7 ⊢ ((𝑋 = 0 ∨ 𝑋 = 1) → (𝑌 ∈ {1, 2, 3} → (𝑋 ≠ 𝑌 → (𝑃‘𝑋) ≠ (𝑃‘𝑌))))
134	21, 133	syl 18	. . . . . 6 ⊢ (𝑋 ∈ {0, 1} → (𝑌 ∈ {1, 2, 3} → (𝑋 ≠ 𝑌 → (𝑃‘𝑋) ≠ (𝑃‘𝑌))))
135		elpri 4608	. . . . . . 7 ⊢ (𝑋 ∈ {2, 3} → (𝑋 = 2 ∨ 𝑋 = 3))
136	112	necomi 3009	. . . . . . . . . . . . . 14 ⊢ (𝑃‘2) ≠ (𝑃‘1)
137	136	a1i 11	. . . . . . . . . . . . 13 ⊢ ((𝑌 = 1 ∧ 𝑋 = 2) → (𝑃‘2) ≠ (𝑃‘1))
138		fveq2 6880	. . . . . . . . . . . . . 14 ⊢ (𝑋 = 2 → (𝑃‘𝑋) = (𝑃‘2))
139	138	adantl 487	. . . . . . . . . . . . 13 ⊢ ((𝑌 = 1 ∧ 𝑋 = 2) → (𝑃‘𝑋) = (𝑃‘2))
140	51	adantr 486	. . . . . . . . . . . . 13 ⊢ ((𝑌 = 1 ∧ 𝑋 = 2) → (𝑃‘𝑌) = (𝑃‘1))
141	137, 139, 140	3netr4d 3032	. . . . . . . . . . . 12 ⊢ ((𝑌 = 1 ∧ 𝑋 = 2) → (𝑃‘𝑋) ≠ (𝑃‘𝑌))
142	141	a1d 26	. . . . . . . . . . 11 ⊢ ((𝑌 = 1 ∧ 𝑋 = 2) → (𝑋 ≠ 𝑌 → (𝑃‘𝑋) ≠ (𝑃‘𝑌)))
143	142	ex 418	. . . . . . . . . 10 ⊢ (𝑌 = 1 → (𝑋 = 2 → (𝑋 ≠ 𝑌 → (𝑃‘𝑋) ≠ (𝑃‘𝑌))))
144		simpr 490	. . . . . . . . . . . . 13 ⊢ ((𝑌 = 2 ∧ 𝑋 = 2) → 𝑋 = 2)
145		simpl 488	. . . . . . . . . . . . 13 ⊢ ((𝑌 = 2 ∧ 𝑋 = 2) → 𝑌 = 2)
146	144, 145	neeq12d 3016	. . . . . . . . . . . 12 ⊢ ((𝑌 = 2 ∧ 𝑋 = 2) → (𝑋 ≠ 𝑌 ↔ 2 ≠ 2))
147		eqid 2760	. . . . . . . . . . . . 13 ⊢ 2 = 2
148		eqneqall 2966	. . . . . . . . . . . . 13 ⊢ (2 = 2 → (2 ≠ 2 → (𝑃‘𝑋) ≠ (𝑃‘𝑌)))
149	147, 148	ax-mp 5	. . . . . . . . . . . 12 ⊢ (2 ≠ 2 → (𝑃‘𝑋) ≠ (𝑃‘𝑌))
150	146, 149	biimtrdi 256	. . . . . . . . . . 11 ⊢ ((𝑌 = 2 ∧ 𝑋 = 2) → (𝑋 ≠ 𝑌 → (𝑃‘𝑋) ≠ (𝑃‘𝑌)))
151	150	ex 418	. . . . . . . . . 10 ⊢ (𝑌 = 2 → (𝑋 = 2 → (𝑋 ≠ 𝑌 → (𝑃‘𝑋) ≠ (𝑃‘𝑌))))
152	22	necomi 3009	. . . . . . . . . . . . . . . . 17 ⊢ 1 ≠ 0
153	152	olci 880	. . . . . . . . . . . . . . . 16 ⊢ (1 ≠ 1 ∨ 1 ≠ 0)
154	108, 108	opthne 5458	. . . . . . . . . . . . . . . 16 ⊢ (⟨1, 1⟩ ≠ ⟨1, 0⟩ ↔ (1 ≠ 1 ∨ 1 ≠ 0))
155	153, 154	mpbir 234	. . . . . . . . . . . . . . 15 ⊢ ⟨1, 1⟩ ≠ ⟨1, 0⟩
156	66, 86	neeq12i 3021	. . . . . . . . . . . . . . 15 ⊢ ((𝑃‘2) ≠ (𝑃‘3) ↔ ⟨1, 1⟩ ≠ ⟨1, 0⟩)
157	155, 156	mpbir 234	. . . . . . . . . . . . . 14 ⊢ (𝑃‘2) ≠ (𝑃‘3)
158	157	a1i 11	. . . . . . . . . . . . 13 ⊢ ((𝑌 = 3 ∧ 𝑋 = 2) → (𝑃‘2) ≠ (𝑃‘3))
159	138	adantl 487	. . . . . . . . . . . . 13 ⊢ ((𝑌 = 3 ∧ 𝑋 = 2) → (𝑃‘𝑋) = (𝑃‘2))
160	91	adantr 486	. . . . . . . . . . . . 13 ⊢ ((𝑌 = 3 ∧ 𝑋 = 2) → (𝑃‘𝑌) = (𝑃‘3))
161	158, 159, 160	3netr4d 3032	. . . . . . . . . . . 12 ⊢ ((𝑌 = 3 ∧ 𝑋 = 2) → (𝑃‘𝑋) ≠ (𝑃‘𝑌))
162	161	a1d 26	. . . . . . . . . . 11 ⊢ ((𝑌 = 3 ∧ 𝑋 = 2) → (𝑋 ≠ 𝑌 → (𝑃‘𝑋) ≠ (𝑃‘𝑌)))
163	162	ex 418	. . . . . . . . . 10 ⊢ (𝑌 = 3 → (𝑋 = 2 → (𝑋 ≠ 𝑌 → (𝑃‘𝑋) ≠ (𝑃‘𝑌))))
164	143, 151, 163	3jaoi 1454	. . . . . . . . 9 ⊢ ((𝑌 = 1 ∨ 𝑌 = 2 ∨ 𝑌 = 3) → (𝑋 = 2 → (𝑋 ≠ 𝑌 → (𝑃‘𝑋) ≠ (𝑃‘𝑌))))
165	164, 97	syl11 34	. . . . . . . 8 ⊢ (𝑋 = 2 → (𝑌 ∈ {1, 2, 3} → (𝑋 ≠ 𝑌 → (𝑃‘𝑋) ≠ (𝑃‘𝑌))))
166	124	necomi 3009	. . . . . . . . . . . . . 14 ⊢ (𝑃‘3) ≠ (𝑃‘1)
167	166	a1i 11	. . . . . . . . . . . . 13 ⊢ ((𝑌 = 1 ∧ 𝑋 = 3) → (𝑃‘3) ≠ (𝑃‘1))
168		fveq2 6880	. . . . . . . . . . . . . 14 ⊢ (𝑋 = 3 → (𝑃‘𝑋) = (𝑃‘3))
169	168	adantl 487	. . . . . . . . . . . . 13 ⊢ ((𝑌 = 1 ∧ 𝑋 = 3) → (𝑃‘𝑋) = (𝑃‘3))
170	51	adantr 486	. . . . . . . . . . . . 13 ⊢ ((𝑌 = 1 ∧ 𝑋 = 3) → (𝑃‘𝑌) = (𝑃‘1))
171	167, 169, 170	3netr4d 3032	. . . . . . . . . . . 12 ⊢ ((𝑌 = 1 ∧ 𝑋 = 3) → (𝑃‘𝑋) ≠ (𝑃‘𝑌))
172	171	a1d 26	. . . . . . . . . . 11 ⊢ ((𝑌 = 1 ∧ 𝑋 = 3) → (𝑋 ≠ 𝑌 → (𝑃‘𝑋) ≠ (𝑃‘𝑌)))
173	172	ex 418	. . . . . . . . . 10 ⊢ (𝑌 = 1 → (𝑋 = 3 → (𝑋 ≠ 𝑌 → (𝑃‘𝑋) ≠ (𝑃‘𝑌))))
174	157	necomi 3009	. . . . . . . . . . . . . 14 ⊢ (𝑃‘3) ≠ (𝑃‘2)
175	174	a1i 11	. . . . . . . . . . . . 13 ⊢ ((𝑌 = 2 ∧ 𝑋 = 3) → (𝑃‘3) ≠ (𝑃‘2))
176	168	adantl 487	. . . . . . . . . . . . 13 ⊢ ((𝑌 = 2 ∧ 𝑋 = 3) → (𝑃‘𝑋) = (𝑃‘3))
177	71	adantr 486	. . . . . . . . . . . . 13 ⊢ ((𝑌 = 2 ∧ 𝑋 = 3) → (𝑃‘𝑌) = (𝑃‘2))
178	175, 176, 177	3netr4d 3032	. . . . . . . . . . . 12 ⊢ ((𝑌 = 2 ∧ 𝑋 = 3) → (𝑃‘𝑋) ≠ (𝑃‘𝑌))
179	178	a1d 26	. . . . . . . . . . 11 ⊢ ((𝑌 = 2 ∧ 𝑋 = 3) → (𝑋 ≠ 𝑌 → (𝑃‘𝑋) ≠ (𝑃‘𝑌)))
180	179	ex 418	. . . . . . . . . 10 ⊢ (𝑌 = 2 → (𝑋 = 3 → (𝑋 ≠ 𝑌 → (𝑃‘𝑋) ≠ (𝑃‘𝑌))))
181		simpr 490	. . . . . . . . . . . . 13 ⊢ ((𝑌 = 3 ∧ 𝑋 = 3) → 𝑋 = 3)
182		simpl 488	. . . . . . . . . . . . 13 ⊢ ((𝑌 = 3 ∧ 𝑋 = 3) → 𝑌 = 3)
183	181, 182	neeq12d 3016	. . . . . . . . . . . 12 ⊢ ((𝑌 = 3 ∧ 𝑋 = 3) → (𝑋 ≠ 𝑌 ↔ 3 ≠ 3))
184		eqid 2760	. . . . . . . . . . . . 13 ⊢ 3 = 3
185		eqneqall 2966	. . . . . . . . . . . . 13 ⊢ (3 = 3 → (3 ≠ 3 → (𝑃‘𝑋) ≠ (𝑃‘𝑌)))
186	184, 185	ax-mp 5	. . . . . . . . . . . 12 ⊢ (3 ≠ 3 → (𝑃‘𝑋) ≠ (𝑃‘𝑌))
187	183, 186	biimtrdi 256	. . . . . . . . . . 11 ⊢ ((𝑌 = 3 ∧ 𝑋 = 3) → (𝑋 ≠ 𝑌 → (𝑃‘𝑋) ≠ (𝑃‘𝑌)))
188	187	ex 418	. . . . . . . . . 10 ⊢ (𝑌 = 3 → (𝑋 = 3 → (𝑋 ≠ 𝑌 → (𝑃‘𝑋) ≠ (𝑃‘𝑌))))
189	173, 180, 188	3jaoi 1454	. . . . . . . . 9 ⊢ ((𝑌 = 1 ∨ 𝑌 = 2 ∨ 𝑌 = 3) → (𝑋 = 3 → (𝑋 ≠ 𝑌 → (𝑃‘𝑋) ≠ (𝑃‘𝑌))))
190	189, 97	syl11 34	. . . . . . . 8 ⊢ (𝑋 = 3 → (𝑌 ∈ {1, 2, 3} → (𝑋 ≠ 𝑌 → (𝑃‘𝑋) ≠ (𝑃‘𝑌))))
191	165, 190	jaoi 871	. . . . . . 7 ⊢ ((𝑋 = 2 ∨ 𝑋 = 3) → (𝑌 ∈ {1, 2, 3} → (𝑋 ≠ 𝑌 → (𝑃‘𝑋) ≠ (𝑃‘𝑌))))
192	135, 191	syl 18	. . . . . 6 ⊢ (𝑋 ∈ {2, 3} → (𝑌 ∈ {1, 2, 3} → (𝑋 ≠ 𝑌 → (𝑃‘𝑋) ≠ (𝑃‘𝑌))))
193	134, 192	jaoi 871	. . . . 5 ⊢ ((𝑋 ∈ {0, 1} ∨ 𝑋 ∈ {2, 3}) → (𝑌 ∈ {1, 2, 3} → (𝑋 ≠ 𝑌 → (𝑃‘𝑋) ≠ (𝑃‘𝑌))))
194		elsni 4601	. . . . . 6 ⊢ (𝑋 ∈ {4} → 𝑋 = 4)
195	1	fveq1i 6881	. . . . . . . . . . . . . 14 ⊢ (𝑃‘4) = (⟨“⟨0, 0⟩⟨0, 1⟩⟨1, 1⟩⟨1, 0⟩⟨0, 0⟩”⟩‘4)
196	29, 30, 31	cats1fvn 14951	. . . . . . . . . . . . . . 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 2783	. . . . . . . . . . . . 13 ⊢ (𝑃‘4) = ⟨0, 0⟩
199	198, 45	neeq12i 3021	. . . . . . . . . . . 12 ⊢ ((𝑃‘4) ≠ (𝑃‘1) ↔ ⟨0, 0⟩ ≠ ⟨0, 1⟩)
200	26, 199	mpbir 234	. . . . . . . . . . 11 ⊢ (𝑃‘4) ≠ (𝑃‘1)
201	200	a1i 11	. . . . . . . . . 10 ⊢ ((𝑌 = 1 ∧ 𝑋 = 4) → (𝑃‘4) ≠ (𝑃‘1))
202		fveq2 6880	. . . . . . . . . . 11 ⊢ (𝑋 = 4 → (𝑃‘𝑋) = (𝑃‘4))
203	202	adantl 487	. . . . . . . . . 10 ⊢ ((𝑌 = 1 ∧ 𝑋 = 4) → (𝑃‘𝑋) = (𝑃‘4))
204	51	adantr 486	. . . . . . . . . 10 ⊢ ((𝑌 = 1 ∧ 𝑋 = 4) → (𝑃‘𝑌) = (𝑃‘1))
205	201, 203, 204	3netr4d 3032	. . . . . . . . 9 ⊢ ((𝑌 = 1 ∧ 𝑋 = 4) → (𝑃‘𝑋) ≠ (𝑃‘𝑌))
206	205	a1d 26	. . . . . . . 8 ⊢ ((𝑌 = 1 ∧ 𝑋 = 4) → (𝑋 ≠ 𝑌 → (𝑃‘𝑋) ≠ (𝑃‘𝑌)))
207	206	ex 418	. . . . . . 7 ⊢ (𝑌 = 1 → (𝑋 = 4 → (𝑋 ≠ 𝑌 → (𝑃‘𝑋) ≠ (𝑃‘𝑌))))
208	198, 66	neeq12i 3021	. . . . . . . . . . . 12 ⊢ ((𝑃‘4) ≠ (𝑃‘2) ↔ ⟨0, 0⟩ ≠ ⟨1, 1⟩)
209	58, 208	mpbir 234	. . . . . . . . . . 11 ⊢ (𝑃‘4) ≠ (𝑃‘2)
210	209	a1i 11	. . . . . . . . . 10 ⊢ ((𝑌 = 2 ∧ 𝑋 = 4) → (𝑃‘4) ≠ (𝑃‘2))
211	202	adantl 487	. . . . . . . . . 10 ⊢ ((𝑌 = 2 ∧ 𝑋 = 4) → (𝑃‘𝑋) = (𝑃‘4))
212	71	adantr 486	. . . . . . . . . 10 ⊢ ((𝑌 = 2 ∧ 𝑋 = 4) → (𝑃‘𝑌) = (𝑃‘2))
213	210, 211, 212	3netr4d 3032	. . . . . . . . 9 ⊢ ((𝑌 = 2 ∧ 𝑋 = 4) → (𝑃‘𝑋) ≠ (𝑃‘𝑌))
214	213	a1d 26	. . . . . . . 8 ⊢ ((𝑌 = 2 ∧ 𝑋 = 4) → (𝑋 ≠ 𝑌 → (𝑃‘𝑋) ≠ (𝑃‘𝑌)))
215	214	ex 418	. . . . . . 7 ⊢ (𝑌 = 2 → (𝑋 = 4 → (𝑋 ≠ 𝑌 → (𝑃‘𝑋) ≠ (𝑃‘𝑌))))
216	198, 86	neeq12i 3021	. . . . . . . . . . . 12 ⊢ ((𝑃‘4) ≠ (𝑃‘3) ↔ ⟨0, 0⟩ ≠ ⟨1, 0⟩)
217	78, 216	mpbir 234	. . . . . . . . . . 11 ⊢ (𝑃‘4) ≠ (𝑃‘3)
218	217	a1i 11	. . . . . . . . . 10 ⊢ ((𝑌 = 3 ∧ 𝑋 = 4) → (𝑃‘4) ≠ (𝑃‘3))
219	202	adantl 487	. . . . . . . . . 10 ⊢ ((𝑌 = 3 ∧ 𝑋 = 4) → (𝑃‘𝑋) = (𝑃‘4))
220	91	adantr 486	. . . . . . . . . 10 ⊢ ((𝑌 = 3 ∧ 𝑋 = 4) → (𝑃‘𝑌) = (𝑃‘3))
221	218, 219, 220	3netr4d 3032	. . . . . . . . 9 ⊢ ((𝑌 = 3 ∧ 𝑋 = 4) → (𝑃‘𝑋) ≠ (𝑃‘𝑌))
222	221	a1d 26	. . . . . . . 8 ⊢ ((𝑌 = 3 ∧ 𝑋 = 4) → (𝑋 ≠ 𝑌 → (𝑃‘𝑋) ≠ (𝑃‘𝑌)))
223	222	ex 418	. . . . . . 7 ⊢ (𝑌 = 3 → (𝑋 = 4 → (𝑋 ≠ 𝑌 → (𝑃‘𝑋) ≠ (𝑃‘𝑌))))
224	207, 215, 223	3jaoi 1454	. . . . . 6 ⊢ ((𝑌 = 1 ∨ 𝑌 = 2 ∨ 𝑌 = 3) → (𝑋 = 4 → (𝑋 ≠ 𝑌 → (𝑃‘𝑋) ≠ (𝑃‘𝑌))))
225	97, 194, 224	syl2imc 42	. . . . 5 ⊢ (𝑋 ∈ {4} → (𝑌 ∈ {1, 2, 3} → (𝑋 ≠ 𝑌 → (𝑃‘𝑋) ≠ (𝑃‘𝑌))))
226	193, 225	jaoi 871	. . . 4 ⊢ (((𝑋 ∈ {0, 1} ∨ 𝑋 ∈ {2, 3}) ∨ 𝑋 ∈ {4}) → (𝑌 ∈ {1, 2, 3} → (𝑋 ≠ 𝑌 → (𝑃‘𝑋) ≠ (𝑃‘𝑌))))
227	20, 226	sylbi 220	. . 3 ⊢ (𝑋 ∈ (({0, 1} ∪ {2, 3}) ∪ {4}) → (𝑌 ∈ {1, 2, 3} → (𝑋 ≠ 𝑌 → (𝑃‘𝑋) ≠ (𝑃‘𝑌))))
228	227	imp 412	. 2 ⊢ ((𝑋 ∈ (({0, 1} ∪ {2, 3}) ∪ {4}) ∧ 𝑌 ∈ {1, 2, 3}) → (𝑋 ≠ 𝑌 → (𝑃‘𝑋) ≠ (𝑃‘𝑌)))
229	14, 16, 228	syl2anb 610	1 ⊢ ((𝑋 ∈ (0..^(♯‘𝑃)) ∧ 𝑌 ∈ (1..^4)) → (𝑋 ≠ 𝑌 → (𝑃‘𝑋) ≠ (𝑃‘𝑌)))

Colors of variables: wff setvar class

This proof depends on syntax axioms: → wi 4 ∧ wa 401 ∨ wo 861 ∨ w3o 1102 = wceq 1570 ∈ wcel 2145 ≠ wne 2955 Vcvv 3450 ∪ cun 3897 {csn 4584 {cpr 4586 {ctp 4588 ⟨cop 4590 ‘cfv 6534 (class class class)co 7415 0cc0 11146 1c1 11147 + caddc 11149 2c2 12341 3c3 12342 4c4 12343 5c5 12344 ℕ₀cn0 12550 ℤ_≥cuz 12909 ..^cfzo 13731 ♯chash 14416 ⟨“cs4 14936 ⟨“cs5 14937

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1943 ax-6 2000 ax-7 2041 ax-8 2147 ax-9 2155 ax-10 2178 ax-11 2194 ax-12 2213 ax-ext 2732 ax-rep 5232 ax-sep 5251 ax-nul 5263 ax-pow 5330 ax-pr 5398 ax-un 7738 ax-cnex 11202 ax-resscn 11203 ax-1cn 11204 ax-icn 11205 ax-addcl 11206 ax-addrcl 11207 ax-mulcl 11208 ax-mulrcl 11209 ax-mulcom 11210 ax-addass 11211 ax-mulass 11212 ax-distr 11213 ax-i2m1 11214 ax-1ne0 11215 ax-1rid 11216 ax-rnegex 11217 ax-rrecex 11218 ax-cnre 11219 ax-pre-lttri 11220 ax-pre-lttrn 11221 ax-pre-ltadd 11222 ax-pre-mulgt0 11223

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2100 df-mo 2564 df-eu 2594 df-clab 2739 df-cleq 2752 df-clel 2835 df-nfc 2909 df-ne 2956 df-nel 3062 df-ral 3077 df-rex 3087 df-reu 3366 df-rab 3413 df-v 3452 df-sbc 3740 df-csb 3848 df-dif 3902 df-un 3904 df-in 3906 df-ss 3916 df-pss 3919 df-nul 4280 df-if 4483 df-pw 4559 df-sn 4585 df-pr 4587 df-tp 4589 df-op 4591 df-uni 4868 df-int 4908 df-iun 4953 df-br 5104 df-opab 5168 df-mpt 5187 df-tr 5213 df-id 5550 df-eprel 5555 df-po 5563 df-so 5564 df-fr 5608 df-we 5610 df-xp 5661 df-rel 5662 df-cnv 5663 df-co 5664 df-dm 5665 df-rn 5666 df-res 5667 df-ima 5668 df-pred 6300 df-ord 6361 df-on 6362 df-lim 6363 df-suc 6364 df-iota 6490 df-fun 6536 df-fn 6537 df-f 6538 df-f1 6539 df-fo 6540 df-f1o 6541 df-fv 6542 df-riota 7372 df-ov 7418 df-oprab 7419 df-mpo 7420 df-om 7865 df-1st 7988 df-2nd 7989 df-frecs 8282 df-wrecs 8313 df-recs 8362 df-rdg 8401 df-1o 8459 df-er 8700 df-en 8957 df-dom 8958 df-sdom 8959 df-fin 8960 df-card 9966 df-pnf 11291 df-mnf 11292 df-xr 11293 df-ltxr 11294 df-le 11295 df-sub 11489 df-neg 11490 df-nn 12280 df-2 12349 df-3 12350 df-4 12351 df-5 12352 df-n0 12551 df-z 12638 df-uz 12910 df-fz 13584 df-fzo 13732 df-hash 14417 df-word 14601 df-concat 14658 df-s1 14685 df-s2 14941 df-s3 14942 df-s4 14943 df-s5 14944

This theorem is used by: gpgprismgr4cycllem11 49035

W3C validator