pgnbgreunbgrlem2lem3 - Mathbox for Alexander van der Vekens

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

Theorem pgnbgreunbgrlem2lem3 49215

Description: Lemma 3 for pgnbgreunbgrlem2 49216. (Contributed by AV, 17-Nov-2025.)

**Hypotheses**
Ref	Expression
pgnbgreunbgr.g	⊢ 𝐺 = (5 gPetersenGr 2)
pgnbgreunbgr.v	⊢ 𝑉 = (Vtx‘𝐺)
pgnbgreunbgr.e	⊢ 𝐸 = (Edg‘𝐺)
pgnbgreunbgr.n	⊢ 𝑁 = (𝐺 NeighbVtx 𝑋)

**Assertion**
Ref	Expression
pgnbgreunbgrlem2lem3	⊢ ((((𝐿 = ⟨1, ((𝑦 + 2) mod 5)⟩ ∧ 𝐾 = ⟨1, ((𝑦 − 2) mod 5)⟩) ∧ (𝑏 ∈ (0..^5) ∧ 𝑦 ∈ (0..^5))) ∧ {𝐾, ⟨0, 𝑏⟩} ∈ 𝐸) → ¬ {⟨0, 𝑏⟩, 𝐿} ∈ 𝐸)

Distinct variable group: 𝑦,𝑏 Allowed substitution hints: 𝐸(𝑦, 𝑏) 𝐺(𝑦, 𝑏) 𝐾(𝑦, 𝑏) 𝐿(𝑦, 𝑏) 𝑁(𝑦, 𝑏) 𝑉(𝑦, 𝑏) 𝑋(𝑦, 𝑏)

**Proof of Theorem pgnbgreunbgrlem2lem3**
Step	Hyp	Ref	Expression
1		prcom 4693	. . . . . . . 8 ⊢ {⟨1, ((𝑦 − 2) mod 5)⟩, ⟨0, 𝑏⟩} = {⟨0, 𝑏⟩, ⟨1, ((𝑦 − 2) mod 5)⟩}
2	1	eleq1i 2852	. . . . . . 7 ⊢ ({⟨1, ((𝑦 − 2) mod 5)⟩, ⟨0, 𝑏⟩} ∈ 𝐸 ↔ {⟨0, 𝑏⟩, ⟨1, ((𝑦 − 2) mod 5)⟩} ∈ 𝐸)
3	2	a1i 11	. . . . . 6 ⊢ ((𝑏 ∈ (0..^5) ∧ 𝑦 ∈ (0..^5)) → ({⟨1, ((𝑦 − 2) mod 5)⟩, ⟨0, 𝑏⟩} ∈ 𝐸 ↔ {⟨0, 𝑏⟩, ⟨1, ((𝑦 − 2) mod 5)⟩} ∈ 𝐸))
4		5eluz3 13011	. . . . . . . 8 ⊢ 5 ∈ (ℤ_≥‘3)
5		pglem 49190	. . . . . . . 8 ⊢ 2 ∈ (1..^(⌈‘(5 / 2)))
6	4, 5	pm3.2i 476	. . . . . . 7 ⊢ (5 ∈ (ℤ_≥‘3) ∧ 2 ∈ (1..^(⌈‘(5 / 2))))
7		c0ex 11301	. . . . . . . 8 ⊢ 0 ∈ V
8		vex 3455	. . . . . . . 8 ⊢ 𝑏 ∈ V
9	7, 8	op1st 8010	. . . . . . 7 ⊢ (1^st ‘⟨0, 𝑏⟩) = 0
10		eqid 2761	. . . . . . . 8 ⊢ (1..^(⌈‘(5 / 2))) = (1..^(⌈‘(5 / 2)))
11		pgnbgreunbgr.g	. . . . . . . 8 ⊢ 𝐺 = (5 gPetersenGr 2)
12		pgnbgreunbgr.v	. . . . . . . 8 ⊢ 𝑉 = (Vtx‘𝐺)
13		pgnbgreunbgr.e	. . . . . . . 8 ⊢ 𝐸 = (Edg‘𝐺)
14	10, 11, 12, 13	gpgvtxedg0 49162	. . . . . . 7 ⊢ (((5 ∈ (ℤ_≥‘3) ∧ 2 ∈ (1..^(⌈‘(5 / 2)))) ∧ (1^st ‘⟨0, 𝑏⟩) = 0 ∧ {⟨0, 𝑏⟩, ⟨1, ((𝑦 − 2) mod 5)⟩} ∈ 𝐸) → (⟨1, ((𝑦 − 2) mod 5)⟩ = ⟨0, (((2^nd ‘⟨0, 𝑏⟩) + 1) mod 5)⟩ ∨ ⟨1, ((𝑦 − 2) mod 5)⟩ = ⟨1, (2^nd ‘⟨0, 𝑏⟩)⟩ ∨ ⟨1, ((𝑦 − 2) mod 5)⟩ = ⟨0, (((2^nd ‘⟨0, 𝑏⟩) − 1) mod 5)⟩))
15	6, 9, 14	mp3an12 1480	. . . . . 6 ⊢ ({⟨0, 𝑏⟩, ⟨1, ((𝑦 − 2) mod 5)⟩} ∈ 𝐸 → (⟨1, ((𝑦 − 2) mod 5)⟩ = ⟨0, (((2^nd ‘⟨0, 𝑏⟩) + 1) mod 5)⟩ ∨ ⟨1, ((𝑦 − 2) mod 5)⟩ = ⟨1, (2^nd ‘⟨0, 𝑏⟩)⟩ ∨ ⟨1, ((𝑦 − 2) mod 5)⟩ = ⟨0, (((2^nd ‘⟨0, 𝑏⟩) − 1) mod 5)⟩))
16	3, 15	biimtrdi 256	. . . . 5 ⊢ ((𝑏 ∈ (0..^5) ∧ 𝑦 ∈ (0..^5)) → ({⟨1, ((𝑦 − 2) mod 5)⟩, ⟨0, 𝑏⟩} ∈ 𝐸 → (⟨1, ((𝑦 − 2) mod 5)⟩ = ⟨0, (((2^nd ‘⟨0, 𝑏⟩) + 1) mod 5)⟩ ∨ ⟨1, ((𝑦 − 2) mod 5)⟩ = ⟨1, (2^nd ‘⟨0, 𝑏⟩)⟩ ∨ ⟨1, ((𝑦 − 2) mod 5)⟩ = ⟨0, (((2^nd ‘⟨0, 𝑏⟩) − 1) mod 5)⟩)))
17	10, 11, 12, 13	gpgvtxedg0 49162	. . . . . . . . 9 ⊢ (((5 ∈ (ℤ_≥‘3) ∧ 2 ∈ (1..^(⌈‘(5 / 2)))) ∧ (1^st ‘⟨0, 𝑏⟩) = 0 ∧ {⟨0, 𝑏⟩, ⟨1, ((𝑦 + 2) mod 5)⟩} ∈ 𝐸) → (⟨1, ((𝑦 + 2) mod 5)⟩ = ⟨0, (((2^nd ‘⟨0, 𝑏⟩) + 1) mod 5)⟩ ∨ ⟨1, ((𝑦 + 2) mod 5)⟩ = ⟨1, (2^nd ‘⟨0, 𝑏⟩)⟩ ∨ ⟨1, ((𝑦 + 2) mod 5)⟩ = ⟨0, (((2^nd ‘⟨0, 𝑏⟩) − 1) mod 5)⟩))
18	6, 9, 17	mp3an12 1480	. . . . . . . 8 ⊢ ({⟨0, 𝑏⟩, ⟨1, ((𝑦 + 2) mod 5)⟩} ∈ 𝐸 → (⟨1, ((𝑦 + 2) mod 5)⟩ = ⟨0, (((2^nd ‘⟨0, 𝑏⟩) + 1) mod 5)⟩ ∨ ⟨1, ((𝑦 + 2) mod 5)⟩ = ⟨1, (2^nd ‘⟨0, 𝑏⟩)⟩ ∨ ⟨1, ((𝑦 + 2) mod 5)⟩ = ⟨0, (((2^nd ‘⟨0, 𝑏⟩) − 1) mod 5)⟩))
19		1ex 11304	. . . . . . . . . . 11 ⊢ 1 ∈ V
20		ovex 7454	. . . . . . . . . . 11 ⊢ ((𝑦 + 2) mod 5) ∈ V
21	19, 20	opth 5445	. . . . . . . . . 10 ⊢ (⟨1, ((𝑦 + 2) mod 5)⟩ = ⟨0, (((2^nd ‘⟨0, 𝑏⟩) + 1) mod 5)⟩ ↔ (1 = 0 ∧ ((𝑦 + 2) mod 5) = (((2^nd ‘⟨0, 𝑏⟩) + 1) mod 5)))
22		ax-1ne0 11270	. . . . . . . . . . . 12 ⊢ 1 ≠ 0
23		eqneqall 2967	. . . . . . . . . . . 12 ⊢ (1 = 0 → (1 ≠ 0 → (((𝑏 ∈ (0..^5) ∧ 𝑦 ∈ (0..^5)) ∧ (⟨1, ((𝑦 − 2) mod 5)⟩ = ⟨0, (((2^nd ‘⟨0, 𝑏⟩) + 1) mod 5)⟩ ∨ ⟨1, ((𝑦 − 2) mod 5)⟩ = ⟨1, (2^nd ‘⟨0, 𝑏⟩)⟩ ∨ ⟨1, ((𝑦 − 2) mod 5)⟩ = ⟨0, (((2^nd ‘⟨0, 𝑏⟩) − 1) mod 5)⟩)) → ¬ {⟨0, 𝑏⟩, ⟨1, ((𝑦 + 2) mod 5)⟩} ∈ 𝐸)))
24	22, 23	mpi 21	. . . . . . . . . . 11 ⊢ (1 = 0 → (((𝑏 ∈ (0..^5) ∧ 𝑦 ∈ (0..^5)) ∧ (⟨1, ((𝑦 − 2) mod 5)⟩ = ⟨0, (((2^nd ‘⟨0, 𝑏⟩) + 1) mod 5)⟩ ∨ ⟨1, ((𝑦 − 2) mod 5)⟩ = ⟨1, (2^nd ‘⟨0, 𝑏⟩)⟩ ∨ ⟨1, ((𝑦 − 2) mod 5)⟩ = ⟨0, (((2^nd ‘⟨0, 𝑏⟩) − 1) mod 5)⟩)) → ¬ {⟨0, 𝑏⟩, ⟨1, ((𝑦 + 2) mod 5)⟩} ∈ 𝐸))
25	24	adantr 486	. . . . . . . . . 10 ⊢ ((1 = 0 ∧ ((𝑦 + 2) mod 5) = (((2^nd ‘⟨0, 𝑏⟩) + 1) mod 5)) → (((𝑏 ∈ (0..^5) ∧ 𝑦 ∈ (0..^5)) ∧ (⟨1, ((𝑦 − 2) mod 5)⟩ = ⟨0, (((2^nd ‘⟨0, 𝑏⟩) + 1) mod 5)⟩ ∨ ⟨1, ((𝑦 − 2) mod 5)⟩ = ⟨1, (2^nd ‘⟨0, 𝑏⟩)⟩ ∨ ⟨1, ((𝑦 − 2) mod 5)⟩ = ⟨0, (((2^nd ‘⟨0, 𝑏⟩) − 1) mod 5)⟩)) → ¬ {⟨0, 𝑏⟩, ⟨1, ((𝑦 + 2) mod 5)⟩} ∈ 𝐸))
26	21, 25	sylbi 220	. . . . . . . . 9 ⊢ (⟨1, ((𝑦 + 2) mod 5)⟩ = ⟨0, (((2^nd ‘⟨0, 𝑏⟩) + 1) mod 5)⟩ → (((𝑏 ∈ (0..^5) ∧ 𝑦 ∈ (0..^5)) ∧ (⟨1, ((𝑦 − 2) mod 5)⟩ = ⟨0, (((2^nd ‘⟨0, 𝑏⟩) + 1) mod 5)⟩ ∨ ⟨1, ((𝑦 − 2) mod 5)⟩ = ⟨1, (2^nd ‘⟨0, 𝑏⟩)⟩ ∨ ⟨1, ((𝑦 − 2) mod 5)⟩ = ⟨0, (((2^nd ‘⟨0, 𝑏⟩) − 1) mod 5)⟩)) → ¬ {⟨0, 𝑏⟩, ⟨1, ((𝑦 + 2) mod 5)⟩} ∈ 𝐸))
27	19, 20	opth 5445	. . . . . . . . . 10 ⊢ (⟨1, ((𝑦 + 2) mod 5)⟩ = ⟨1, (2^nd ‘⟨0, 𝑏⟩)⟩ ↔ (1 = 1 ∧ ((𝑦 + 2) mod 5) = (2^nd ‘⟨0, 𝑏⟩)))
28	7, 8	op2nd 8011	. . . . . . . . . . . 12 ⊢ (2^nd ‘⟨0, 𝑏⟩) = 𝑏
29	28	eqeq2i 2774	. . . . . . . . . . 11 ⊢ (((𝑦 + 2) mod 5) = (2^nd ‘⟨0, 𝑏⟩) ↔ ((𝑦 + 2) mod 5) = 𝑏)
30		ovex 7454	. . . . . . . . . . . . . . . 16 ⊢ ((𝑦 − 2) mod 5) ∈ V
31	19, 30	opth 5445	. . . . . . . . . . . . . . 15 ⊢ (⟨1, ((𝑦 − 2) mod 5)⟩ = ⟨0, (((2^nd ‘⟨0, 𝑏⟩) + 1) mod 5)⟩ ↔ (1 = 0 ∧ ((𝑦 − 2) mod 5) = (((2^nd ‘⟨0, 𝑏⟩) + 1) mod 5)))
32		eqneqall 2967	. . . . . . . . . . . . . . . . 17 ⊢ (1 = 0 → (1 ≠ 0 → ((𝑏 ∈ (0..^5) ∧ 𝑦 ∈ (0..^5)) → (((𝑦 + 2) mod 5) = 𝑏 → ¬ {⟨0, 𝑏⟩, ⟨1, ((𝑦 + 2) mod 5)⟩} ∈ 𝐸))))
33	22, 32	mpi 21	. . . . . . . . . . . . . . . 16 ⊢ (1 = 0 → ((𝑏 ∈ (0..^5) ∧ 𝑦 ∈ (0..^5)) → (((𝑦 + 2) mod 5) = 𝑏 → ¬ {⟨0, 𝑏⟩, ⟨1, ((𝑦 + 2) mod 5)⟩} ∈ 𝐸)))
34	33	adantr 486	. . . . . . . . . . . . . . 15 ⊢ ((1 = 0 ∧ ((𝑦 − 2) mod 5) = (((2^nd ‘⟨0, 𝑏⟩) + 1) mod 5)) → ((𝑏 ∈ (0..^5) ∧ 𝑦 ∈ (0..^5)) → (((𝑦 + 2) mod 5) = 𝑏 → ¬ {⟨0, 𝑏⟩, ⟨1, ((𝑦 + 2) mod 5)⟩} ∈ 𝐸)))
35	31, 34	sylbi 220	. . . . . . . . . . . . . 14 ⊢ (⟨1, ((𝑦 − 2) mod 5)⟩ = ⟨0, (((2^nd ‘⟨0, 𝑏⟩) + 1) mod 5)⟩ → ((𝑏 ∈ (0..^5) ∧ 𝑦 ∈ (0..^5)) → (((𝑦 + 2) mod 5) = 𝑏 → ¬ {⟨0, 𝑏⟩, ⟨1, ((𝑦 + 2) mod 5)⟩} ∈ 𝐸)))
36	19, 30	opth 5445	. . . . . . . . . . . . . . 15 ⊢ (⟨1, ((𝑦 − 2) mod 5)⟩ = ⟨1, (2^nd ‘⟨0, 𝑏⟩)⟩ ↔ (1 = 1 ∧ ((𝑦 − 2) mod 5) = (2^nd ‘⟨0, 𝑏⟩)))
37	28	eqeq2i 2774	. . . . . . . . . . . . . . . 16 ⊢ (((𝑦 − 2) mod 5) = (2^nd ‘⟨0, 𝑏⟩) ↔ ((𝑦 − 2) mod 5) = 𝑏)
38		eqeq2 2773	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑏 = ((𝑦 − 2) mod 5) → (((𝑦 + 2) mod 5) = 𝑏 ↔ ((𝑦 + 2) mod 5) = ((𝑦 − 2) mod 5)))
39	38	eqcoms 2769	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑦 − 2) mod 5) = 𝑏 → (((𝑦 + 2) mod 5) = 𝑏 ↔ ((𝑦 + 2) mod 5) = ((𝑦 − 2) mod 5)))
40	39	adantl 487	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑦 ∈ (0..^5) ∧ ((𝑦 − 2) mod 5) = 𝑏) → (((𝑦 + 2) mod 5) = 𝑏 ↔ ((𝑦 + 2) mod 5) = ((𝑦 − 2) mod 5)))
41		elfzoelz 13794	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑦 ∈ (0..^5) → 𝑦 ∈ ℤ)
42		2z 12729	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ 2 ∈ ℤ
43	42	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑦 ∈ (0..^5) → 2 ∈ ℤ)
44	41, 43	zaddcld 12808	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑦 ∈ (0..^5) → (𝑦 + 2) ∈ ℤ)
45	41, 43	zsubcld 12809	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑦 ∈ (0..^5) → (𝑦 − 2) ∈ ℤ)
46		5nn 12430	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ 5 ∈ ℕ
47	46	a1i 11	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑦 ∈ (0..^5) → 5 ∈ ℕ)
48		difmod0 16458	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝑦 + 2) ∈ ℤ ∧ (𝑦 − 2) ∈ ℤ ∧ 5 ∈ ℕ) → ((((𝑦 + 2) − (𝑦 − 2)) mod 5) = 0 ↔ ((𝑦 + 2) mod 5) = ((𝑦 − 2) mod 5)))
49	48	bicomd 226	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑦 + 2) ∈ ℤ ∧ (𝑦 − 2) ∈ ℤ ∧ 5 ∈ ℕ) → (((𝑦 + 2) mod 5) = ((𝑦 − 2) mod 5) ↔ (((𝑦 + 2) − (𝑦 − 2)) mod 5) = 0))
50	44, 45, 47, 49	syl3anc 1398	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑦 ∈ (0..^5) → (((𝑦 + 2) mod 5) = ((𝑦 − 2) mod 5) ↔ (((𝑦 + 2) − (𝑦 − 2)) mod 5) = 0))
51	41	zcnd 12805	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑦 ∈ (0..^5) → 𝑦 ∈ ℂ)
52		2cnd 12422	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑦 ∈ (0..^5) → 2 ∈ ℂ)
53	51, 52, 52	pnncand 11709	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑦 ∈ (0..^5) → ((𝑦 + 2) − (𝑦 − 2)) = (2 + 2))
54		2p2e4 12478	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (2 + 2) = 4
55	53, 54	eqtrdi 2812	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑦 ∈ (0..^5) → ((𝑦 + 2) − (𝑦 − 2)) = 4)
56	55	oveq1d 7436	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑦 ∈ (0..^5) → (((𝑦 + 2) − (𝑦 − 2)) mod 5) = (4 mod 5))
57	56	eqeq1d 2763	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑦 ∈ (0..^5) → ((((𝑦 + 2) − (𝑦 − 2)) mod 5) = 0 ↔ (4 mod 5) = 0))
58		4re 12428	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ 4 ∈ ℝ
59		5rp 13128	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ 5 ∈ ℝ⁺
60		0re 11311	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ 0 ∈ ℝ
61		4pos 12454	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ 0 < 4
62	60, 58, 61	ltleii 11434	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ 0 ≤ 4
63		4lt5 12523	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ 4 < 5
64		modid 14037	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((4 ∈ ℝ ∧ 5 ∈ ℝ⁺) ∧ (0 ≤ 4 ∧ 4 < 5)) → (4 mod 5) = 4)
65	58, 59, 62, 63, 64	mp4an 706	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (4 mod 5) = 4
66	65	eqeq1i 2766	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((4 mod 5) = 0 ↔ 4 = 0)
67		4ne0 12455	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ 4 ≠ 0
68	67	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ({⟨0, 𝑏⟩, ⟨1, ((𝑦 + 2) mod 5)⟩} ∈ 𝐸 → 4 ≠ 0)
69	68	necon2bi 2986	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (4 = 0 → ¬ {⟨0, 𝑏⟩, ⟨1, ((𝑦 + 2) mod 5)⟩} ∈ 𝐸)
70	66, 69	sylbi 220	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((4 mod 5) = 0 → ¬ {⟨0, 𝑏⟩, ⟨1, ((𝑦 + 2) mod 5)⟩} ∈ 𝐸)
71	57, 70	biimtrdi 256	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑦 ∈ (0..^5) → ((((𝑦 + 2) − (𝑦 − 2)) mod 5) = 0 → ¬ {⟨0, 𝑏⟩, ⟨1, ((𝑦 + 2) mod 5)⟩} ∈ 𝐸))
72	50, 71	sylbid 243	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑦 ∈ (0..^5) → (((𝑦 + 2) mod 5) = ((𝑦 − 2) mod 5) → ¬ {⟨0, 𝑏⟩, ⟨1, ((𝑦 + 2) mod 5)⟩} ∈ 𝐸))
73	72	adantr 486	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑦 ∈ (0..^5) ∧ ((𝑦 − 2) mod 5) = 𝑏) → (((𝑦 + 2) mod 5) = ((𝑦 − 2) mod 5) → ¬ {⟨0, 𝑏⟩, ⟨1, ((𝑦 + 2) mod 5)⟩} ∈ 𝐸))
74	40, 73	sylbid 243	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑦 ∈ (0..^5) ∧ ((𝑦 − 2) mod 5) = 𝑏) → (((𝑦 + 2) mod 5) = 𝑏 → ¬ {⟨0, 𝑏⟩, ⟨1, ((𝑦 + 2) mod 5)⟩} ∈ 𝐸))
75	74	ex 418	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 ∈ (0..^5) → (((𝑦 − 2) mod 5) = 𝑏 → (((𝑦 + 2) mod 5) = 𝑏 → ¬ {⟨0, 𝑏⟩, ⟨1, ((𝑦 + 2) mod 5)⟩} ∈ 𝐸)))
76	75	adantl 487	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑏 ∈ (0..^5) ∧ 𝑦 ∈ (0..^5)) → (((𝑦 − 2) mod 5) = 𝑏 → (((𝑦 + 2) mod 5) = 𝑏 → ¬ {⟨0, 𝑏⟩, ⟨1, ((𝑦 + 2) mod 5)⟩} ∈ 𝐸)))
77	76	com12 33	. . . . . . . . . . . . . . . 16 ⊢ (((𝑦 − 2) mod 5) = 𝑏 → ((𝑏 ∈ (0..^5) ∧ 𝑦 ∈ (0..^5)) → (((𝑦 + 2) mod 5) = 𝑏 → ¬ {⟨0, 𝑏⟩, ⟨1, ((𝑦 + 2) mod 5)⟩} ∈ 𝐸)))
78	37, 77	sylbi 220	. . . . . . . . . . . . . . 15 ⊢ (((𝑦 − 2) mod 5) = (2^nd ‘⟨0, 𝑏⟩) → ((𝑏 ∈ (0..^5) ∧ 𝑦 ∈ (0..^5)) → (((𝑦 + 2) mod 5) = 𝑏 → ¬ {⟨0, 𝑏⟩, ⟨1, ((𝑦 + 2) mod 5)⟩} ∈ 𝐸)))
79	36, 78	simplbiim 514	. . . . . . . . . . . . . 14 ⊢ (⟨1, ((𝑦 − 2) mod 5)⟩ = ⟨1, (2^nd ‘⟨0, 𝑏⟩)⟩ → ((𝑏 ∈ (0..^5) ∧ 𝑦 ∈ (0..^5)) → (((𝑦 + 2) mod 5) = 𝑏 → ¬ {⟨0, 𝑏⟩, ⟨1, ((𝑦 + 2) mod 5)⟩} ∈ 𝐸)))
80	19, 30	opth 5445	. . . . . . . . . . . . . . 15 ⊢ (⟨1, ((𝑦 − 2) mod 5)⟩ = ⟨0, (((2^nd ‘⟨0, 𝑏⟩) − 1) mod 5)⟩ ↔ (1 = 0 ∧ ((𝑦 − 2) mod 5) = (((2^nd ‘⟨0, 𝑏⟩) − 1) mod 5)))
81	33	adantr 486	. . . . . . . . . . . . . . 15 ⊢ ((1 = 0 ∧ ((𝑦 − 2) mod 5) = (((2^nd ‘⟨0, 𝑏⟩) − 1) mod 5)) → ((𝑏 ∈ (0..^5) ∧ 𝑦 ∈ (0..^5)) → (((𝑦 + 2) mod 5) = 𝑏 → ¬ {⟨0, 𝑏⟩, ⟨1, ((𝑦 + 2) mod 5)⟩} ∈ 𝐸)))
82	80, 81	sylbi 220	. . . . . . . . . . . . . 14 ⊢ (⟨1, ((𝑦 − 2) mod 5)⟩ = ⟨0, (((2^nd ‘⟨0, 𝑏⟩) − 1) mod 5)⟩ → ((𝑏 ∈ (0..^5) ∧ 𝑦 ∈ (0..^5)) → (((𝑦 + 2) mod 5) = 𝑏 → ¬ {⟨0, 𝑏⟩, ⟨1, ((𝑦 + 2) mod 5)⟩} ∈ 𝐸)))
83	35, 79, 82	3jaoi 1454	. . . . . . . . . . . . 13 ⊢ ((⟨1, ((𝑦 − 2) mod 5)⟩ = ⟨0, (((2^nd ‘⟨0, 𝑏⟩) + 1) mod 5)⟩ ∨ ⟨1, ((𝑦 − 2) mod 5)⟩ = ⟨1, (2^nd ‘⟨0, 𝑏⟩)⟩ ∨ ⟨1, ((𝑦 − 2) mod 5)⟩ = ⟨0, (((2^nd ‘⟨0, 𝑏⟩) − 1) mod 5)⟩) → ((𝑏 ∈ (0..^5) ∧ 𝑦 ∈ (0..^5)) → (((𝑦 + 2) mod 5) = 𝑏 → ¬ {⟨0, 𝑏⟩, ⟨1, ((𝑦 + 2) mod 5)⟩} ∈ 𝐸)))
84	83	com13 89	. . . . . . . . . . . 12 ⊢ (((𝑦 + 2) mod 5) = 𝑏 → ((𝑏 ∈ (0..^5) ∧ 𝑦 ∈ (0..^5)) → ((⟨1, ((𝑦 − 2) mod 5)⟩ = ⟨0, (((2^nd ‘⟨0, 𝑏⟩) + 1) mod 5)⟩ ∨ ⟨1, ((𝑦 − 2) mod 5)⟩ = ⟨1, (2^nd ‘⟨0, 𝑏⟩)⟩ ∨ ⟨1, ((𝑦 − 2) mod 5)⟩ = ⟨0, (((2^nd ‘⟨0, 𝑏⟩) − 1) mod 5)⟩) → ¬ {⟨0, 𝑏⟩, ⟨1, ((𝑦 + 2) mod 5)⟩} ∈ 𝐸)))
85	84	impd 416	. . . . . . . . . . 11 ⊢ (((𝑦 + 2) mod 5) = 𝑏 → (((𝑏 ∈ (0..^5) ∧ 𝑦 ∈ (0..^5)) ∧ (⟨1, ((𝑦 − 2) mod 5)⟩ = ⟨0, (((2^nd ‘⟨0, 𝑏⟩) + 1) mod 5)⟩ ∨ ⟨1, ((𝑦 − 2) mod 5)⟩ = ⟨1, (2^nd ‘⟨0, 𝑏⟩)⟩ ∨ ⟨1, ((𝑦 − 2) mod 5)⟩ = ⟨0, (((2^nd ‘⟨0, 𝑏⟩) − 1) mod 5)⟩)) → ¬ {⟨0, 𝑏⟩, ⟨1, ((𝑦 + 2) mod 5)⟩} ∈ 𝐸))
86	29, 85	sylbi 220	. . . . . . . . . 10 ⊢ (((𝑦 + 2) mod 5) = (2^nd ‘⟨0, 𝑏⟩) → (((𝑏 ∈ (0..^5) ∧ 𝑦 ∈ (0..^5)) ∧ (⟨1, ((𝑦 − 2) mod 5)⟩ = ⟨0, (((2^nd ‘⟨0, 𝑏⟩) + 1) mod 5)⟩ ∨ ⟨1, ((𝑦 − 2) mod 5)⟩ = ⟨1, (2^nd ‘⟨0, 𝑏⟩)⟩ ∨ ⟨1, ((𝑦 − 2) mod 5)⟩ = ⟨0, (((2^nd ‘⟨0, 𝑏⟩) − 1) mod 5)⟩)) → ¬ {⟨0, 𝑏⟩, ⟨1, ((𝑦 + 2) mod 5)⟩} ∈ 𝐸))
87	27, 86	simplbiim 514	. . . . . . . . 9 ⊢ (⟨1, ((𝑦 + 2) mod 5)⟩ = ⟨1, (2^nd ‘⟨0, 𝑏⟩)⟩ → (((𝑏 ∈ (0..^5) ∧ 𝑦 ∈ (0..^5)) ∧ (⟨1, ((𝑦 − 2) mod 5)⟩ = ⟨0, (((2^nd ‘⟨0, 𝑏⟩) + 1) mod 5)⟩ ∨ ⟨1, ((𝑦 − 2) mod 5)⟩ = ⟨1, (2^nd ‘⟨0, 𝑏⟩)⟩ ∨ ⟨1, ((𝑦 − 2) mod 5)⟩ = ⟨0, (((2^nd ‘⟨0, 𝑏⟩) − 1) mod 5)⟩)) → ¬ {⟨0, 𝑏⟩, ⟨1, ((𝑦 + 2) mod 5)⟩} ∈ 𝐸))
88	19, 20	opth 5445	. . . . . . . . . 10 ⊢ (⟨1, ((𝑦 + 2) mod 5)⟩ = ⟨0, (((2^nd ‘⟨0, 𝑏⟩) − 1) mod 5)⟩ ↔ (1 = 0 ∧ ((𝑦 + 2) mod 5) = (((2^nd ‘⟨0, 𝑏⟩) − 1) mod 5)))
89	24	adantr 486	. . . . . . . . . 10 ⊢ ((1 = 0 ∧ ((𝑦 + 2) mod 5) = (((2^nd ‘⟨0, 𝑏⟩) − 1) mod 5)) → (((𝑏 ∈ (0..^5) ∧ 𝑦 ∈ (0..^5)) ∧ (⟨1, ((𝑦 − 2) mod 5)⟩ = ⟨0, (((2^nd ‘⟨0, 𝑏⟩) + 1) mod 5)⟩ ∨ ⟨1, ((𝑦 − 2) mod 5)⟩ = ⟨1, (2^nd ‘⟨0, 𝑏⟩)⟩ ∨ ⟨1, ((𝑦 − 2) mod 5)⟩ = ⟨0, (((2^nd ‘⟨0, 𝑏⟩) − 1) mod 5)⟩)) → ¬ {⟨0, 𝑏⟩, ⟨1, ((𝑦 + 2) mod 5)⟩} ∈ 𝐸))
90	88, 89	sylbi 220	. . . . . . . . 9 ⊢ (⟨1, ((𝑦 + 2) mod 5)⟩ = ⟨0, (((2^nd ‘⟨0, 𝑏⟩) − 1) mod 5)⟩ → (((𝑏 ∈ (0..^5) ∧ 𝑦 ∈ (0..^5)) ∧ (⟨1, ((𝑦 − 2) mod 5)⟩ = ⟨0, (((2^nd ‘⟨0, 𝑏⟩) + 1) mod 5)⟩ ∨ ⟨1, ((𝑦 − 2) mod 5)⟩ = ⟨1, (2^nd ‘⟨0, 𝑏⟩)⟩ ∨ ⟨1, ((𝑦 − 2) mod 5)⟩ = ⟨0, (((2^nd ‘⟨0, 𝑏⟩) − 1) mod 5)⟩)) → ¬ {⟨0, 𝑏⟩, ⟨1, ((𝑦 + 2) mod 5)⟩} ∈ 𝐸))
91	26, 87, 90	3jaoi 1454	. . . . . . . 8 ⊢ ((⟨1, ((𝑦 + 2) mod 5)⟩ = ⟨0, (((2^nd ‘⟨0, 𝑏⟩) + 1) mod 5)⟩ ∨ ⟨1, ((𝑦 + 2) mod 5)⟩ = ⟨1, (2^nd ‘⟨0, 𝑏⟩)⟩ ∨ ⟨1, ((𝑦 + 2) mod 5)⟩ = ⟨0, (((2^nd ‘⟨0, 𝑏⟩) − 1) mod 5)⟩) → (((𝑏 ∈ (0..^5) ∧ 𝑦 ∈ (0..^5)) ∧ (⟨1, ((𝑦 − 2) mod 5)⟩ = ⟨0, (((2^nd ‘⟨0, 𝑏⟩) + 1) mod 5)⟩ ∨ ⟨1, ((𝑦 − 2) mod 5)⟩ = ⟨1, (2^nd ‘⟨0, 𝑏⟩)⟩ ∨ ⟨1, ((𝑦 − 2) mod 5)⟩ = ⟨0, (((2^nd ‘⟨0, 𝑏⟩) − 1) mod 5)⟩)) → ¬ {⟨0, 𝑏⟩, ⟨1, ((𝑦 + 2) mod 5)⟩} ∈ 𝐸))
92	18, 91	syl 18	. . . . . . 7 ⊢ ({⟨0, 𝑏⟩, ⟨1, ((𝑦 + 2) mod 5)⟩} ∈ 𝐸 → (((𝑏 ∈ (0..^5) ∧ 𝑦 ∈ (0..^5)) ∧ (⟨1, ((𝑦 − 2) mod 5)⟩ = ⟨0, (((2^nd ‘⟨0, 𝑏⟩) + 1) mod 5)⟩ ∨ ⟨1, ((𝑦 − 2) mod 5)⟩ = ⟨1, (2^nd ‘⟨0, 𝑏⟩)⟩ ∨ ⟨1, ((𝑦 − 2) mod 5)⟩ = ⟨0, (((2^nd ‘⟨0, 𝑏⟩) − 1) mod 5)⟩)) → ¬ {⟨0, 𝑏⟩, ⟨1, ((𝑦 + 2) mod 5)⟩} ∈ 𝐸))
93		ax-1 6	. . . . . . 7 ⊢ (¬ {⟨0, 𝑏⟩, ⟨1, ((𝑦 + 2) mod 5)⟩} ∈ 𝐸 → (((𝑏 ∈ (0..^5) ∧ 𝑦 ∈ (0..^5)) ∧ (⟨1, ((𝑦 − 2) mod 5)⟩ = ⟨0, (((2^nd ‘⟨0, 𝑏⟩) + 1) mod 5)⟩ ∨ ⟨1, ((𝑦 − 2) mod 5)⟩ = ⟨1, (2^nd ‘⟨0, 𝑏⟩)⟩ ∨ ⟨1, ((𝑦 − 2) mod 5)⟩ = ⟨0, (((2^nd ‘⟨0, 𝑏⟩) − 1) mod 5)⟩)) → ¬ {⟨0, 𝑏⟩, ⟨1, ((𝑦 + 2) mod 5)⟩} ∈ 𝐸))
94	92, 93	pm2.61i 184	. . . . . 6 ⊢ (((𝑏 ∈ (0..^5) ∧ 𝑦 ∈ (0..^5)) ∧ (⟨1, ((𝑦 − 2) mod 5)⟩ = ⟨0, (((2^nd ‘⟨0, 𝑏⟩) + 1) mod 5)⟩ ∨ ⟨1, ((𝑦 − 2) mod 5)⟩ = ⟨1, (2^nd ‘⟨0, 𝑏⟩)⟩ ∨ ⟨1, ((𝑦 − 2) mod 5)⟩ = ⟨0, (((2^nd ‘⟨0, 𝑏⟩) − 1) mod 5)⟩)) → ¬ {⟨0, 𝑏⟩, ⟨1, ((𝑦 + 2) mod 5)⟩} ∈ 𝐸)
95	94	ex 418	. . . . 5 ⊢ ((𝑏 ∈ (0..^5) ∧ 𝑦 ∈ (0..^5)) → ((⟨1, ((𝑦 − 2) mod 5)⟩ = ⟨0, (((2^nd ‘⟨0, 𝑏⟩) + 1) mod 5)⟩ ∨ ⟨1, ((𝑦 − 2) mod 5)⟩ = ⟨1, (2^nd ‘⟨0, 𝑏⟩)⟩ ∨ ⟨1, ((𝑦 − 2) mod 5)⟩ = ⟨0, (((2^nd ‘⟨0, 𝑏⟩) − 1) mod 5)⟩) → ¬ {⟨0, 𝑏⟩, ⟨1, ((𝑦 + 2) mod 5)⟩} ∈ 𝐸))
96	16, 95	syld 48	. . . 4 ⊢ ((𝑏 ∈ (0..^5) ∧ 𝑦 ∈ (0..^5)) → ({⟨1, ((𝑦 − 2) mod 5)⟩, ⟨0, 𝑏⟩} ∈ 𝐸 → ¬ {⟨0, 𝑏⟩, ⟨1, ((𝑦 + 2) mod 5)⟩} ∈ 𝐸))
97	96	adantl 487	. . 3 ⊢ (((𝐿 = ⟨1, ((𝑦 + 2) mod 5)⟩ ∧ 𝐾 = ⟨1, ((𝑦 − 2) mod 5)⟩) ∧ (𝑏 ∈ (0..^5) ∧ 𝑦 ∈ (0..^5))) → ({⟨1, ((𝑦 − 2) mod 5)⟩, ⟨0, 𝑏⟩} ∈ 𝐸 → ¬ {⟨0, 𝑏⟩, ⟨1, ((𝑦 + 2) mod 5)⟩} ∈ 𝐸))
98		preq1 4694	. . . . . . 7 ⊢ (𝐾 = ⟨1, ((𝑦 − 2) mod 5)⟩ → {𝐾, ⟨0, 𝑏⟩} = {⟨1, ((𝑦 − 2) mod 5)⟩, ⟨0, 𝑏⟩})
99	98	eleq1d 2846	. . . . . 6 ⊢ (𝐾 = ⟨1, ((𝑦 − 2) mod 5)⟩ → ({𝐾, ⟨0, 𝑏⟩} ∈ 𝐸 ↔ {⟨1, ((𝑦 − 2) mod 5)⟩, ⟨0, 𝑏⟩} ∈ 𝐸))
100	99	adantl 487	. . . . 5 ⊢ ((𝐿 = ⟨1, ((𝑦 + 2) mod 5)⟩ ∧ 𝐾 = ⟨1, ((𝑦 − 2) mod 5)⟩) → ({𝐾, ⟨0, 𝑏⟩} ∈ 𝐸 ↔ {⟨1, ((𝑦 − 2) mod 5)⟩, ⟨0, 𝑏⟩} ∈ 𝐸))
101		preq2 4695	. . . . . . . 8 ⊢ (𝐿 = ⟨1, ((𝑦 + 2) mod 5)⟩ → {⟨0, 𝑏⟩, 𝐿} = {⟨0, 𝑏⟩, ⟨1, ((𝑦 + 2) mod 5)⟩})
102	101	eleq1d 2846	. . . . . . 7 ⊢ (𝐿 = ⟨1, ((𝑦 + 2) mod 5)⟩ → ({⟨0, 𝑏⟩, 𝐿} ∈ 𝐸 ↔ {⟨0, 𝑏⟩, ⟨1, ((𝑦 + 2) mod 5)⟩} ∈ 𝐸))
103	102	notbid 321	. . . . . 6 ⊢ (𝐿 = ⟨1, ((𝑦 + 2) mod 5)⟩ → (¬ {⟨0, 𝑏⟩, 𝐿} ∈ 𝐸 ↔ ¬ {⟨0, 𝑏⟩, ⟨1, ((𝑦 + 2) mod 5)⟩} ∈ 𝐸))
104	103	adantr 486	. . . . 5 ⊢ ((𝐿 = ⟨1, ((𝑦 + 2) mod 5)⟩ ∧ 𝐾 = ⟨1, ((𝑦 − 2) mod 5)⟩) → (¬ {⟨0, 𝑏⟩, 𝐿} ∈ 𝐸 ↔ ¬ {⟨0, 𝑏⟩, ⟨1, ((𝑦 + 2) mod 5)⟩} ∈ 𝐸))
105	100, 104	imbi12d 347	. . . 4 ⊢ ((𝐿 = ⟨1, ((𝑦 + 2) mod 5)⟩ ∧ 𝐾 = ⟨1, ((𝑦 − 2) mod 5)⟩) → (({𝐾, ⟨0, 𝑏⟩} ∈ 𝐸 → ¬ {⟨0, 𝑏⟩, 𝐿} ∈ 𝐸) ↔ ({⟨1, ((𝑦 − 2) mod 5)⟩, ⟨0, 𝑏⟩} ∈ 𝐸 → ¬ {⟨0, 𝑏⟩, ⟨1, ((𝑦 + 2) mod 5)⟩} ∈ 𝐸)))
106	105	adantr 486	. . 3 ⊢ (((𝐿 = ⟨1, ((𝑦 + 2) mod 5)⟩ ∧ 𝐾 = ⟨1, ((𝑦 − 2) mod 5)⟩) ∧ (𝑏 ∈ (0..^5) ∧ 𝑦 ∈ (0..^5))) → (({𝐾, ⟨0, 𝑏⟩} ∈ 𝐸 → ¬ {⟨0, 𝑏⟩, 𝐿} ∈ 𝐸) ↔ ({⟨1, ((𝑦 − 2) mod 5)⟩, ⟨0, 𝑏⟩} ∈ 𝐸 → ¬ {⟨0, 𝑏⟩, ⟨1, ((𝑦 + 2) mod 5)⟩} ∈ 𝐸)))
107	97, 106	mpbird 260	. 2 ⊢ (((𝐿 = ⟨1, ((𝑦 + 2) mod 5)⟩ ∧ 𝐾 = ⟨1, ((𝑦 − 2) mod 5)⟩) ∧ (𝑏 ∈ (0..^5) ∧ 𝑦 ∈ (0..^5))) → ({𝐾, ⟨0, 𝑏⟩} ∈ 𝐸 → ¬ {⟨0, 𝑏⟩, 𝐿} ∈ 𝐸))
108	107	imp 412	1 ⊢ ((((𝐿 = ⟨1, ((𝑦 + 2) mod 5)⟩ ∧ 𝐾 = ⟨1, ((𝑦 − 2) mod 5)⟩) ∧ (𝑏 ∈ (0..^5) ∧ 𝑦 ∈ (0..^5))) ∧ {𝐾, ⟨0, 𝑏⟩} ∈ 𝐸) → ¬ {⟨0, 𝑏⟩, 𝐿} ∈ 𝐸)

Colors of variables: wff setvar class

This proof depends on syntax axioms: ¬ wn 3 → wi 4 ↔ wb 209 ∧ wa 401 ∨ w3o 1102 ∧ w3a 1103 = wceq 1570 ∈ wcel 2145 ≠ wne 2956 {cpr 4586 ⟨cop 4590 class class class wbr 5103 ‘cfv 6539 (class class class)co 7421 1^st c1st 8000 2^nd c2nd 8001 ℝcr 11200 0cc0 11201 1c1 11202 + caddc 11204 < clt 11344 ≤ cle 11345 − cmin 11542 / cdiv 11974 ℕcn 12336 2c2 12398 3c3 12399 4c4 12400 5c5 12401 ℤcz 12694 ℤ_≥cuz 12966 ℝ⁺crp 13121 ..^cfzo 13789 ⌈cceil 13932 mod cmo 14010 Vtxcvtx 29575 Edgcedg 29626 NeighbVtx cnbgr 29914 gPetersenGr cgpg 49139

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 2733 ax-rep 5232 ax-sep 5249 ax-nul 5260 ax-pow 5327 ax-pr 5391 ax-un 7752 ax-cnex 11257 ax-resscn 11258 ax-1cn 11259 ax-icn 11260 ax-addcl 11261 ax-addrcl 11262 ax-mulcl 11263 ax-mulrcl 11264 ax-mulcom 11265 ax-addass 11266 ax-mulass 11267 ax-distr 11268 ax-i2m1 11269 ax-1ne0 11270 ax-1rid 11271 ax-rnegex 11272 ax-rrecex 11273 ax-cnre 11274 ax-pre-lttri 11275 ax-pre-lttrn 11276 ax-pre-ltadd 11277 ax-pre-mulgt0 11278 ax-pre-sup 11279

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 2565 df-eu 2595 df-clab 2740 df-cleq 2753 df-clel 2836 df-nfc 2910 df-ne 2957 df-nel 3063 df-ral 3078 df-rex 3088 df-rmo 3366 df-reu 3367 df-rab 3414 df-v 3453 df-sbc 3740 df-csb 3848 df-dif 3900 df-un 3902 df-in 3904 df-ss 3915 df-pss 4035 df-nul 4280 df-if 4483 df-pw 4559 df-sn 4585 df-pr 4587 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 5546 df-eprel 5551 df-po 5559 df-so 5560 df-fr 5604 df-we 5606 df-xp 5657 df-rel 5658 df-cnv 5659 df-co 5660 df-dm 5661 df-rn 5662 df-res 5663 df-ima 5664 df-pred 6305 df-ord 6366 df-on 6367 df-lim 6368 df-suc 6369 df-iota 6495 df-fun 6541 df-fn 6542 df-f 6543 df-f1 6544 df-fo 6545 df-f1o 6546 df-fv 6547 df-riota 7378 df-ov 7424 df-oprab 7425 df-mpo 7426 df-om 7879 df-1st 8002 df-2nd 8003 df-frecs 8300 df-wrecs 8331 df-recs 8380 df-rdg 8419 df-1o 8477 df-oadd 8481 df-er 8718 df-en 8975 df-dom 8976 df-sdom 8977 df-fin 8978 df-sup 9435 df-inf 9436 df-dju 9983 df-card 10021 df-pnf 11346 df-mnf 11347 df-xr 11348 df-ltxr 11349 df-le 11350 df-sub 11544 df-neg 11545 df-div 11975 df-nn 12337 df-2 12406 df-3 12407 df-4 12408 df-5 12409 df-6 12410 df-7 12411 df-8 12412 df-9 12413 df-n0 12608 df-xnn0 12681 df-z 12695 df-dec 12816 df-uz 12967 df-rp 13122 df-fz 13641 df-fzo 13790 df-fl 13933 df-ceil 13934 df-mod 14011 df-hash 14476 df-dvds 16424 df-struct 17326 df-slot 17361 df-ndx 17373 df-base 17389 df-edgf 29568 df-vtx 29577 df-iedg 29578 df-edg 29627 df-umgr 29662 df-usgr 29733 df-gpg 49140

This theorem is used by: pgnbgreunbgrlem2 49216

W3C validator