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 48894

Description: Lemma 7 for gpgprismgr4cycl0 48899: 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 48891	. . . . . 6 ⊢ (♯‘𝑃) = 5
3		df-5 12310	. . . . . 6 ⊢ 5 = (4 + 1)
4	2, 3	eqtri 2786	. . . . 5 ⊢ (♯‘𝑃) = (4 + 1)
5	4	oveq2i 7421	. . . 4 ⊢ (0..^(♯‘𝑃)) = (0..^(4 + 1))
6		4nn0 12527	. . . . . 6 ⊢ 4 ∈ ℕ₀
7		elnn0uz 12907	. . . . . 6 ⊢ (4 ∈ ℕ₀ ↔ 4 ∈ (ℤ_≥‘0))
8	6, 7	mpbi 233	. . . . 5 ⊢ 4 ∈ (ℤ_≥‘0)
9		fzosplitsn 13810	. . . . 5 ⊢ (4 ∈ (ℤ_≥‘0) → (0..^(4 + 1)) = ((0..^4) ∪ {4}))
10	8, 9	ax-mp 5	. . . 4 ⊢ (0..^(4 + 1)) = ((0..^4) ∪ {4})
11		fzo0to42pr 13787	. . . . 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 2790	. . 3 ⊢ (0..^(♯‘𝑃)) = (({0, 1} ∪ {2, 3}) ∪ {4})
14	13	eleq2i 2855	. 2 ⊢ (𝑋 ∈ (0..^(♯‘𝑃)) ↔ 𝑋 ∈ (({0, 1} ∪ {2, 3}) ∪ {4}))
15		fzo1to4tp 13788	. . 3 ⊢ (1..^4) = {1, 2, 3}
16	15	eleq2i 2855	. 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 926	. . . . 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 4613	. . . . . . 7 ⊢ (𝑋 ∈ {0, 1} → (𝑋 = 0 ∨ 𝑋 = 1))
22		0ne1 12316	. . . . . . . . . . . . . . . . 17 ⊢ 0 ≠ 1
23	22	olci 879	. . . . . . . . . . . . . . . 16 ⊢ (0 ≠ 0 ∨ 0 ≠ 1)
24		c0ex 11204	. . . . . . . . . . . . . . . . 17 ⊢ 0 ∈ V
25	24, 24	opthne 5464	. . . . . . . . . . . . . . . 16 ⊢ (⟨0, 0⟩ ≠ ⟨0, 1⟩ ↔ (0 ≠ 0 ∨ 0 ≠ 1))
26	23, 25	mpbir 234	. . . . . . . . . . . . . . 15 ⊢ ⟨0, 0⟩ ≠ ⟨0, 1⟩
27	1	fveq1i 6882	. . . . . . . . . . . . . . . . 17 ⊢ (𝑃‘0) = (⟨“⟨0, 0⟩⟨0, 1⟩⟨1, 1⟩⟨1, 0⟩⟨0, 0⟩”⟩‘0)
28		opex 5445	. . . . . . . . . . . . . . . . . 18 ⊢ ⟨0, 0⟩ ∈ V
29		df-s5 14893	. . . . . . . . . . . . . . . . . . 19 ⊢ ⟨“⟨0, 0⟩⟨0, 1⟩⟨1, 1⟩⟨1, 0⟩⟨0, 0⟩”⟩ = (⟨“⟨0, 0⟩⟨0, 1⟩⟨1, 1⟩⟨1, 0⟩”⟩ ++ ⟨“⟨0, 0⟩”⟩)
30		s4cli 14924	. . . . . . . . . . . . . . . . . . 19 ⊢ ⟨“⟨0, 0⟩⟨0, 1⟩⟨1, 1⟩⟨1, 0⟩”⟩ ∈ Word V
31		s4len 14941	. . . . . . . . . . . . . . . . . . 19 ⊢ (♯‘⟨“⟨0, 0⟩⟨0, 1⟩⟨1, 1⟩⟨1, 0⟩”⟩) = 4
32		s4fv0 14937	. . . . . . . . . . . . . . . . . . 19 ⊢ (⟨0, 0⟩ ∈ V → (⟨“⟨0, 0⟩⟨0, 1⟩⟨1, 1⟩⟨1, 0⟩”⟩‘0) = ⟨0, 0⟩)
33		0nn0 12523	. . . . . . . . . . . . . . . . . . 19 ⊢ 0 ∈ ℕ₀
34		4pos 12355	. . . . . . . . . . . . . . . . . . 19 ⊢ 0 < 4
35	29, 30, 31, 32, 33, 34	cats1fv 14901	. . . . . . . . . . . . . . . . . 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 2786	. . . . . . . . . . . . . . . 16 ⊢ (𝑃‘0) = ⟨0, 0⟩
38	1	fveq1i 6882	. . . . . . . . . . . . . . . . 17 ⊢ (𝑃‘1) = (⟨“⟨0, 0⟩⟨0, 1⟩⟨1, 1⟩⟨1, 0⟩⟨0, 0⟩”⟩‘1)
39		opex 5445	. . . . . . . . . . . . . . . . . 18 ⊢ ⟨0, 1⟩ ∈ V
40		s4fv1 14938	. . . . . . . . . . . . . . . . . . 19 ⊢ (⟨0, 1⟩ ∈ V → (⟨“⟨0, 0⟩⟨0, 1⟩⟨1, 1⟩⟨1, 0⟩”⟩‘1) = ⟨0, 1⟩)
41		1nn0 12524	. . . . . . . . . . . . . . . . . . 19 ⊢ 1 ∈ ℕ₀
42		1lt4 12423	. . . . . . . . . . . . . . . . . . 19 ⊢ 1 < 4
43	29, 30, 31, 40, 41, 42	cats1fv 14901	. . . . . . . . . . . . . . . . . 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 2786	. . . . . . . . . . . . . . . 16 ⊢ (𝑃‘1) = ⟨0, 1⟩
46	37, 45	neeq12i 3024	. . . . . . . . . . . . . . 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 6881	. . . . . . . . . . . . . 14 ⊢ (𝑋 = 0 → (𝑃‘𝑋) = (𝑃‘0))
50	49	adantl 486	. . . . . . . . . . . . 13 ⊢ ((𝑌 = 1 ∧ 𝑋 = 0) → (𝑃‘𝑋) = (𝑃‘0))
51		fveq2 6881	. . . . . . . . . . . . . 14 ⊢ (𝑌 = 1 → (𝑃‘𝑌) = (𝑃‘1))
52	51	adantr 485	. . . . . . . . . . . . 13 ⊢ ((𝑌 = 1 ∧ 𝑋 = 0) → (𝑃‘𝑌) = (𝑃‘1))
53	48, 50, 52	3netr4d 3035	. . . . . . . . . . . 12 ⊢ ((𝑌 = 1 ∧ 𝑋 = 0) → (𝑃‘𝑋) ≠ (𝑃‘𝑌))
54	53	a1d 26	. . . . . . . . . . 11 ⊢ ((𝑌 = 1 ∧ 𝑋 = 0) → (𝑋 ≠ 𝑌 → (𝑃‘𝑋) ≠ (𝑃‘𝑌)))
55	54	ex 417	. . . . . . . . . 10 ⊢ (𝑌 = 1 → (𝑋 = 0 → (𝑋 ≠ 𝑌 → (𝑃‘𝑋) ≠ (𝑃‘𝑌))))
56	22	orci 878	. . . . . . . . . . . . . . . 16 ⊢ (0 ≠ 1 ∨ 0 ≠ 1)
57	24, 24	opthne 5464	. . . . . . . . . . . . . . . 16 ⊢ (⟨0, 0⟩ ≠ ⟨1, 1⟩ ↔ (0 ≠ 1 ∨ 0 ≠ 1))
58	56, 57	mpbir 234	. . . . . . . . . . . . . . 15 ⊢ ⟨0, 0⟩ ≠ ⟨1, 1⟩
59	1	fveq1i 6882	. . . . . . . . . . . . . . . . 17 ⊢ (𝑃‘2) = (⟨“⟨0, 0⟩⟨0, 1⟩⟨1, 1⟩⟨1, 0⟩⟨0, 0⟩”⟩‘2)
60		opex 5445	. . . . . . . . . . . . . . . . . 18 ⊢ ⟨1, 1⟩ ∈ V
61		s4fv2 14939	. . . . . . . . . . . . . . . . . . 19 ⊢ (⟨1, 1⟩ ∈ V → (⟨“⟨0, 0⟩⟨0, 1⟩⟨1, 1⟩⟨1, 0⟩”⟩‘2) = ⟨1, 1⟩)
62		2nn0 12525	. . . . . . . . . . . . . . . . . . 19 ⊢ 2 ∈ ℕ₀
63		2lt4 12422	. . . . . . . . . . . . . . . . . . 19 ⊢ 2 < 4
64	29, 30, 31, 61, 62, 63	cats1fv 14901	. . . . . . . . . . . . . . . . . 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 2786	. . . . . . . . . . . . . . . 16 ⊢ (𝑃‘2) = ⟨1, 1⟩
67	37, 66	neeq12i 3024	. . . . . . . . . . . . . . 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 486	. . . . . . . . . . . . 13 ⊢ ((𝑌 = 2 ∧ 𝑋 = 0) → (𝑃‘𝑋) = (𝑃‘0))
71		fveq2 6881	. . . . . . . . . . . . . 14 ⊢ (𝑌 = 2 → (𝑃‘𝑌) = (𝑃‘2))
72	71	adantr 485	. . . . . . . . . . . . 13 ⊢ ((𝑌 = 2 ∧ 𝑋 = 0) → (𝑃‘𝑌) = (𝑃‘2))
73	69, 70, 72	3netr4d 3035	. . . . . . . . . . . 12 ⊢ ((𝑌 = 2 ∧ 𝑋 = 0) → (𝑃‘𝑋) ≠ (𝑃‘𝑌))
74	73	a1d 26	. . . . . . . . . . 11 ⊢ ((𝑌 = 2 ∧ 𝑋 = 0) → (𝑋 ≠ 𝑌 → (𝑃‘𝑋) ≠ (𝑃‘𝑌)))
75	74	ex 417	. . . . . . . . . 10 ⊢ (𝑌 = 2 → (𝑋 = 0 → (𝑋 ≠ 𝑌 → (𝑃‘𝑋) ≠ (𝑃‘𝑌))))
76	22	orci 878	. . . . . . . . . . . . . . . 16 ⊢ (0 ≠ 1 ∨ 0 ≠ 0)
77	24, 24	opthne 5464	. . . . . . . . . . . . . . . 16 ⊢ (⟨0, 0⟩ ≠ ⟨1, 0⟩ ↔ (0 ≠ 1 ∨ 0 ≠ 0))
78	76, 77	mpbir 234	. . . . . . . . . . . . . . 15 ⊢ ⟨0, 0⟩ ≠ ⟨1, 0⟩
79	1	fveq1i 6882	. . . . . . . . . . . . . . . . 17 ⊢ (𝑃‘3) = (⟨“⟨0, 0⟩⟨0, 1⟩⟨1, 1⟩⟨1, 0⟩⟨0, 0⟩”⟩‘3)
80		opex 5445	. . . . . . . . . . . . . . . . . 18 ⊢ ⟨1, 0⟩ ∈ V
81		s4fv3 14940	. . . . . . . . . . . . . . . . . . 19 ⊢ (⟨1, 0⟩ ∈ V → (⟨“⟨0, 0⟩⟨0, 1⟩⟨1, 1⟩⟨1, 0⟩”⟩‘3) = ⟨1, 0⟩)
82		3nn0 12526	. . . . . . . . . . . . . . . . . . 19 ⊢ 3 ∈ ℕ₀
83		3lt4 12421	. . . . . . . . . . . . . . . . . . 19 ⊢ 3 < 4
84	29, 30, 31, 81, 82, 83	cats1fv 14901	. . . . . . . . . . . . . . . . . 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 2786	. . . . . . . . . . . . . . . 16 ⊢ (𝑃‘3) = ⟨1, 0⟩
87	37, 86	neeq12i 3024	. . . . . . . . . . . . . . 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 486	. . . . . . . . . . . . 13 ⊢ ((𝑌 = 3 ∧ 𝑋 = 0) → (𝑃‘𝑋) = (𝑃‘0))
91		fveq2 6881	. . . . . . . . . . . . . 14 ⊢ (𝑌 = 3 → (𝑃‘𝑌) = (𝑃‘3))
92	91	adantr 485	. . . . . . . . . . . . 13 ⊢ ((𝑌 = 3 ∧ 𝑋 = 0) → (𝑃‘𝑌) = (𝑃‘3))
93	89, 90, 92	3netr4d 3035	. . . . . . . . . . . 12 ⊢ ((𝑌 = 3 ∧ 𝑋 = 0) → (𝑃‘𝑋) ≠ (𝑃‘𝑌))
94	93	a1d 26	. . . . . . . . . . 11 ⊢ ((𝑌 = 3 ∧ 𝑋 = 0) → (𝑋 ≠ 𝑌 → (𝑃‘𝑋) ≠ (𝑃‘𝑌)))
95	94	ex 417	. . . . . . . . . 10 ⊢ (𝑌 = 3 → (𝑋 = 0 → (𝑋 ≠ 𝑌 → (𝑃‘𝑋) ≠ (𝑃‘𝑌))))
96	55, 75, 95	3jaoi 1454	. . . . . . . . 9 ⊢ ((𝑌 = 1 ∨ 𝑌 = 2 ∨ 𝑌 = 3) → (𝑋 = 0 → (𝑋 ≠ 𝑌 → (𝑃‘𝑋) ≠ (𝑃‘𝑌))))
97		eltpi 4654	. . . . . . . . 9 ⊢ (𝑌 ∈ {1, 2, 3} → (𝑌 = 1 ∨ 𝑌 = 2 ∨ 𝑌 = 3))
98	96, 97	syl11 34	. . . . . . . 8 ⊢ (𝑋 = 0 → (𝑌 ∈ {1, 2, 3} → (𝑋 ≠ 𝑌 → (𝑃‘𝑋) ≠ (𝑃‘𝑌))))
99		simpr 489	. . . . . . . . . . . . 13 ⊢ ((𝑌 = 1 ∧ 𝑋 = 1) → 𝑋 = 1)
100		simpl 487	. . . . . . . . . . . . 13 ⊢ ((𝑌 = 1 ∧ 𝑋 = 1) → 𝑌 = 1)
101	99, 100	neeq12d 3019	. . . . . . . . . . . 12 ⊢ ((𝑌 = 1 ∧ 𝑋 = 1) → (𝑋 ≠ 𝑌 ↔ 1 ≠ 1))
102		eqid 2763	. . . . . . . . . . . . 13 ⊢ 1 = 1
103		eqneqall 2969	. . . . . . . . . . . . 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 417	. . . . . . . . . 10 ⊢ (𝑌 = 1 → (𝑋 = 1 → (𝑋 ≠ 𝑌 → (𝑃‘𝑋) ≠ (𝑃‘𝑌))))
107	22	orci 878	. . . . . . . . . . . . . . . 16 ⊢ (0 ≠ 1 ∨ 1 ≠ 1)
108		1ex 11207	. . . . . . . . . . . . . . . . 17 ⊢ 1 ∈ V
109	24, 108	opthne 5464	. . . . . . . . . . . . . . . 16 ⊢ (⟨0, 1⟩ ≠ ⟨1, 1⟩ ↔ (0 ≠ 1 ∨ 1 ≠ 1))
110	107, 109	mpbir 234	. . . . . . . . . . . . . . 15 ⊢ ⟨0, 1⟩ ≠ ⟨1, 1⟩
111	45, 66	neeq12i 3024	. . . . . . . . . . . . . . 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 6881	. . . . . . . . . . . . . 14 ⊢ (𝑋 = 1 → (𝑃‘𝑋) = (𝑃‘1))
115	114	adantl 486	. . . . . . . . . . . . 13 ⊢ ((𝑌 = 2 ∧ 𝑋 = 1) → (𝑃‘𝑋) = (𝑃‘1))
116	71	adantr 485	. . . . . . . . . . . . 13 ⊢ ((𝑌 = 2 ∧ 𝑋 = 1) → (𝑃‘𝑌) = (𝑃‘2))
117	113, 115, 116	3netr4d 3035	. . . . . . . . . . . 12 ⊢ ((𝑌 = 2 ∧ 𝑋 = 1) → (𝑃‘𝑋) ≠ (𝑃‘𝑌))
118	117	a1d 26	. . . . . . . . . . 11 ⊢ ((𝑌 = 2 ∧ 𝑋 = 1) → (𝑋 ≠ 𝑌 → (𝑃‘𝑋) ≠ (𝑃‘𝑌)))
119	118	ex 417	. . . . . . . . . 10 ⊢ (𝑌 = 2 → (𝑋 = 1 → (𝑋 ≠ 𝑌 → (𝑃‘𝑋) ≠ (𝑃‘𝑌))))
120	22	orci 878	. . . . . . . . . . . . . . . 16 ⊢ (0 ≠ 1 ∨ 1 ≠ 0)
121	24, 108	opthne 5464	. . . . . . . . . . . . . . . 16 ⊢ (⟨0, 1⟩ ≠ ⟨1, 0⟩ ↔ (0 ≠ 1 ∨ 1 ≠ 0))
122	120, 121	mpbir 234	. . . . . . . . . . . . . . 15 ⊢ ⟨0, 1⟩ ≠ ⟨1, 0⟩
123	45, 86	neeq12i 3024	. . . . . . . . . . . . . . 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 486	. . . . . . . . . . . . 13 ⊢ ((𝑌 = 3 ∧ 𝑋 = 1) → (𝑃‘𝑋) = (𝑃‘1))
127	91	adantr 485	. . . . . . . . . . . . 13 ⊢ ((𝑌 = 3 ∧ 𝑋 = 1) → (𝑃‘𝑌) = (𝑃‘3))
128	125, 126, 127	3netr4d 3035	. . . . . . . . . . . 12 ⊢ ((𝑌 = 3 ∧ 𝑋 = 1) → (𝑃‘𝑋) ≠ (𝑃‘𝑌))
129	128	a1d 26	. . . . . . . . . . 11 ⊢ ((𝑌 = 3 ∧ 𝑋 = 1) → (𝑋 ≠ 𝑌 → (𝑃‘𝑋) ≠ (𝑃‘𝑌)))
130	129	ex 417	. . . . . . . . . 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 870	. . . . . . 7 ⊢ ((𝑋 = 0 ∨ 𝑋 = 1) → (𝑌 ∈ {1, 2, 3} → (𝑋 ≠ 𝑌 → (𝑃‘𝑋) ≠ (𝑃‘𝑌))))
134	21, 133	syl 18	. . . . . 6 ⊢ (𝑋 ∈ {0, 1} → (𝑌 ∈ {1, 2, 3} → (𝑋 ≠ 𝑌 → (𝑃‘𝑋) ≠ (𝑃‘𝑌))))
135		elpri 4613	. . . . . . 7 ⊢ (𝑋 ∈ {2, 3} → (𝑋 = 2 ∨ 𝑋 = 3))
136	112	necomi 3012	. . . . . . . . . . . . . 14 ⊢ (𝑃‘2) ≠ (𝑃‘1)
137	136	a1i 11	. . . . . . . . . . . . 13 ⊢ ((𝑌 = 1 ∧ 𝑋 = 2) → (𝑃‘2) ≠ (𝑃‘1))
138		fveq2 6881	. . . . . . . . . . . . . 14 ⊢ (𝑋 = 2 → (𝑃‘𝑋) = (𝑃‘2))
139	138	adantl 486	. . . . . . . . . . . . 13 ⊢ ((𝑌 = 1 ∧ 𝑋 = 2) → (𝑃‘𝑋) = (𝑃‘2))
140	51	adantr 485	. . . . . . . . . . . . 13 ⊢ ((𝑌 = 1 ∧ 𝑋 = 2) → (𝑃‘𝑌) = (𝑃‘1))
141	137, 139, 140	3netr4d 3035	. . . . . . . . . . . 12 ⊢ ((𝑌 = 1 ∧ 𝑋 = 2) → (𝑃‘𝑋) ≠ (𝑃‘𝑌))
142	141	a1d 26	. . . . . . . . . . 11 ⊢ ((𝑌 = 1 ∧ 𝑋 = 2) → (𝑋 ≠ 𝑌 → (𝑃‘𝑋) ≠ (𝑃‘𝑌)))
143	142	ex 417	. . . . . . . . . 10 ⊢ (𝑌 = 1 → (𝑋 = 2 → (𝑋 ≠ 𝑌 → (𝑃‘𝑋) ≠ (𝑃‘𝑌))))
144		simpr 489	. . . . . . . . . . . . 13 ⊢ ((𝑌 = 2 ∧ 𝑋 = 2) → 𝑋 = 2)
145		simpl 487	. . . . . . . . . . . . 13 ⊢ ((𝑌 = 2 ∧ 𝑋 = 2) → 𝑌 = 2)
146	144, 145	neeq12d 3019	. . . . . . . . . . . 12 ⊢ ((𝑌 = 2 ∧ 𝑋 = 2) → (𝑋 ≠ 𝑌 ↔ 2 ≠ 2))
147		eqid 2763	. . . . . . . . . . . . 13 ⊢ 2 = 2
148		eqneqall 2969	. . . . . . . . . . . . 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 417	. . . . . . . . . 10 ⊢ (𝑌 = 2 → (𝑋 = 2 → (𝑋 ≠ 𝑌 → (𝑃‘𝑋) ≠ (𝑃‘𝑌))))
152	22	necomi 3012	. . . . . . . . . . . . . . . . 17 ⊢ 1 ≠ 0
153	152	olci 879	. . . . . . . . . . . . . . . 16 ⊢ (1 ≠ 1 ∨ 1 ≠ 0)
154	108, 108	opthne 5464	. . . . . . . . . . . . . . . 16 ⊢ (⟨1, 1⟩ ≠ ⟨1, 0⟩ ↔ (1 ≠ 1 ∨ 1 ≠ 0))
155	153, 154	mpbir 234	. . . . . . . . . . . . . . 15 ⊢ ⟨1, 1⟩ ≠ ⟨1, 0⟩
156	66, 86	neeq12i 3024	. . . . . . . . . . . . . . 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 486	. . . . . . . . . . . . 13 ⊢ ((𝑌 = 3 ∧ 𝑋 = 2) → (𝑃‘𝑋) = (𝑃‘2))
160	91	adantr 485	. . . . . . . . . . . . 13 ⊢ ((𝑌 = 3 ∧ 𝑋 = 2) → (𝑃‘𝑌) = (𝑃‘3))
161	158, 159, 160	3netr4d 3035	. . . . . . . . . . . 12 ⊢ ((𝑌 = 3 ∧ 𝑋 = 2) → (𝑃‘𝑋) ≠ (𝑃‘𝑌))
162	161	a1d 26	. . . . . . . . . . 11 ⊢ ((𝑌 = 3 ∧ 𝑋 = 2) → (𝑋 ≠ 𝑌 → (𝑃‘𝑋) ≠ (𝑃‘𝑌)))
163	162	ex 417	. . . . . . . . . 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 3012	. . . . . . . . . . . . . 14 ⊢ (𝑃‘3) ≠ (𝑃‘1)
167	166	a1i 11	. . . . . . . . . . . . 13 ⊢ ((𝑌 = 1 ∧ 𝑋 = 3) → (𝑃‘3) ≠ (𝑃‘1))
168		fveq2 6881	. . . . . . . . . . . . . 14 ⊢ (𝑋 = 3 → (𝑃‘𝑋) = (𝑃‘3))
169	168	adantl 486	. . . . . . . . . . . . 13 ⊢ ((𝑌 = 1 ∧ 𝑋 = 3) → (𝑃‘𝑋) = (𝑃‘3))
170	51	adantr 485	. . . . . . . . . . . . 13 ⊢ ((𝑌 = 1 ∧ 𝑋 = 3) → (𝑃‘𝑌) = (𝑃‘1))
171	167, 169, 170	3netr4d 3035	. . . . . . . . . . . 12 ⊢ ((𝑌 = 1 ∧ 𝑋 = 3) → (𝑃‘𝑋) ≠ (𝑃‘𝑌))
172	171	a1d 26	. . . . . . . . . . 11 ⊢ ((𝑌 = 1 ∧ 𝑋 = 3) → (𝑋 ≠ 𝑌 → (𝑃‘𝑋) ≠ (𝑃‘𝑌)))
173	172	ex 417	. . . . . . . . . 10 ⊢ (𝑌 = 1 → (𝑋 = 3 → (𝑋 ≠ 𝑌 → (𝑃‘𝑋) ≠ (𝑃‘𝑌))))
174	157	necomi 3012	. . . . . . . . . . . . . 14 ⊢ (𝑃‘3) ≠ (𝑃‘2)
175	174	a1i 11	. . . . . . . . . . . . 13 ⊢ ((𝑌 = 2 ∧ 𝑋 = 3) → (𝑃‘3) ≠ (𝑃‘2))
176	168	adantl 486	. . . . . . . . . . . . 13 ⊢ ((𝑌 = 2 ∧ 𝑋 = 3) → (𝑃‘𝑋) = (𝑃‘3))
177	71	adantr 485	. . . . . . . . . . . . 13 ⊢ ((𝑌 = 2 ∧ 𝑋 = 3) → (𝑃‘𝑌) = (𝑃‘2))
178	175, 176, 177	3netr4d 3035	. . . . . . . . . . . 12 ⊢ ((𝑌 = 2 ∧ 𝑋 = 3) → (𝑃‘𝑋) ≠ (𝑃‘𝑌))
179	178	a1d 26	. . . . . . . . . . 11 ⊢ ((𝑌 = 2 ∧ 𝑋 = 3) → (𝑋 ≠ 𝑌 → (𝑃‘𝑋) ≠ (𝑃‘𝑌)))
180	179	ex 417	. . . . . . . . . 10 ⊢ (𝑌 = 2 → (𝑋 = 3 → (𝑋 ≠ 𝑌 → (𝑃‘𝑋) ≠ (𝑃‘𝑌))))
181		simpr 489	. . . . . . . . . . . . 13 ⊢ ((𝑌 = 3 ∧ 𝑋 = 3) → 𝑋 = 3)
182		simpl 487	. . . . . . . . . . . . 13 ⊢ ((𝑌 = 3 ∧ 𝑋 = 3) → 𝑌 = 3)
183	181, 182	neeq12d 3019	. . . . . . . . . . . 12 ⊢ ((𝑌 = 3 ∧ 𝑋 = 3) → (𝑋 ≠ 𝑌 ↔ 3 ≠ 3))
184		eqid 2763	. . . . . . . . . . . . 13 ⊢ 3 = 3
185		eqneqall 2969	. . . . . . . . . . . . 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 417	. . . . . . . . . 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 870	. . . . . . 7 ⊢ ((𝑋 = 2 ∨ 𝑋 = 3) → (𝑌 ∈ {1, 2, 3} → (𝑋 ≠ 𝑌 → (𝑃‘𝑋) ≠ (𝑃‘𝑌))))
192	135, 191	syl 18	. . . . . 6 ⊢ (𝑋 ∈ {2, 3} → (𝑌 ∈ {1, 2, 3} → (𝑋 ≠ 𝑌 → (𝑃‘𝑋) ≠ (𝑃‘𝑌))))
193	134, 192	jaoi 870	. . . . 5 ⊢ ((𝑋 ∈ {0, 1} ∨ 𝑋 ∈ {2, 3}) → (𝑌 ∈ {1, 2, 3} → (𝑋 ≠ 𝑌 → (𝑃‘𝑋) ≠ (𝑃‘𝑌))))
194		elsni 4606	. . . . . 6 ⊢ (𝑋 ∈ {4} → 𝑋 = 4)
195	1	fveq1i 6882	. . . . . . . . . . . . . 14 ⊢ (𝑃‘4) = (⟨“⟨0, 0⟩⟨0, 1⟩⟨1, 1⟩⟨1, 0⟩⟨0, 0⟩”⟩‘4)
196	29, 30, 31	cats1fvn 14900	. . . . . . . . . . . . . . 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 2786	. . . . . . . . . . . . 13 ⊢ (𝑃‘4) = ⟨0, 0⟩
199	198, 45	neeq12i 3024	. . . . . . . . . . . 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 6881	. . . . . . . . . . 11 ⊢ (𝑋 = 4 → (𝑃‘𝑋) = (𝑃‘4))
203	202	adantl 486	. . . . . . . . . 10 ⊢ ((𝑌 = 1 ∧ 𝑋 = 4) → (𝑃‘𝑋) = (𝑃‘4))
204	51	adantr 485	. . . . . . . . . 10 ⊢ ((𝑌 = 1 ∧ 𝑋 = 4) → (𝑃‘𝑌) = (𝑃‘1))
205	201, 203, 204	3netr4d 3035	. . . . . . . . 9 ⊢ ((𝑌 = 1 ∧ 𝑋 = 4) → (𝑃‘𝑋) ≠ (𝑃‘𝑌))
206	205	a1d 26	. . . . . . . 8 ⊢ ((𝑌 = 1 ∧ 𝑋 = 4) → (𝑋 ≠ 𝑌 → (𝑃‘𝑋) ≠ (𝑃‘𝑌)))
207	206	ex 417	. . . . . . 7 ⊢ (𝑌 = 1 → (𝑋 = 4 → (𝑋 ≠ 𝑌 → (𝑃‘𝑋) ≠ (𝑃‘𝑌))))
208	198, 66	neeq12i 3024	. . . . . . . . . . . 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 486	. . . . . . . . . 10 ⊢ ((𝑌 = 2 ∧ 𝑋 = 4) → (𝑃‘𝑋) = (𝑃‘4))
212	71	adantr 485	. . . . . . . . . 10 ⊢ ((𝑌 = 2 ∧ 𝑋 = 4) → (𝑃‘𝑌) = (𝑃‘2))
213	210, 211, 212	3netr4d 3035	. . . . . . . . 9 ⊢ ((𝑌 = 2 ∧ 𝑋 = 4) → (𝑃‘𝑋) ≠ (𝑃‘𝑌))
214	213	a1d 26	. . . . . . . 8 ⊢ ((𝑌 = 2 ∧ 𝑋 = 4) → (𝑋 ≠ 𝑌 → (𝑃‘𝑋) ≠ (𝑃‘𝑌)))
215	214	ex 417	. . . . . . 7 ⊢ (𝑌 = 2 → (𝑋 = 4 → (𝑋 ≠ 𝑌 → (𝑃‘𝑋) ≠ (𝑃‘𝑌))))
216	198, 86	neeq12i 3024	. . . . . . . . . . . 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 486	. . . . . . . . . 10 ⊢ ((𝑌 = 3 ∧ 𝑋 = 4) → (𝑃‘𝑋) = (𝑃‘4))
220	91	adantr 485	. . . . . . . . . 10 ⊢ ((𝑌 = 3 ∧ 𝑋 = 4) → (𝑃‘𝑌) = (𝑃‘3))
221	218, 219, 220	3netr4d 3035	. . . . . . . . 9 ⊢ ((𝑌 = 3 ∧ 𝑋 = 4) → (𝑃‘𝑋) ≠ (𝑃‘𝑌))
222	221	a1d 26	. . . . . . . 8 ⊢ ((𝑌 = 3 ∧ 𝑋 = 4) → (𝑋 ≠ 𝑌 → (𝑃‘𝑋) ≠ (𝑃‘𝑌)))
223	222	ex 417	. . . . . . 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 870	. . . 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 411	. 2 ⊢ ((𝑋 ∈ (({0, 1} ∪ {2, 3}) ∪ {4}) ∧ 𝑌 ∈ {1, 2, 3}) → (𝑋 ≠ 𝑌 → (𝑃‘𝑋) ≠ (𝑃‘𝑌)))
229	14, 16, 228	syl2anb 609	1 ⊢ ((𝑋 ∈ (0..^(♯‘𝑃)) ∧ 𝑌 ∈ (1..^4)) → (𝑋 ≠ 𝑌 → (𝑃‘𝑋) ≠ (𝑃‘𝑌)))

Colors of variables: wff setvar class

This proof depends on syntax axioms: → wi 4 ∧ wa 400 ∨ wo 860 ∨ w3o 1102 = wceq 1570 ∈ wcel 2143 ≠ wne 2958 Vcvv 3455 ∪ cun 3903 {csn 4589 {cpr 4591 {ctp 4593 ⟨cop 4595 ‘cfv 6536 (class class class)co 7410 0cc0 11104 1c1 11105 + caddc 11107 2c2 12299 3c3 12300 4c4 12301 5c5 12302 ℕ₀cn0 12508 ℤ_≥cuz 12866 ..^cfzo 13687 ♯chash 14371 ⟨“cs4 14885 ⟨“cs5 14886

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1825 ax-4 1839 ax-5 1940 ax-6 1997 ax-7 2038 ax-8 2145 ax-9 2153 ax-10 2176 ax-11 2192 ax-12 2213 ax-ext 2735 ax-rep 5238 ax-sep 5257 ax-nul 5269 ax-pow 5336 ax-pr 5404 ax-un 7732 ax-cnex 11160 ax-resscn 11161 ax-1cn 11162 ax-icn 11163 ax-addcl 11164 ax-addrcl 11165 ax-mulcl 11166 ax-mulrcl 11167 ax-mulcom 11168 ax-addass 11169 ax-mulass 11170 ax-distr 11171 ax-i2m1 11172 ax-1ne0 11173 ax-1rid 11174 ax-rnegex 11175 ax-rrecex 11176 ax-cnre 11177 ax-pre-lttri 11178 ax-pre-lttrn 11179 ax-pre-ltadd 11180 ax-pre-mulgt0 11181

This proof depends on definitions: df-bi 210 df-an 401 df-or 861 df-3or 1104 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1810 df-nf 1814 df-sb 2097 df-mo 2567 df-eu 2597 df-clab 2742 df-cleq 2755 df-clel 2838 df-nfc 2912 df-ne 2959 df-nel 3065 df-ral 3080 df-rex 3090 df-reu 3370 df-rab 3417 df-v 3457 df-sbc 3745 df-csb 3854 df-dif 3908 df-un 3910 df-in 3912 df-ss 3922 df-pss 3925 df-nul 4287 df-if 4488 df-pw 4564 df-sn 4590 df-pr 4592 df-tp 4594 df-op 4596 df-uni 4873 df-int 4913 df-iun 4958 df-br 5110 df-opab 5174 df-mpt 5193 df-tr 5219 df-id 5556 df-eprel 5561 df-po 5569 df-so 5570 df-fr 5614 df-we 5616 df-xp 5667 df-rel 5668 df-cnv 5669 df-co 5670 df-dm 5671 df-rn 5672 df-res 5673 df-ima 5674 df-pred 6302 df-ord 6363 df-on 6364 df-lim 6365 df-suc 6366 df-iota 6492 df-fun 6538 df-fn 6539 df-f 6540 df-f1 6541 df-fo 6542 df-f1o 6543 df-fv 6544 df-riota 7367 df-ov 7413 df-oprab 7414 df-mpo 7415 df-om 7859 df-1st 7982 df-2nd 7983 df-frecs 8274 df-wrecs 8305 df-recs 8354 df-rdg 8393 df-1o 8449 df-er 8690 df-en 8940 df-dom 8941 df-sdom 8942 df-fin 8943 df-card 9930 df-pnf 11249 df-mnf 11250 df-xr 11251 df-ltxr 11252 df-le 11253 df-sub 11447 df-neg 11448 df-nn 12238 df-2 12307 df-3 12308 df-4 12309 df-5 12310 df-n0 12509 df-z 12596 df-uz 12867 df-fz 13540 df-fzo 13688 df-hash 14372 df-word 14556 df-concat 14613 df-s1 14639 df-s2 14890 df-s3 14891 df-s4 14892 df-s5 14893

This theorem is used by: gpgprismgr4cycllem11 48898

W3C validator