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 48944

Description: Lemma 7 for gpgprismgr4cycl0 48949: 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 48941	. . . . . 6 ⊢ (♯‘𝑃) = 5
3		df-5 12326	. . . . . 6 ⊢ 5 = (4 + 1)
4	2, 3	eqtri 2788	. . . . 5 ⊢ (♯‘𝑃) = (4 + 1)
5	4	oveq2i 7431	. . . 4 ⊢ (0..^(♯‘𝑃)) = (0..^(4 + 1))
6		4nn0 12543	. . . . . 6 ⊢ 4 ∈ ℕ₀
7		elnn0uz 12924	. . . . . 6 ⊢ (4 ∈ ℕ₀ ↔ 4 ∈ (ℤ_≥‘0))
8	6, 7	mpbi 233	. . . . 5 ⊢ 4 ∈ (ℤ_≥‘0)
9		fzosplitsn 13827	. . . . 5 ⊢ (4 ∈ (ℤ_≥‘0) → (0..^(4 + 1)) = ((0..^4) ∪ {4}))
10	8, 9	ax-mp 5	. . . 4 ⊢ (0..^(4 + 1)) = ((0..^4) ∪ {4})
11		fzo0to42pr 13804	. . . . 5 ⊢ (0..^4) = ({0, 1} ∪ {2, 3})
12	11	uneq1i 4118	. . . 4 ⊢ ((0..^4) ∪ {4}) = (({0, 1} ∪ {2, 3}) ∪ {4})
13	5, 10, 12	3eqtri 2792	. . 3 ⊢ (0..^(♯‘𝑃)) = (({0, 1} ∪ {2, 3}) ∪ {4})
14	13	eleq2i 2857	. 2 ⊢ (𝑋 ∈ (0..^(♯‘𝑃)) ↔ 𝑋 ∈ (({0, 1} ∪ {2, 3}) ∪ {4}))
15		fzo1to4tp 13805	. . 3 ⊢ (1..^4) = {1, 2, 3}
16	15	eleq2i 2857	. 2 ⊢ (𝑌 ∈ (1..^4) ↔ 𝑌 ∈ {1, 2, 3})
17		elun 4107	. . . . 5 ⊢ (𝑋 ∈ (({0, 1} ∪ {2, 3}) ∪ {4}) ↔ (𝑋 ∈ ({0, 1} ∪ {2, 3}) ∨ 𝑋 ∈ {4}))
18		elun 4107	. . . . . 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 4615	. . . . . . 7 ⊢ (𝑋 ∈ {0, 1} → (𝑋 = 0 ∨ 𝑋 = 1))
22		0ne1 12332	. . . . . . . . . . . . . . . . 17 ⊢ 0 ≠ 1
23	22	olci 880	. . . . . . . . . . . . . . . 16 ⊢ (0 ≠ 0 ∨ 0 ≠ 1)
24		c0ex 11220	. . . . . . . . . . . . . . . . 17 ⊢ 0 ∈ V
25	24, 24	opthne 5466	. . . . . . . . . . . . . . . 16 ⊢ (⟨0, 0⟩ ≠ ⟨0, 1⟩ ↔ (0 ≠ 0 ∨ 0 ≠ 1))
26	23, 25	mpbir 234	. . . . . . . . . . . . . . 15 ⊢ ⟨0, 0⟩ ≠ ⟨0, 1⟩
27	1	fveq1i 6887	. . . . . . . . . . . . . . . . 17 ⊢ (𝑃‘0) = (⟨“⟨0, 0⟩⟨0, 1⟩⟨1, 1⟩⟨1, 0⟩⟨0, 0⟩”⟩‘0)
28		opex 5447	. . . . . . . . . . . . . . . . . 18 ⊢ ⟨0, 0⟩ ∈ V
29		df-s5 14917	. . . . . . . . . . . . . . . . . . 19 ⊢ ⟨“⟨0, 0⟩⟨0, 1⟩⟨1, 1⟩⟨1, 0⟩⟨0, 0⟩”⟩ = (⟨“⟨0, 0⟩⟨0, 1⟩⟨1, 1⟩⟨1, 0⟩”⟩ ++ ⟨“⟨0, 0⟩”⟩)
30		s4cli 14948	. . . . . . . . . . . . . . . . . . 19 ⊢ ⟨“⟨0, 0⟩⟨0, 1⟩⟨1, 1⟩⟨1, 0⟩”⟩ ∈ Word V
31		s4len 14965	. . . . . . . . . . . . . . . . . . 19 ⊢ (♯‘⟨“⟨0, 0⟩⟨0, 1⟩⟨1, 1⟩⟨1, 0⟩”⟩) = 4
32		s4fv0 14961	. . . . . . . . . . . . . . . . . . 19 ⊢ (⟨0, 0⟩ ∈ V → (⟨“⟨0, 0⟩⟨0, 1⟩⟨1, 1⟩⟨1, 0⟩”⟩‘0) = ⟨0, 0⟩)
33		0nn0 12539	. . . . . . . . . . . . . . . . . . 19 ⊢ 0 ∈ ℕ₀
34		4pos 12371	. . . . . . . . . . . . . . . . . . 19 ⊢ 0 < 4
35	29, 30, 31, 32, 33, 34	cats1fv 14925	. . . . . . . . . . . . . . . . . 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 2788	. . . . . . . . . . . . . . . 16 ⊢ (𝑃‘0) = ⟨0, 0⟩
38	1	fveq1i 6887	. . . . . . . . . . . . . . . . 17 ⊢ (𝑃‘1) = (⟨“⟨0, 0⟩⟨0, 1⟩⟨1, 1⟩⟨1, 0⟩⟨0, 0⟩”⟩‘1)
39		opex 5447	. . . . . . . . . . . . . . . . . 18 ⊢ ⟨0, 1⟩ ∈ V
40		s4fv1 14962	. . . . . . . . . . . . . . . . . . 19 ⊢ (⟨0, 1⟩ ∈ V → (⟨“⟨0, 0⟩⟨0, 1⟩⟨1, 1⟩⟨1, 0⟩”⟩‘1) = ⟨0, 1⟩)
41		1nn0 12540	. . . . . . . . . . . . . . . . . . 19 ⊢ 1 ∈ ℕ₀
42		1lt4 12439	. . . . . . . . . . . . . . . . . . 19 ⊢ 1 < 4
43	29, 30, 31, 40, 41, 42	cats1fv 14925	. . . . . . . . . . . . . . . . . 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 2788	. . . . . . . . . . . . . . . 16 ⊢ (𝑃‘1) = ⟨0, 1⟩
46	37, 45	neeq12i 3026	. . . . . . . . . . . . . . 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 6886	. . . . . . . . . . . . . 14 ⊢ (𝑋 = 0 → (𝑃‘𝑋) = (𝑃‘0))
50	49	adantl 487	. . . . . . . . . . . . 13 ⊢ ((𝑌 = 1 ∧ 𝑋 = 0) → (𝑃‘𝑋) = (𝑃‘0))
51		fveq2 6886	. . . . . . . . . . . . . 14 ⊢ (𝑌 = 1 → (𝑃‘𝑌) = (𝑃‘1))
52	51	adantr 486	. . . . . . . . . . . . 13 ⊢ ((𝑌 = 1 ∧ 𝑋 = 0) → (𝑃‘𝑌) = (𝑃‘1))
53	48, 50, 52	3netr4d 3037	. . . . . . . . . . . 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 5466	. . . . . . . . . . . . . . . 16 ⊢ (⟨0, 0⟩ ≠ ⟨1, 1⟩ ↔ (0 ≠ 1 ∨ 0 ≠ 1))
58	56, 57	mpbir 234	. . . . . . . . . . . . . . 15 ⊢ ⟨0, 0⟩ ≠ ⟨1, 1⟩
59	1	fveq1i 6887	. . . . . . . . . . . . . . . . 17 ⊢ (𝑃‘2) = (⟨“⟨0, 0⟩⟨0, 1⟩⟨1, 1⟩⟨1, 0⟩⟨0, 0⟩”⟩‘2)
60		opex 5447	. . . . . . . . . . . . . . . . . 18 ⊢ ⟨1, 1⟩ ∈ V
61		s4fv2 14963	. . . . . . . . . . . . . . . . . . 19 ⊢ (⟨1, 1⟩ ∈ V → (⟨“⟨0, 0⟩⟨0, 1⟩⟨1, 1⟩⟨1, 0⟩”⟩‘2) = ⟨1, 1⟩)
62		2nn0 12541	. . . . . . . . . . . . . . . . . . 19 ⊢ 2 ∈ ℕ₀
63		2lt4 12438	. . . . . . . . . . . . . . . . . . 19 ⊢ 2 < 4
64	29, 30, 31, 61, 62, 63	cats1fv 14925	. . . . . . . . . . . . . . . . . 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 2788	. . . . . . . . . . . . . . . 16 ⊢ (𝑃‘2) = ⟨1, 1⟩
67	37, 66	neeq12i 3026	. . . . . . . . . . . . . . 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 6886	. . . . . . . . . . . . . 14 ⊢ (𝑌 = 2 → (𝑃‘𝑌) = (𝑃‘2))
72	71	adantr 486	. . . . . . . . . . . . 13 ⊢ ((𝑌 = 2 ∧ 𝑋 = 0) → (𝑃‘𝑌) = (𝑃‘2))
73	69, 70, 72	3netr4d 3037	. . . . . . . . . . . 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 5466	. . . . . . . . . . . . . . . 16 ⊢ (⟨0, 0⟩ ≠ ⟨1, 0⟩ ↔ (0 ≠ 1 ∨ 0 ≠ 0))
78	76, 77	mpbir 234	. . . . . . . . . . . . . . 15 ⊢ ⟨0, 0⟩ ≠ ⟨1, 0⟩
79	1	fveq1i 6887	. . . . . . . . . . . . . . . . 17 ⊢ (𝑃‘3) = (⟨“⟨0, 0⟩⟨0, 1⟩⟨1, 1⟩⟨1, 0⟩⟨0, 0⟩”⟩‘3)
80		opex 5447	. . . . . . . . . . . . . . . . . 18 ⊢ ⟨1, 0⟩ ∈ V
81		s4fv3 14964	. . . . . . . . . . . . . . . . . . 19 ⊢ (⟨1, 0⟩ ∈ V → (⟨“⟨0, 0⟩⟨0, 1⟩⟨1, 1⟩⟨1, 0⟩”⟩‘3) = ⟨1, 0⟩)
82		3nn0 12542	. . . . . . . . . . . . . . . . . . 19 ⊢ 3 ∈ ℕ₀
83		3lt4 12437	. . . . . . . . . . . . . . . . . . 19 ⊢ 3 < 4
84	29, 30, 31, 81, 82, 83	cats1fv 14925	. . . . . . . . . . . . . . . . . 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 2788	. . . . . . . . . . . . . . . 16 ⊢ (𝑃‘3) = ⟨1, 0⟩
87	37, 86	neeq12i 3026	. . . . . . . . . . . . . . 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 6886	. . . . . . . . . . . . . 14 ⊢ (𝑌 = 3 → (𝑃‘𝑌) = (𝑃‘3))
92	91	adantr 486	. . . . . . . . . . . . 13 ⊢ ((𝑌 = 3 ∧ 𝑋 = 0) → (𝑃‘𝑌) = (𝑃‘3))
93	89, 90, 92	3netr4d 3037	. . . . . . . . . . . 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 4656	. . . . . . . . 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 3021	. . . . . . . . . . . 12 ⊢ ((𝑌 = 1 ∧ 𝑋 = 1) → (𝑋 ≠ 𝑌 ↔ 1 ≠ 1))
102		eqid 2765	. . . . . . . . . . . . 13 ⊢ 1 = 1
103		eqneqall 2971	. . . . . . . . . . . . 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 11223	. . . . . . . . . . . . . . . . 17 ⊢ 1 ∈ V
109	24, 108	opthne 5466	. . . . . . . . . . . . . . . 16 ⊢ (⟨0, 1⟩ ≠ ⟨1, 1⟩ ↔ (0 ≠ 1 ∨ 1 ≠ 1))
110	107, 109	mpbir 234	. . . . . . . . . . . . . . 15 ⊢ ⟨0, 1⟩ ≠ ⟨1, 1⟩
111	45, 66	neeq12i 3026	. . . . . . . . . . . . . . 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 6886	. . . . . . . . . . . . . 14 ⊢ (𝑋 = 1 → (𝑃‘𝑋) = (𝑃‘1))
115	114	adantl 487	. . . . . . . . . . . . 13 ⊢ ((𝑌 = 2 ∧ 𝑋 = 1) → (𝑃‘𝑋) = (𝑃‘1))
116	71	adantr 486	. . . . . . . . . . . . 13 ⊢ ((𝑌 = 2 ∧ 𝑋 = 1) → (𝑃‘𝑌) = (𝑃‘2))
117	113, 115, 116	3netr4d 3037	. . . . . . . . . . . 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 5466	. . . . . . . . . . . . . . . 16 ⊢ (⟨0, 1⟩ ≠ ⟨1, 0⟩ ↔ (0 ≠ 1 ∨ 1 ≠ 0))
122	120, 121	mpbir 234	. . . . . . . . . . . . . . 15 ⊢ ⟨0, 1⟩ ≠ ⟨1, 0⟩
123	45, 86	neeq12i 3026	. . . . . . . . . . . . . . 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 3037	. . . . . . . . . . . 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 4615	. . . . . . 7 ⊢ (𝑋 ∈ {2, 3} → (𝑋 = 2 ∨ 𝑋 = 3))
136	112	necomi 3014	. . . . . . . . . . . . . 14 ⊢ (𝑃‘2) ≠ (𝑃‘1)
137	136	a1i 11	. . . . . . . . . . . . 13 ⊢ ((𝑌 = 1 ∧ 𝑋 = 2) → (𝑃‘2) ≠ (𝑃‘1))
138		fveq2 6886	. . . . . . . . . . . . . 14 ⊢ (𝑋 = 2 → (𝑃‘𝑋) = (𝑃‘2))
139	138	adantl 487	. . . . . . . . . . . . 13 ⊢ ((𝑌 = 1 ∧ 𝑋 = 2) → (𝑃‘𝑋) = (𝑃‘2))
140	51	adantr 486	. . . . . . . . . . . . 13 ⊢ ((𝑌 = 1 ∧ 𝑋 = 2) → (𝑃‘𝑌) = (𝑃‘1))
141	137, 139, 140	3netr4d 3037	. . . . . . . . . . . 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 3021	. . . . . . . . . . . 12 ⊢ ((𝑌 = 2 ∧ 𝑋 = 2) → (𝑋 ≠ 𝑌 ↔ 2 ≠ 2))
147		eqid 2765	. . . . . . . . . . . . 13 ⊢ 2 = 2
148		eqneqall 2971	. . . . . . . . . . . . 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 3014	. . . . . . . . . . . . . . . . 17 ⊢ 1 ≠ 0
153	152	olci 880	. . . . . . . . . . . . . . . 16 ⊢ (1 ≠ 1 ∨ 1 ≠ 0)
154	108, 108	opthne 5466	. . . . . . . . . . . . . . . 16 ⊢ (⟨1, 1⟩ ≠ ⟨1, 0⟩ ↔ (1 ≠ 1 ∨ 1 ≠ 0))
155	153, 154	mpbir 234	. . . . . . . . . . . . . . 15 ⊢ ⟨1, 1⟩ ≠ ⟨1, 0⟩
156	66, 86	neeq12i 3026	. . . . . . . . . . . . . . 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 3037	. . . . . . . . . . . 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 3014	. . . . . . . . . . . . . 14 ⊢ (𝑃‘3) ≠ (𝑃‘1)
167	166	a1i 11	. . . . . . . . . . . . 13 ⊢ ((𝑌 = 1 ∧ 𝑋 = 3) → (𝑃‘3) ≠ (𝑃‘1))
168		fveq2 6886	. . . . . . . . . . . . . 14 ⊢ (𝑋 = 3 → (𝑃‘𝑋) = (𝑃‘3))
169	168	adantl 487	. . . . . . . . . . . . 13 ⊢ ((𝑌 = 1 ∧ 𝑋 = 3) → (𝑃‘𝑋) = (𝑃‘3))
170	51	adantr 486	. . . . . . . . . . . . 13 ⊢ ((𝑌 = 1 ∧ 𝑋 = 3) → (𝑃‘𝑌) = (𝑃‘1))
171	167, 169, 170	3netr4d 3037	. . . . . . . . . . . 12 ⊢ ((𝑌 = 1 ∧ 𝑋 = 3) → (𝑃‘𝑋) ≠ (𝑃‘𝑌))
172	171	a1d 26	. . . . . . . . . . 11 ⊢ ((𝑌 = 1 ∧ 𝑋 = 3) → (𝑋 ≠ 𝑌 → (𝑃‘𝑋) ≠ (𝑃‘𝑌)))
173	172	ex 418	. . . . . . . . . 10 ⊢ (𝑌 = 1 → (𝑋 = 3 → (𝑋 ≠ 𝑌 → (𝑃‘𝑋) ≠ (𝑃‘𝑌))))
174	157	necomi 3014	. . . . . . . . . . . . . 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 3037	. . . . . . . . . . . 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 3021	. . . . . . . . . . . 12 ⊢ ((𝑌 = 3 ∧ 𝑋 = 3) → (𝑋 ≠ 𝑌 ↔ 3 ≠ 3))
184		eqid 2765	. . . . . . . . . . . . 13 ⊢ 3 = 3
185		eqneqall 2971	. . . . . . . . . . . . 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 4608	. . . . . 6 ⊢ (𝑋 ∈ {4} → 𝑋 = 4)
195	1	fveq1i 6887	. . . . . . . . . . . . . 14 ⊢ (𝑃‘4) = (⟨“⟨0, 0⟩⟨0, 1⟩⟨1, 1⟩⟨1, 0⟩⟨0, 0⟩”⟩‘4)
196	29, 30, 31	cats1fvn 14924	. . . . . . . . . . . . . . 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 2788	. . . . . . . . . . . . 13 ⊢ (𝑃‘4) = ⟨0, 0⟩
199	198, 45	neeq12i 3026	. . . . . . . . . . . 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 6886	. . . . . . . . . . 11 ⊢ (𝑋 = 4 → (𝑃‘𝑋) = (𝑃‘4))
203	202	adantl 487	. . . . . . . . . 10 ⊢ ((𝑌 = 1 ∧ 𝑋 = 4) → (𝑃‘𝑋) = (𝑃‘4))
204	51	adantr 486	. . . . . . . . . 10 ⊢ ((𝑌 = 1 ∧ 𝑋 = 4) → (𝑃‘𝑌) = (𝑃‘1))
205	201, 203, 204	3netr4d 3037	. . . . . . . . 9 ⊢ ((𝑌 = 1 ∧ 𝑋 = 4) → (𝑃‘𝑋) ≠ (𝑃‘𝑌))
206	205	a1d 26	. . . . . . . 8 ⊢ ((𝑌 = 1 ∧ 𝑋 = 4) → (𝑋 ≠ 𝑌 → (𝑃‘𝑋) ≠ (𝑃‘𝑌)))
207	206	ex 418	. . . . . . 7 ⊢ (𝑌 = 1 → (𝑋 = 4 → (𝑋 ≠ 𝑌 → (𝑃‘𝑋) ≠ (𝑃‘𝑌))))
208	198, 66	neeq12i 3026	. . . . . . . . . . . 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 3037	. . . . . . . . 9 ⊢ ((𝑌 = 2 ∧ 𝑋 = 4) → (𝑃‘𝑋) ≠ (𝑃‘𝑌))
214	213	a1d 26	. . . . . . . 8 ⊢ ((𝑌 = 2 ∧ 𝑋 = 4) → (𝑋 ≠ 𝑌 → (𝑃‘𝑋) ≠ (𝑃‘𝑌)))
215	214	ex 418	. . . . . . 7 ⊢ (𝑌 = 2 → (𝑋 = 4 → (𝑋 ≠ 𝑌 → (𝑃‘𝑋) ≠ (𝑃‘𝑌))))
216	198, 86	neeq12i 3026	. . . . . . . . . . . 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 3037	. . . . . . . . 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 2146 ≠ wne 2960 Vcvv 3457 ∪ cun 3904 {csn 4591 {cpr 4593 {ctp 4595 ⟨cop 4597 ‘cfv 6541 (class class class)co 7420 0cc0 11120 1c1 11121 + caddc 11123 2c2 12315 3c3 12316 4c4 12317 5c5 12318 ℕ₀cn0 12524 ℤ_≥cuz 12883 ..^cfzo 13704 ♯chash 14389 ⟨“cs4 14909 ⟨“cs5 14910

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 2148 ax-9 2156 ax-10 2179 ax-11 2195 ax-12 2216 ax-ext 2737 ax-rep 5240 ax-sep 5259 ax-nul 5271 ax-pow 5338 ax-pr 5406 ax-un 7743 ax-cnex 11176 ax-resscn 11177 ax-1cn 11178 ax-icn 11179 ax-addcl 11180 ax-addrcl 11181 ax-mulcl 11182 ax-mulrcl 11183 ax-mulcom 11184 ax-addass 11185 ax-mulass 11186 ax-distr 11187 ax-i2m1 11188 ax-1ne0 11189 ax-1rid 11190 ax-rnegex 11191 ax-rrecex 11192 ax-cnre 11193 ax-pre-lttri 11194 ax-pre-lttrn 11195 ax-pre-ltadd 11196 ax-pre-mulgt0 11197

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 2569 df-eu 2599 df-clab 2744 df-cleq 2757 df-clel 2840 df-nfc 2914 df-ne 2961 df-nel 3067 df-ral 3082 df-rex 3092 df-reu 3372 df-rab 3419 df-v 3459 df-sbc 3747 df-csb 3855 df-dif 3909 df-un 3911 df-in 3913 df-ss 3923 df-pss 3926 df-nul 4287 df-if 4490 df-pw 4566 df-sn 4592 df-pr 4594 df-tp 4596 df-op 4598 df-uni 4875 df-int 4915 df-iun 4960 df-br 5112 df-opab 5176 df-mpt 5195 df-tr 5221 df-id 5558 df-eprel 5563 df-po 5571 df-so 5572 df-fr 5616 df-we 5618 df-xp 5669 df-rel 5670 df-cnv 5671 df-co 5672 df-dm 5673 df-rn 5674 df-res 5675 df-ima 5676 df-pred 6307 df-ord 6368 df-on 6369 df-lim 6370 df-suc 6371 df-iota 6497 df-fun 6543 df-fn 6544 df-f 6545 df-f1 6546 df-fo 6547 df-f1o 6548 df-fv 6549 df-riota 7377 df-ov 7423 df-oprab 7424 df-mpo 7425 df-om 7870 df-1st 7993 df-2nd 7994 df-frecs 8285 df-wrecs 8316 df-recs 8365 df-rdg 8404 df-1o 8460 df-er 8701 df-en 8951 df-dom 8952 df-sdom 8953 df-fin 8954 df-card 9942 df-pnf 11265 df-mnf 11266 df-xr 11267 df-ltxr 11268 df-le 11269 df-sub 11463 df-neg 11464 df-nn 12254 df-2 12323 df-3 12324 df-4 12325 df-5 12326 df-n0 12525 df-z 12612 df-uz 12884 df-fz 13557 df-fzo 13705 df-hash 14390 df-word 14574 df-concat 14631 df-s1 14658 df-s2 14914 df-s3 14915 df-s4 14916 df-s5 14917

This theorem is used by: gpgprismgr4cycllem11 48948

W3C validator