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 48084

Description: Lemma 7 for gpgprismgr4cycl0 48089: 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 48081	. . . . . 6 ⊢ (♯‘𝑃) = 5
3		df-5 12228	. . . . . 6 ⊢ 5 = (4 + 1)
4	2, 3	eqtri 2752	. . . . 5 ⊢ (♯‘𝑃) = (4 + 1)
5	4	oveq2i 7380	. . . 4 ⊢ (0..^(♯‘𝑃)) = (0..^(4 + 1))
6		4nn0 12437	. . . . . 6 ⊢ 4 ∈ ℕ₀
7		elnn0uz 12814	. . . . . 6 ⊢ (4 ∈ ℕ₀ ↔ 4 ∈ (ℤ_≥‘0))
8	6, 7	mpbi 230	. . . . 5 ⊢ 4 ∈ (ℤ_≥‘0)
9		fzosplitsn 13712	. . . . 5 ⊢ (4 ∈ (ℤ_≥‘0) → (0..^(4 + 1)) = ((0..^4) ∪ {4}))
10	8, 9	ax-mp 5	. . . 4 ⊢ (0..^(4 + 1)) = ((0..^4) ∪ {4})
11		fzo0to42pr 13690	. . . . 5 ⊢ (0..^4) = ({0, 1} ∪ {2, 3})
12	11	uneq1i 4123	. . . 4 ⊢ ((0..^4) ∪ {4}) = (({0, 1} ∪ {2, 3}) ∪ {4})
13	5, 10, 12	3eqtri 2756	. . 3 ⊢ (0..^(♯‘𝑃)) = (({0, 1} ∪ {2, 3}) ∪ {4})
14	13	eleq2i 2820	. 2 ⊢ (𝑋 ∈ (0..^(♯‘𝑃)) ↔ 𝑋 ∈ (({0, 1} ∪ {2, 3}) ∪ {4}))
15		fzo1to4tp 13691	. . 3 ⊢ (1..^4) = {1, 2, 3}
16	15	eleq2i 2820	. 2 ⊢ (𝑌 ∈ (1..^4) ↔ 𝑌 ∈ {1, 2, 3})
17		elun 4112	. . . . 5 ⊢ (𝑋 ∈ (({0, 1} ∪ {2, 3}) ∪ {4}) ↔ (𝑋 ∈ ({0, 1} ∪ {2, 3}) ∨ 𝑋 ∈ {4}))
18		elun 4112	. . . . . 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 4609	. . . . . . 7 ⊢ (𝑋 ∈ {0, 1} → (𝑋 = 0 ∨ 𝑋 = 1))
22		0ne1 12233	. . . . . . . . . . . . . . . . 17 ⊢ 0 ≠ 1
23	22	olci 866	. . . . . . . . . . . . . . . 16 ⊢ (0 ≠ 0 ∨ 0 ≠ 1)
24		c0ex 11144	. . . . . . . . . . . . . . . . 17 ⊢ 0 ∈ V
25	24, 24	opthne 5437	. . . . . . . . . . . . . . . 16 ⊢ (⟨0, 0⟩ ≠ ⟨0, 1⟩ ↔ (0 ≠ 0 ∨ 0 ≠ 1))
26	23, 25	mpbir 231	. . . . . . . . . . . . . . 15 ⊢ ⟨0, 0⟩ ≠ ⟨0, 1⟩
27	1	fveq1i 6841	. . . . . . . . . . . . . . . . 17 ⊢ (𝑃‘0) = (⟨“⟨0, 0⟩⟨0, 1⟩⟨1, 1⟩⟨1, 0⟩⟨0, 0⟩”⟩‘0)
28		opex 5419	. . . . . . . . . . . . . . . . . 18 ⊢ ⟨0, 0⟩ ∈ V
29		df-s5 14793	. . . . . . . . . . . . . . . . . . 19 ⊢ ⟨“⟨0, 0⟩⟨0, 1⟩⟨1, 1⟩⟨1, 0⟩⟨0, 0⟩”⟩ = (⟨“⟨0, 0⟩⟨0, 1⟩⟨1, 1⟩⟨1, 0⟩”⟩ ++ ⟨“⟨0, 0⟩”⟩)
30		s4cli 14824	. . . . . . . . . . . . . . . . . . 19 ⊢ ⟨“⟨0, 0⟩⟨0, 1⟩⟨1, 1⟩⟨1, 0⟩”⟩ ∈ Word V
31		s4len 14841	. . . . . . . . . . . . . . . . . . 19 ⊢ (♯‘⟨“⟨0, 0⟩⟨0, 1⟩⟨1, 1⟩⟨1, 0⟩”⟩) = 4
32		s4fv0 14837	. . . . . . . . . . . . . . . . . . 19 ⊢ (⟨0, 0⟩ ∈ V → (⟨“⟨0, 0⟩⟨0, 1⟩⟨1, 1⟩⟨1, 0⟩”⟩‘0) = ⟨0, 0⟩)
33		0nn0 12433	. . . . . . . . . . . . . . . . . . 19 ⊢ 0 ∈ ℕ₀
34		4pos 12269	. . . . . . . . . . . . . . . . . . 19 ⊢ 0 < 4
35	29, 30, 31, 32, 33, 34	cats1fv 14801	. . . . . . . . . . . . . . . . . 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 2752	. . . . . . . . . . . . . . . 16 ⊢ (𝑃‘0) = ⟨0, 0⟩
38	1	fveq1i 6841	. . . . . . . . . . . . . . . . 17 ⊢ (𝑃‘1) = (⟨“⟨0, 0⟩⟨0, 1⟩⟨1, 1⟩⟨1, 0⟩⟨0, 0⟩”⟩‘1)
39		opex 5419	. . . . . . . . . . . . . . . . . 18 ⊢ ⟨0, 1⟩ ∈ V
40		s4fv1 14838	. . . . . . . . . . . . . . . . . . 19 ⊢ (⟨0, 1⟩ ∈ V → (⟨“⟨0, 0⟩⟨0, 1⟩⟨1, 1⟩⟨1, 0⟩”⟩‘1) = ⟨0, 1⟩)
41		1nn0 12434	. . . . . . . . . . . . . . . . . . 19 ⊢ 1 ∈ ℕ₀
42		1lt4 12333	. . . . . . . . . . . . . . . . . . 19 ⊢ 1 < 4
43	29, 30, 31, 40, 41, 42	cats1fv 14801	. . . . . . . . . . . . . . . . . 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 2752	. . . . . . . . . . . . . . . 16 ⊢ (𝑃‘1) = ⟨0, 1⟩
46	37, 45	neeq12i 2991	. . . . . . . . . . . . . . 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 6840	. . . . . . . . . . . . . 14 ⊢ (𝑋 = 0 → (𝑃‘𝑋) = (𝑃‘0))
50	49	adantl 481	. . . . . . . . . . . . 13 ⊢ ((𝑌 = 1 ∧ 𝑋 = 0) → (𝑃‘𝑋) = (𝑃‘0))
51		fveq2 6840	. . . . . . . . . . . . . 14 ⊢ (𝑌 = 1 → (𝑃‘𝑌) = (𝑃‘1))
52	51	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝑌 = 1 ∧ 𝑋 = 0) → (𝑃‘𝑌) = (𝑃‘1))
53	48, 50, 52	3netr4d 3002	. . . . . . . . . . . 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 5437	. . . . . . . . . . . . . . . 16 ⊢ (⟨0, 0⟩ ≠ ⟨1, 1⟩ ↔ (0 ≠ 1 ∨ 0 ≠ 1))
58	56, 57	mpbir 231	. . . . . . . . . . . . . . 15 ⊢ ⟨0, 0⟩ ≠ ⟨1, 1⟩
59	1	fveq1i 6841	. . . . . . . . . . . . . . . . 17 ⊢ (𝑃‘2) = (⟨“⟨0, 0⟩⟨0, 1⟩⟨1, 1⟩⟨1, 0⟩⟨0, 0⟩”⟩‘2)
60		opex 5419	. . . . . . . . . . . . . . . . . 18 ⊢ ⟨1, 1⟩ ∈ V
61		s4fv2 14839	. . . . . . . . . . . . . . . . . . 19 ⊢ (⟨1, 1⟩ ∈ V → (⟨“⟨0, 0⟩⟨0, 1⟩⟨1, 1⟩⟨1, 0⟩”⟩‘2) = ⟨1, 1⟩)
62		2nn0 12435	. . . . . . . . . . . . . . . . . . 19 ⊢ 2 ∈ ℕ₀
63		2lt4 12332	. . . . . . . . . . . . . . . . . . 19 ⊢ 2 < 4
64	29, 30, 31, 61, 62, 63	cats1fv 14801	. . . . . . . . . . . . . . . . . 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 2752	. . . . . . . . . . . . . . . 16 ⊢ (𝑃‘2) = ⟨1, 1⟩
67	37, 66	neeq12i 2991	. . . . . . . . . . . . . . 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 6840	. . . . . . . . . . . . . 14 ⊢ (𝑌 = 2 → (𝑃‘𝑌) = (𝑃‘2))
72	71	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝑌 = 2 ∧ 𝑋 = 0) → (𝑃‘𝑌) = (𝑃‘2))
73	69, 70, 72	3netr4d 3002	. . . . . . . . . . . 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 5437	. . . . . . . . . . . . . . . 16 ⊢ (⟨0, 0⟩ ≠ ⟨1, 0⟩ ↔ (0 ≠ 1 ∨ 0 ≠ 0))
78	76, 77	mpbir 231	. . . . . . . . . . . . . . 15 ⊢ ⟨0, 0⟩ ≠ ⟨1, 0⟩
79	1	fveq1i 6841	. . . . . . . . . . . . . . . . 17 ⊢ (𝑃‘3) = (⟨“⟨0, 0⟩⟨0, 1⟩⟨1, 1⟩⟨1, 0⟩⟨0, 0⟩”⟩‘3)
80		opex 5419	. . . . . . . . . . . . . . . . . 18 ⊢ ⟨1, 0⟩ ∈ V
81		s4fv3 14840	. . . . . . . . . . . . . . . . . . 19 ⊢ (⟨1, 0⟩ ∈ V → (⟨“⟨0, 0⟩⟨0, 1⟩⟨1, 1⟩⟨1, 0⟩”⟩‘3) = ⟨1, 0⟩)
82		3nn0 12436	. . . . . . . . . . . . . . . . . . 19 ⊢ 3 ∈ ℕ₀
83		3lt4 12331	. . . . . . . . . . . . . . . . . . 19 ⊢ 3 < 4
84	29, 30, 31, 81, 82, 83	cats1fv 14801	. . . . . . . . . . . . . . . . . 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 2752	. . . . . . . . . . . . . . . 16 ⊢ (𝑃‘3) = ⟨1, 0⟩
87	37, 86	neeq12i 2991	. . . . . . . . . . . . . . 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 6840	. . . . . . . . . . . . . 14 ⊢ (𝑌 = 3 → (𝑃‘𝑌) = (𝑃‘3))
92	91	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝑌 = 3 ∧ 𝑋 = 0) → (𝑃‘𝑌) = (𝑃‘3))
93	89, 90, 92	3netr4d 3002	. . . . . . . . . . . 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 4648	. . . . . . . . 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 2986	. . . . . . . . . . . 12 ⊢ ((𝑌 = 1 ∧ 𝑋 = 1) → (𝑋 ≠ 𝑌 ↔ 1 ≠ 1))
102		eqid 2729	. . . . . . . . . . . . 13 ⊢ 1 = 1
103		eqneqall 2936	. . . . . . . . . . . . 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 11146	. . . . . . . . . . . . . . . . 17 ⊢ 1 ∈ V
109	24, 108	opthne 5437	. . . . . . . . . . . . . . . 16 ⊢ (⟨0, 1⟩ ≠ ⟨1, 1⟩ ↔ (0 ≠ 1 ∨ 1 ≠ 1))
110	107, 109	mpbir 231	. . . . . . . . . . . . . . 15 ⊢ ⟨0, 1⟩ ≠ ⟨1, 1⟩
111	45, 66	neeq12i 2991	. . . . . . . . . . . . . . 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 6840	. . . . . . . . . . . . . 14 ⊢ (𝑋 = 1 → (𝑃‘𝑋) = (𝑃‘1))
115	114	adantl 481	. . . . . . . . . . . . 13 ⊢ ((𝑌 = 2 ∧ 𝑋 = 1) → (𝑃‘𝑋) = (𝑃‘1))
116	71	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝑌 = 2 ∧ 𝑋 = 1) → (𝑃‘𝑌) = (𝑃‘2))
117	113, 115, 116	3netr4d 3002	. . . . . . . . . . . 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 5437	. . . . . . . . . . . . . . . 16 ⊢ (⟨0, 1⟩ ≠ ⟨1, 0⟩ ↔ (0 ≠ 1 ∨ 1 ≠ 0))
122	120, 121	mpbir 231	. . . . . . . . . . . . . . 15 ⊢ ⟨0, 1⟩ ≠ ⟨1, 0⟩
123	45, 86	neeq12i 2991	. . . . . . . . . . . . . . 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 3002	. . . . . . . . . . . 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 4609	. . . . . . 7 ⊢ (𝑋 ∈ {2, 3} → (𝑋 = 2 ∨ 𝑋 = 3))
136	112	necomi 2979	. . . . . . . . . . . . . 14 ⊢ (𝑃‘2) ≠ (𝑃‘1)
137	136	a1i 11	. . . . . . . . . . . . 13 ⊢ ((𝑌 = 1 ∧ 𝑋 = 2) → (𝑃‘2) ≠ (𝑃‘1))
138		fveq2 6840	. . . . . . . . . . . . . 14 ⊢ (𝑋 = 2 → (𝑃‘𝑋) = (𝑃‘2))
139	138	adantl 481	. . . . . . . . . . . . 13 ⊢ ((𝑌 = 1 ∧ 𝑋 = 2) → (𝑃‘𝑋) = (𝑃‘2))
140	51	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝑌 = 1 ∧ 𝑋 = 2) → (𝑃‘𝑌) = (𝑃‘1))
141	137, 139, 140	3netr4d 3002	. . . . . . . . . . . 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 2986	. . . . . . . . . . . 12 ⊢ ((𝑌 = 2 ∧ 𝑋 = 2) → (𝑋 ≠ 𝑌 ↔ 2 ≠ 2))
147		eqid 2729	. . . . . . . . . . . . 13 ⊢ 2 = 2
148		eqneqall 2936	. . . . . . . . . . . . 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 2979	. . . . . . . . . . . . . . . . 17 ⊢ 1 ≠ 0
153	152	olci 866	. . . . . . . . . . . . . . . 16 ⊢ (1 ≠ 1 ∨ 1 ≠ 0)
154	108, 108	opthne 5437	. . . . . . . . . . . . . . . 16 ⊢ (⟨1, 1⟩ ≠ ⟨1, 0⟩ ↔ (1 ≠ 1 ∨ 1 ≠ 0))
155	153, 154	mpbir 231	. . . . . . . . . . . . . . 15 ⊢ ⟨1, 1⟩ ≠ ⟨1, 0⟩
156	66, 86	neeq12i 2991	. . . . . . . . . . . . . . 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 3002	. . . . . . . . . . . 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 2979	. . . . . . . . . . . . . 14 ⊢ (𝑃‘3) ≠ (𝑃‘1)
167	166	a1i 11	. . . . . . . . . . . . 13 ⊢ ((𝑌 = 1 ∧ 𝑋 = 3) → (𝑃‘3) ≠ (𝑃‘1))
168		fveq2 6840	. . . . . . . . . . . . . 14 ⊢ (𝑋 = 3 → (𝑃‘𝑋) = (𝑃‘3))
169	168	adantl 481	. . . . . . . . . . . . 13 ⊢ ((𝑌 = 1 ∧ 𝑋 = 3) → (𝑃‘𝑋) = (𝑃‘3))
170	51	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝑌 = 1 ∧ 𝑋 = 3) → (𝑃‘𝑌) = (𝑃‘1))
171	167, 169, 170	3netr4d 3002	. . . . . . . . . . . 12 ⊢ ((𝑌 = 1 ∧ 𝑋 = 3) → (𝑃‘𝑋) ≠ (𝑃‘𝑌))
172	171	a1d 25	. . . . . . . . . . 11 ⊢ ((𝑌 = 1 ∧ 𝑋 = 3) → (𝑋 ≠ 𝑌 → (𝑃‘𝑋) ≠ (𝑃‘𝑌)))
173	172	ex 412	. . . . . . . . . 10 ⊢ (𝑌 = 1 → (𝑋 = 3 → (𝑋 ≠ 𝑌 → (𝑃‘𝑋) ≠ (𝑃‘𝑌))))
174	157	necomi 2979	. . . . . . . . . . . . . 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 3002	. . . . . . . . . . . 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 2986	. . . . . . . . . . . 12 ⊢ ((𝑌 = 3 ∧ 𝑋 = 3) → (𝑋 ≠ 𝑌 ↔ 3 ≠ 3))
184		eqid 2729	. . . . . . . . . . . . 13 ⊢ 3 = 3
185		eqneqall 2936	. . . . . . . . . . . . 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 4602	. . . . . 6 ⊢ (𝑋 ∈ {4} → 𝑋 = 4)
195	1	fveq1i 6841	. . . . . . . . . . . . . 14 ⊢ (𝑃‘4) = (⟨“⟨0, 0⟩⟨0, 1⟩⟨1, 1⟩⟨1, 0⟩⟨0, 0⟩”⟩‘4)
196	29, 30, 31	cats1fvn 14800	. . . . . . . . . . . . . . 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 2752	. . . . . . . . . . . . 13 ⊢ (𝑃‘4) = ⟨0, 0⟩
199	198, 45	neeq12i 2991	. . . . . . . . . . . 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 6840	. . . . . . . . . . 11 ⊢ (𝑋 = 4 → (𝑃‘𝑋) = (𝑃‘4))
203	202	adantl 481	. . . . . . . . . 10 ⊢ ((𝑌 = 1 ∧ 𝑋 = 4) → (𝑃‘𝑋) = (𝑃‘4))
204	51	adantr 480	. . . . . . . . . 10 ⊢ ((𝑌 = 1 ∧ 𝑋 = 4) → (𝑃‘𝑌) = (𝑃‘1))
205	201, 203, 204	3netr4d 3002	. . . . . . . . 9 ⊢ ((𝑌 = 1 ∧ 𝑋 = 4) → (𝑃‘𝑋) ≠ (𝑃‘𝑌))
206	205	a1d 25	. . . . . . . 8 ⊢ ((𝑌 = 1 ∧ 𝑋 = 4) → (𝑋 ≠ 𝑌 → (𝑃‘𝑋) ≠ (𝑃‘𝑌)))
207	206	ex 412	. . . . . . 7 ⊢ (𝑌 = 1 → (𝑋 = 4 → (𝑋 ≠ 𝑌 → (𝑃‘𝑋) ≠ (𝑃‘𝑌))))
208	198, 66	neeq12i 2991	. . . . . . . . . . . 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 3002	. . . . . . . . 9 ⊢ ((𝑌 = 2 ∧ 𝑋 = 4) → (𝑃‘𝑋) ≠ (𝑃‘𝑌))
214	213	a1d 25	. . . . . . . 8 ⊢ ((𝑌 = 2 ∧ 𝑋 = 4) → (𝑋 ≠ 𝑌 → (𝑃‘𝑋) ≠ (𝑃‘𝑌)))
215	214	ex 412	. . . . . . 7 ⊢ (𝑌 = 2 → (𝑋 = 4 → (𝑋 ≠ 𝑌 → (𝑃‘𝑋) ≠ (𝑃‘𝑌))))
216	198, 86	neeq12i 2991	. . . . . . . . . . . 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 3002	. . . . . . . . 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 1540 ∈ wcel 2109 ≠ wne 2925 Vcvv 3444 ∪ cun 3909 {csn 4585 {cpr 4587 {ctp 4589 ⟨cop 4591 ‘cfv 6499 (class class class)co 7369 0cc0 11044 1c1 11045 + caddc 11047 2c2 12217 3c3 12218 4c4 12219 5c5 12220 ℕ₀cn0 12418 ℤ_≥cuz 12769 ..^cfzo 13591 ♯chash 14271 ⟨“cs4 14785 ⟨“cs5 14786

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2008 ax-8 2111 ax-9 2119 ax-10 2142 ax-11 2158 ax-12 2178 ax-ext 2701 ax-rep 5229 ax-sep 5246 ax-nul 5256 ax-pow 5315 ax-pr 5382 ax-un 7691 ax-cnex 11100 ax-resscn 11101 ax-1cn 11102 ax-icn 11103 ax-addcl 11104 ax-addrcl 11105 ax-mulcl 11106 ax-mulrcl 11107 ax-mulcom 11108 ax-addass 11109 ax-mulass 11110 ax-distr 11111 ax-i2m1 11112 ax-1ne0 11113 ax-1rid 11114 ax-rnegex 11115 ax-rrecex 11116 ax-cnre 11117 ax-pre-lttri 11118 ax-pre-lttrn 11119 ax-pre-ltadd 11120 ax-pre-mulgt0 11121

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2066 df-mo 2533 df-eu 2562 df-clab 2708 df-cleq 2721 df-clel 2803 df-nfc 2878 df-ne 2926 df-nel 3030 df-ral 3045 df-rex 3054 df-reu 3352 df-rab 3403 df-v 3446 df-sbc 3751 df-csb 3860 df-dif 3914 df-un 3916 df-in 3918 df-ss 3928 df-pss 3931 df-nul 4293 df-if 4485 df-pw 4561 df-sn 4586 df-pr 4588 df-tp 4590 df-op 4592 df-uni 4868 df-int 4907 df-iun 4953 df-br 5103 df-opab 5165 df-mpt 5184 df-tr 5210 df-id 5526 df-eprel 5531 df-po 5539 df-so 5540 df-fr 5584 df-we 5586 df-xp 5637 df-rel 5638 df-cnv 5639 df-co 5640 df-dm 5641 df-rn 5642 df-res 5643 df-ima 5644 df-pred 6262 df-ord 6323 df-on 6324 df-lim 6325 df-suc 6326 df-iota 6452 df-fun 6501 df-fn 6502 df-f 6503 df-f1 6504 df-fo 6505 df-f1o 6506 df-fv 6507 df-riota 7326 df-ov 7372 df-oprab 7373 df-mpo 7374 df-om 7823 df-1st 7947 df-2nd 7948 df-frecs 8237 df-wrecs 8268 df-recs 8317 df-rdg 8355 df-1o 8411 df-er 8648 df-en 8896 df-dom 8897 df-sdom 8898 df-fin 8899 df-card 9868 df-pnf 11186 df-mnf 11187 df-xr 11188 df-ltxr 11189 df-le 11190 df-sub 11383 df-neg 11384 df-nn 12163 df-2 12225 df-3 12226 df-4 12227 df-5 12228 df-n0 12419 df-z 12506 df-uz 12770 df-fz 13445 df-fzo 13592 df-hash 14272 df-word 14455 df-concat 14512 df-s1 14537 df-s2 14790 df-s3 14791 df-s4 14792 df-s5 14793

This theorem is referenced by: gpgprismgr4cycllem11 48088

W3C validator