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 48699

Description: Lemma 3 for pgnbgreunbgrlem2 48700. (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 4688	. . . . . . . 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 12878	. . . . . . . 8 ⊢ 5 ∈ (ℤ_≥‘3)
5		pglem 48674	. . . . . . . 8 ⊢ 2 ∈ (1..^(⌈‘(5 / 2)))
6	4, 5	pm3.2i 474	. . . . . . 7 ⊢ (5 ∈ (ℤ_≥‘3) ∧ 2 ∈ (1..^(⌈‘(5 / 2))))
7		c0ex 11167	. . . . . . . 8 ⊢ 0 ∈ V
8		vex 3457	. . . . . . . 8 ⊢ 𝑏 ∈ V
9	7, 8	op1st 7973	. . . . . . 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 48646	. . . . . . 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 1471	. . . . . 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 255	. . . . 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 48646	. . . . . . . . 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 1471	. . . . . . . 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 11170	. . . . . . . . . . 11 ⊢ 1 ∈ V
20		ovex 7424	. . . . . . . . . . 11 ⊢ ((𝑦 + 2) mod 5) ∈ V
21	19, 20	opth 5441	. . . . . . . . . 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 11136	. . . . . . . . . . . 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 20	. . . . . . . . . . 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 484	. . . . . . . . . 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 219	. . . . . . . . 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 5441	. . . . . . . . . 10 ⊢ (⟨1, ((𝑦 + 2) mod 5)⟩ = ⟨1, (2^nd ‘⟨0, 𝑏⟩)⟩ ↔ (1 = 1 ∧ ((𝑦 + 2) mod 5) = (2^nd ‘⟨0, 𝑏⟩)))
28	7, 8	op2nd 7974	. . . . . . . . . . . 12 ⊢ (2^nd ‘⟨0, 𝑏⟩) = 𝑏
29	28	eqeq2i 2774	. . . . . . . . . . 11 ⊢ (((𝑦 + 2) mod 5) = (2^nd ‘⟨0, 𝑏⟩) ↔ ((𝑦 + 2) mod 5) = 𝑏)
30		ovex 7424	. . . . . . . . . . . . . . . 16 ⊢ ((𝑦 − 2) mod 5) ∈ V
31	19, 30	opth 5441	. . . . . . . . . . . . . . 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 20	. . . . . . . . . . . . . . . 16 ⊢ (1 = 0 → ((𝑏 ∈ (0..^5) ∧ 𝑦 ∈ (0..^5)) → (((𝑦 + 2) mod 5) = 𝑏 → ¬ {⟨0, 𝑏⟩, ⟨1, ((𝑦 + 2) mod 5)⟩} ∈ 𝐸)))
34	33	adantr 484	. . . . . . . . . . . . . . 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 219	. . . . . . . . . . . . . 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 5441	. . . . . . . . . . . . . . 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 485	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑦 ∈ (0..^5) ∧ ((𝑦 − 2) mod 5) = 𝑏) → (((𝑦 + 2) mod 5) = 𝑏 ↔ ((𝑦 + 2) mod 5) = ((𝑦 − 2) mod 5)))
41		elfzoelz 13658	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑦 ∈ (0..^5) → 𝑦 ∈ ℤ)
42		2z 12597	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ 2 ∈ ℤ
43	42	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑦 ∈ (0..^5) → 2 ∈ ℤ)
44	41, 43	zaddcld 12675	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑦 ∈ (0..^5) → (𝑦 + 2) ∈ ℤ)
45	41, 43	zsubcld 12676	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑦 ∈ (0..^5) → (𝑦 − 2) ∈ ℤ)
46		5nn 12298	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ 5 ∈ ℕ
47	46	a1i 11	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑦 ∈ (0..^5) → 5 ∈ ℕ)
48		difmod0 16312	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝑦 + 2) ∈ ℤ ∧ (𝑦 − 2) ∈ ℤ ∧ 5 ∈ ℕ) → ((((𝑦 + 2) − (𝑦 − 2)) mod 5) = 0 ↔ ((𝑦 + 2) mod 5) = ((𝑦 − 2) mod 5)))
49	48	bicomd 225	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑦 + 2) ∈ ℤ ∧ (𝑦 − 2) ∈ ℤ ∧ 5 ∈ ℕ) → (((𝑦 + 2) mod 5) = ((𝑦 − 2) mod 5) ↔ (((𝑦 + 2) − (𝑦 − 2)) mod 5) = 0))
50	44, 45, 47, 49	syl3anc 1389	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑦 ∈ (0..^5) → (((𝑦 + 2) mod 5) = ((𝑦 − 2) mod 5) ↔ (((𝑦 + 2) − (𝑦 − 2)) mod 5) = 0))
51	41	zcnd 12672	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑦 ∈ (0..^5) → 𝑦 ∈ ℂ)
52		2cnd 12290	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑦 ∈ (0..^5) → 2 ∈ ℂ)
53	51, 52, 52	pnncand 11575	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑦 ∈ (0..^5) → ((𝑦 + 2) − (𝑦 − 2)) = (2 + 2))
54		2p2e4 12346	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (2 + 2) = 4
55	53, 54	eqtrdi 2812	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑦 ∈ (0..^5) → ((𝑦 + 2) − (𝑦 − 2)) = 4)
56	55	oveq1d 7406	. . . . . . . . . . . . . . . . . . . . . . . 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 12296	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ 4 ∈ ℝ
59		5rp 12994	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ 5 ∈ ℝ⁺
60		0re 11177	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ 0 ∈ ℝ
61		4pos 12322	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ 0 < 4
62	60, 58, 61	ltleii 11300	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ 0 ≤ 4
63		4lt5 12391	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ 4 < 5
64		modid 13900	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((4 ∈ ℝ ∧ 5 ∈ ℝ⁺) ∧ (0 ≤ 4 ∧ 4 < 5)) → (4 mod 5) = 4)
65	58, 59, 62, 63, 64	mp4an 703	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (4 mod 5) = 4
66	65	eqeq1i 2766	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((4 mod 5) = 0 ↔ 4 = 0)
67		4ne0 12323	. . . . . . . . . . . . . . . . . . . . . . . . . 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 219	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((4 mod 5) = 0 → ¬ {⟨0, 𝑏⟩, ⟨1, ((𝑦 + 2) mod 5)⟩} ∈ 𝐸)
71	57, 70	biimtrdi 255	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑦 ∈ (0..^5) → ((((𝑦 + 2) − (𝑦 − 2)) mod 5) = 0 → ¬ {⟨0, 𝑏⟩, ⟨1, ((𝑦 + 2) mod 5)⟩} ∈ 𝐸))
72	50, 71	sylbid 242	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑦 ∈ (0..^5) → (((𝑦 + 2) mod 5) = ((𝑦 − 2) mod 5) → ¬ {⟨0, 𝑏⟩, ⟨1, ((𝑦 + 2) mod 5)⟩} ∈ 𝐸))
73	72	adantr 484	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑦 ∈ (0..^5) ∧ ((𝑦 − 2) mod 5) = 𝑏) → (((𝑦 + 2) mod 5) = ((𝑦 − 2) mod 5) → ¬ {⟨0, 𝑏⟩, ⟨1, ((𝑦 + 2) mod 5)⟩} ∈ 𝐸))
74	40, 73	sylbid 242	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑦 ∈ (0..^5) ∧ ((𝑦 − 2) mod 5) = 𝑏) → (((𝑦 + 2) mod 5) = 𝑏 → ¬ {⟨0, 𝑏⟩, ⟨1, ((𝑦 + 2) mod 5)⟩} ∈ 𝐸))
75	74	ex 416	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 ∈ (0..^5) → (((𝑦 − 2) mod 5) = 𝑏 → (((𝑦 + 2) mod 5) = 𝑏 → ¬ {⟨0, 𝑏⟩, ⟨1, ((𝑦 + 2) mod 5)⟩} ∈ 𝐸)))
76	75	adantl 485	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑏 ∈ (0..^5) ∧ 𝑦 ∈ (0..^5)) → (((𝑦 − 2) mod 5) = 𝑏 → (((𝑦 + 2) mod 5) = 𝑏 → ¬ {⟨0, 𝑏⟩, ⟨1, ((𝑦 + 2) mod 5)⟩} ∈ 𝐸)))
77	76	com12 32	. . . . . . . . . . . . . . . 16 ⊢ (((𝑦 − 2) mod 5) = 𝑏 → ((𝑏 ∈ (0..^5) ∧ 𝑦 ∈ (0..^5)) → (((𝑦 + 2) mod 5) = 𝑏 → ¬ {⟨0, 𝑏⟩, ⟨1, ((𝑦 + 2) mod 5)⟩} ∈ 𝐸)))
78	37, 77	sylbi 219	. . . . . . . . . . . . . . 15 ⊢ (((𝑦 − 2) mod 5) = (2^nd ‘⟨0, 𝑏⟩) → ((𝑏 ∈ (0..^5) ∧ 𝑦 ∈ (0..^5)) → (((𝑦 + 2) mod 5) = 𝑏 → ¬ {⟨0, 𝑏⟩, ⟨1, ((𝑦 + 2) mod 5)⟩} ∈ 𝐸)))
79	36, 78	simplbiim 512	. . . . . . . . . . . . . 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 5441	. . . . . . . . . . . . . . 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 484	. . . . . . . . . . . . . . 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 219	. . . . . . . . . . . . . 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 1446	. . . . . . . . . . . . 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 88	. . . . . . . . . . . 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 414	. . . . . . . . . . 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 219	. . . . . . . . . 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 512	. . . . . . . . 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 5441	. . . . . . . . . 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 484	. . . . . . . . . 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 219	. . . . . . . . 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 1446	. . . . . . . 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 17	. . . . . . 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 183	. . . . . 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 416	. . . . 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 47	. . . 4 ⊢ ((𝑏 ∈ (0..^5) ∧ 𝑦 ∈ (0..^5)) → ({⟨1, ((𝑦 − 2) mod 5)⟩, ⟨0, 𝑏⟩} ∈ 𝐸 → ¬ {⟨0, 𝑏⟩, ⟨1, ((𝑦 + 2) mod 5)⟩} ∈ 𝐸))
97	96	adantl 485	. . 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 4689	. . . . . . 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 485	. . . . 5 ⊢ ((𝐿 = ⟨1, ((𝑦 + 2) mod 5)⟩ ∧ 𝐾 = ⟨1, ((𝑦 − 2) mod 5)⟩) → ({𝐾, ⟨0, 𝑏⟩} ∈ 𝐸 ↔ {⟨1, ((𝑦 − 2) mod 5)⟩, ⟨0, 𝑏⟩} ∈ 𝐸))
101		preq2 4690	. . . . . . . 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 320	. . . . . 6 ⊢ (𝐿 = ⟨1, ((𝑦 + 2) mod 5)⟩ → (¬ {⟨0, 𝑏⟩, 𝐿} ∈ 𝐸 ↔ ¬ {⟨0, 𝑏⟩, ⟨1, ((𝑦 + 2) mod 5)⟩} ∈ 𝐸))
104	103	adantr 484	. . . . 5 ⊢ ((𝐿 = ⟨1, ((𝑦 + 2) mod 5)⟩ ∧ 𝐾 = ⟨1, ((𝑦 − 2) mod 5)⟩) → (¬ {⟨0, 𝑏⟩, 𝐿} ∈ 𝐸 ↔ ¬ {⟨0, 𝑏⟩, ⟨1, ((𝑦 + 2) mod 5)⟩} ∈ 𝐸))
105	100, 104	imbi12d 346	. . . 4 ⊢ ((𝐿 = ⟨1, ((𝑦 + 2) mod 5)⟩ ∧ 𝐾 = ⟨1, ((𝑦 − 2) mod 5)⟩) → (({𝐾, ⟨0, 𝑏⟩} ∈ 𝐸 → ¬ {⟨0, 𝑏⟩, 𝐿} ∈ 𝐸) ↔ ({⟨1, ((𝑦 − 2) mod 5)⟩, ⟨0, 𝑏⟩} ∈ 𝐸 → ¬ {⟨0, 𝑏⟩, ⟨1, ((𝑦 + 2) mod 5)⟩} ∈ 𝐸)))
106	105	adantr 484	. . 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 259	. 2 ⊢ (((𝐿 = ⟨1, ((𝑦 + 2) mod 5)⟩ ∧ 𝐾 = ⟨1, ((𝑦 − 2) mod 5)⟩) ∧ (𝑏 ∈ (0..^5) ∧ 𝑦 ∈ (0..^5))) → ({𝐾, ⟨0, 𝑏⟩} ∈ 𝐸 → ¬ {⟨0, 𝑏⟩, 𝐿} ∈ 𝐸))
108	107	imp 410	1 ⊢ ((((𝐿 = ⟨1, ((𝑦 + 2) mod 5)⟩ ∧ 𝐾 = ⟨1, ((𝑦 − 2) mod 5)⟩) ∧ (𝑏 ∈ (0..^5) ∧ 𝑦 ∈ (0..^5))) ∧ {𝐾, ⟨0, 𝑏⟩} ∈ 𝐸) → ¬ {⟨0, 𝑏⟩, 𝐿} ∈ 𝐸)

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 208 ∧ wa 399 ∨ w3o 1096 ∧ w3a 1097 = wceq 1559 ∈ wcel 2141 ≠ wne 2956 {cpr 4581 ⟨cop 4585 class class class wbr 5097 ‘cfv 6516 (class class class)co 7391 1^st c1st 7963 2^nd c2nd 7964 ℝcr 11066 0cc0 11067 1c1 11068 + caddc 11070 < clt 11210 ≤ cle 11211 − cmin 11408 / cdiv 11838 ℕcn 12204 2c2 12266 3c3 12267 4c4 12268 5c5 12269 ℤcz 12562 ℤ_≥cuz 12833 ℝ⁺crp 12987 ..^cfzo 13653 ⌈cceil 13795 mod cmo 13873 Vtxcvtx 29154 Edgcedg 29205 NeighbVtx cnbgr 29490 gPetersenGr cgpg 48623

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1814 ax-4 1828 ax-5 1929 ax-6 1986 ax-7 2027 ax-8 2143 ax-9 2151 ax-10 2174 ax-11 2190 ax-12 2211 ax-ext 2733 ax-rep 5224 ax-sep 5243 ax-nul 5253 ax-pow 5319 ax-pr 5387 ax-un 7713 ax-cnex 11123 ax-resscn 11124 ax-1cn 11125 ax-icn 11126 ax-addcl 11127 ax-addrcl 11128 ax-mulcl 11129 ax-mulrcl 11130 ax-mulcom 11131 ax-addass 11132 ax-mulass 11133 ax-distr 11134 ax-i2m1 11135 ax-1ne0 11136 ax-1rid 11137 ax-rnegex 11138 ax-rrecex 11139 ax-cnre 11140 ax-pre-lttri 11141 ax-pre-lttrn 11142 ax-pre-ltadd 11143 ax-pre-mulgt0 11144 ax-pre-sup 11145

This theorem depends on definitions: df-bi 209 df-an 400 df-or 859 df-3or 1098 df-3an 1099 df-tru 1562 df-fal 1572 df-ex 1799 df-nf 1803 df-sb 2090 df-mo 2565 df-eu 2595 df-clab 2740 df-cleq 2753 df-clel 2836 df-nfc 2910 df-ne 2957 df-nel 3061 df-ral 3076 df-rex 3086 df-rmo 3366 df-reu 3367 df-rab 3414 df-v 3455 df-sbc 3743 df-csb 3851 df-dif 3905 df-un 3907 df-in 3909 df-ss 3919 df-pss 3922 df-nul 4284 df-if 4478 df-pw 4554 df-sn 4580 df-pr 4582 df-op 4586 df-uni 4863 df-int 4903 df-iun 4948 df-br 5098 df-opab 5160 df-mpt 5179 df-tr 5205 df-id 5538 df-eprel 5543 df-po 5551 df-so 5552 df-fr 5596 df-we 5598 df-xp 5649 df-rel 5650 df-cnv 5651 df-co 5652 df-dm 5653 df-rn 5654 df-res 5655 df-ima 5656 df-pred 6283 df-ord 6344 df-on 6345 df-lim 6346 df-suc 6347 df-iota 6472 df-fun 6518 df-fn 6519 df-f 6520 df-f1 6521 df-fo 6522 df-f1o 6523 df-fv 6524 df-riota 7348 df-ov 7394 df-oprab 7395 df-mpo 7396 df-om 7842 df-1st 7965 df-2nd 7966 df-frecs 8256 df-wrecs 8287 df-recs 8336 df-rdg 8375 df-1o 8431 df-oadd 8435 df-er 8672 df-en 8922 df-dom 8923 df-sdom 8924 df-fin 8925 df-sup 9382 df-inf 9383 df-dju 9853 df-card 9891 df-pnf 11212 df-mnf 11213 df-xr 11214 df-ltxr 11215 df-le 11216 df-sub 11410 df-neg 11411 df-div 11839 df-nn 12205 df-2 12274 df-3 12275 df-4 12276 df-5 12277 df-6 12278 df-7 12279 df-8 12280 df-9 12281 df-n0 12476 df-xnn0 12549 df-z 12563 df-dec 12683 df-uz 12834 df-rp 12988 df-fz 13507 df-fzo 13654 df-fl 13796 df-ceil 13797 df-mod 13874 df-hash 14338 df-dvds 16278 df-struct 17174 df-slot 17209 df-ndx 17221 df-base 17237 df-edgf 29147 df-vtx 29156 df-iedg 29157 df-edg 29206 df-umgr 29241 df-usgr 29309 df-gpg 48624

This theorem is referenced by: pgnbgreunbgrlem2 48700

W3C validator