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 48604

Description: Lemma 3 for pgnbgreunbgrlem2 48605. (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 4677	. . . . . . . 8 ⊢ {⟨1, ((𝑦 − 2) mod 5)⟩, ⟨0, 𝑏⟩} = {⟨0, 𝑏⟩, ⟨1, ((𝑦 − 2) mod 5)⟩}
2	1	eleq1i 2828	. . . . . . 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 12824	. . . . . . . 8 ⊢ 5 ∈ (ℤ_≥‘3)
5		pglem 48579	. . . . . . . 8 ⊢ 2 ∈ (1..^(⌈‘(5 / 2)))
6	4, 5	pm3.2i 470	. . . . . . 7 ⊢ (5 ∈ (ℤ_≥‘3) ∧ 2 ∈ (1..^(⌈‘(5 / 2))))
7		c0ex 11129	. . . . . . . 8 ⊢ 0 ∈ V
8		vex 3434	. . . . . . . 8 ⊢ 𝑏 ∈ V
9	7, 8	op1st 7943	. . . . . . 7 ⊢ (1^st ‘⟨0, 𝑏⟩) = 0
10		eqid 2737	. . . . . . . 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 48551	. . . . . . 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 1454	. . . . . 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 253	. . . . 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 48551	. . . . . . . . 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 1454	. . . . . . . 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 11131	. . . . . . . . . . 11 ⊢ 1 ∈ V
20		ovex 7393	. . . . . . . . . . 11 ⊢ ((𝑦 + 2) mod 5) ∈ V
21	19, 20	opth 5424	. . . . . . . . . 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 11098	. . . . . . . . . . . 12 ⊢ 1 ≠ 0
23		eqneqall 2944	. . . . . . . . . . . 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 480	. . . . . . . . . 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 217	. . . . . . . . 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 5424	. . . . . . . . . 10 ⊢ (⟨1, ((𝑦 + 2) mod 5)⟩ = ⟨1, (2^nd ‘⟨0, 𝑏⟩)⟩ ↔ (1 = 1 ∧ ((𝑦 + 2) mod 5) = (2^nd ‘⟨0, 𝑏⟩)))
28	7, 8	op2nd 7944	. . . . . . . . . . . 12 ⊢ (2^nd ‘⟨0, 𝑏⟩) = 𝑏
29	28	eqeq2i 2750	. . . . . . . . . . 11 ⊢ (((𝑦 + 2) mod 5) = (2^nd ‘⟨0, 𝑏⟩) ↔ ((𝑦 + 2) mod 5) = 𝑏)
30		ovex 7393	. . . . . . . . . . . . . . . 16 ⊢ ((𝑦 − 2) mod 5) ∈ V
31	19, 30	opth 5424	. . . . . . . . . . . . . . 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 2944	. . . . . . . . . . . . . . . . 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 480	. . . . . . . . . . . . . . 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 217	. . . . . . . . . . . . . 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 5424	. . . . . . . . . . . . . . 15 ⊢ (⟨1, ((𝑦 − 2) mod 5)⟩ = ⟨1, (2^nd ‘⟨0, 𝑏⟩)⟩ ↔ (1 = 1 ∧ ((𝑦 − 2) mod 5) = (2^nd ‘⟨0, 𝑏⟩)))
37	28	eqeq2i 2750	. . . . . . . . . . . . . . . 16 ⊢ (((𝑦 − 2) mod 5) = (2^nd ‘⟨0, 𝑏⟩) ↔ ((𝑦 − 2) mod 5) = 𝑏)
38		eqeq2 2749	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑏 = ((𝑦 − 2) mod 5) → (((𝑦 + 2) mod 5) = 𝑏 ↔ ((𝑦 + 2) mod 5) = ((𝑦 − 2) mod 5)))
39	38	eqcoms 2745	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑦 − 2) mod 5) = 𝑏 → (((𝑦 + 2) mod 5) = 𝑏 ↔ ((𝑦 + 2) mod 5) = ((𝑦 − 2) mod 5)))
40	39	adantl 481	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑦 ∈ (0..^5) ∧ ((𝑦 − 2) mod 5) = 𝑏) → (((𝑦 + 2) mod 5) = 𝑏 ↔ ((𝑦 + 2) mod 5) = ((𝑦 − 2) mod 5)))
41		elfzoelz 13604	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑦 ∈ (0..^5) → 𝑦 ∈ ℤ)
42		2z 12550	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ 2 ∈ ℤ
43	42	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑦 ∈ (0..^5) → 2 ∈ ℤ)
44	41, 43	zaddcld 12628	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑦 ∈ (0..^5) → (𝑦 + 2) ∈ ℤ)
45	41, 43	zsubcld 12629	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑦 ∈ (0..^5) → (𝑦 − 2) ∈ ℤ)
46		5nn 12258	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ 5 ∈ ℕ
47	46	a1i 11	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑦 ∈ (0..^5) → 5 ∈ ℕ)
48		difmod0 16247	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝑦 + 2) ∈ ℤ ∧ (𝑦 − 2) ∈ ℤ ∧ 5 ∈ ℕ) → ((((𝑦 + 2) − (𝑦 − 2)) mod 5) = 0 ↔ ((𝑦 + 2) mod 5) = ((𝑦 − 2) mod 5)))
49	48	bicomd 223	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑦 + 2) ∈ ℤ ∧ (𝑦 − 2) ∈ ℤ ∧ 5 ∈ ℕ) → (((𝑦 + 2) mod 5) = ((𝑦 − 2) mod 5) ↔ (((𝑦 + 2) − (𝑦 − 2)) mod 5) = 0))
50	44, 45, 47, 49	syl3anc 1374	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑦 ∈ (0..^5) → (((𝑦 + 2) mod 5) = ((𝑦 − 2) mod 5) ↔ (((𝑦 + 2) − (𝑦 − 2)) mod 5) = 0))
51	41	zcnd 12625	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑦 ∈ (0..^5) → 𝑦 ∈ ℂ)
52		2cnd 12250	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑦 ∈ (0..^5) → 2 ∈ ℂ)
53	51, 52, 52	pnncand 11535	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑦 ∈ (0..^5) → ((𝑦 + 2) − (𝑦 − 2)) = (2 + 2))
54		2p2e4 12302	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (2 + 2) = 4
55	53, 54	eqtrdi 2788	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑦 ∈ (0..^5) → ((𝑦 + 2) − (𝑦 − 2)) = 4)
56	55	oveq1d 7375	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑦 ∈ (0..^5) → (((𝑦 + 2) − (𝑦 − 2)) mod 5) = (4 mod 5))
57	56	eqeq1d 2739	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑦 ∈ (0..^5) → ((((𝑦 + 2) − (𝑦 − 2)) mod 5) = 0 ↔ (4 mod 5) = 0))
58		4re 12256	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ 4 ∈ ℝ
59		5rp 12940	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ 5 ∈ ℝ⁺
60		0re 11137	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ 0 ∈ ℝ
61		4pos 12279	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ 0 < 4
62	60, 58, 61	ltleii 11260	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ 0 ≤ 4
63		4lt5 12344	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ 4 < 5
64		modid 13846	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((4 ∈ ℝ ∧ 5 ∈ ℝ⁺) ∧ (0 ≤ 4 ∧ 4 < 5)) → (4 mod 5) = 4)
65	58, 59, 62, 63, 64	mp4an 694	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (4 mod 5) = 4
66	65	eqeq1i 2742	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((4 mod 5) = 0 ↔ 4 = 0)
67		4ne0 12280	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ 4 ≠ 0
68	67	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ({⟨0, 𝑏⟩, ⟨1, ((𝑦 + 2) mod 5)⟩} ∈ 𝐸 → 4 ≠ 0)
69	68	necon2bi 2963	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (4 = 0 → ¬ {⟨0, 𝑏⟩, ⟨1, ((𝑦 + 2) mod 5)⟩} ∈ 𝐸)
70	66, 69	sylbi 217	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((4 mod 5) = 0 → ¬ {⟨0, 𝑏⟩, ⟨1, ((𝑦 + 2) mod 5)⟩} ∈ 𝐸)
71	57, 70	biimtrdi 253	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑦 ∈ (0..^5) → ((((𝑦 + 2) − (𝑦 − 2)) mod 5) = 0 → ¬ {⟨0, 𝑏⟩, ⟨1, ((𝑦 + 2) mod 5)⟩} ∈ 𝐸))
72	50, 71	sylbid 240	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑦 ∈ (0..^5) → (((𝑦 + 2) mod 5) = ((𝑦 − 2) mod 5) → ¬ {⟨0, 𝑏⟩, ⟨1, ((𝑦 + 2) mod 5)⟩} ∈ 𝐸))
73	72	adantr 480	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑦 ∈ (0..^5) ∧ ((𝑦 − 2) mod 5) = 𝑏) → (((𝑦 + 2) mod 5) = ((𝑦 − 2) mod 5) → ¬ {⟨0, 𝑏⟩, ⟨1, ((𝑦 + 2) mod 5)⟩} ∈ 𝐸))
74	40, 73	sylbid 240	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑦 ∈ (0..^5) ∧ ((𝑦 − 2) mod 5) = 𝑏) → (((𝑦 + 2) mod 5) = 𝑏 → ¬ {⟨0, 𝑏⟩, ⟨1, ((𝑦 + 2) mod 5)⟩} ∈ 𝐸))
75	74	ex 412	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 ∈ (0..^5) → (((𝑦 − 2) mod 5) = 𝑏 → (((𝑦 + 2) mod 5) = 𝑏 → ¬ {⟨0, 𝑏⟩, ⟨1, ((𝑦 + 2) mod 5)⟩} ∈ 𝐸)))
76	75	adantl 481	. . . . . . . . . . . . . . . . 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 217	. . . . . . . . . . . . . . 15 ⊢ (((𝑦 − 2) mod 5) = (2^nd ‘⟨0, 𝑏⟩) → ((𝑏 ∈ (0..^5) ∧ 𝑦 ∈ (0..^5)) → (((𝑦 + 2) mod 5) = 𝑏 → ¬ {⟨0, 𝑏⟩, ⟨1, ((𝑦 + 2) mod 5)⟩} ∈ 𝐸)))
79	36, 78	simplbiim 504	. . . . . . . . . . . . . 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 5424	. . . . . . . . . . . . . . 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 480	. . . . . . . . . . . . . . 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 217	. . . . . . . . . . . . . 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 1431	. . . . . . . . . . . . 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 410	. . . . . . . . . . 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 217	. . . . . . . . . 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 504	. . . . . . . . 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 5424	. . . . . . . . . 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 480	. . . . . . . . . 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 217	. . . . . . . . 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 1431	. . . . . . . 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 182	. . . . . 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 412	. . . . 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 481	. . 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 4678	. . . . . . 7 ⊢ (𝐾 = ⟨1, ((𝑦 − 2) mod 5)⟩ → {𝐾, ⟨0, 𝑏⟩} = {⟨1, ((𝑦 − 2) mod 5)⟩, ⟨0, 𝑏⟩})
99	98	eleq1d 2822	. . . . . 6 ⊢ (𝐾 = ⟨1, ((𝑦 − 2) mod 5)⟩ → ({𝐾, ⟨0, 𝑏⟩} ∈ 𝐸 ↔ {⟨1, ((𝑦 − 2) mod 5)⟩, ⟨0, 𝑏⟩} ∈ 𝐸))
100	99	adantl 481	. . . . 5 ⊢ ((𝐿 = ⟨1, ((𝑦 + 2) mod 5)⟩ ∧ 𝐾 = ⟨1, ((𝑦 − 2) mod 5)⟩) → ({𝐾, ⟨0, 𝑏⟩} ∈ 𝐸 ↔ {⟨1, ((𝑦 − 2) mod 5)⟩, ⟨0, 𝑏⟩} ∈ 𝐸))
101		preq2 4679	. . . . . . . 8 ⊢ (𝐿 = ⟨1, ((𝑦 + 2) mod 5)⟩ → {⟨0, 𝑏⟩, 𝐿} = {⟨0, 𝑏⟩, ⟨1, ((𝑦 + 2) mod 5)⟩})
102	101	eleq1d 2822	. . . . . . 7 ⊢ (𝐿 = ⟨1, ((𝑦 + 2) mod 5)⟩ → ({⟨0, 𝑏⟩, 𝐿} ∈ 𝐸 ↔ {⟨0, 𝑏⟩, ⟨1, ((𝑦 + 2) mod 5)⟩} ∈ 𝐸))
103	102	notbid 318	. . . . . 6 ⊢ (𝐿 = ⟨1, ((𝑦 + 2) mod 5)⟩ → (¬ {⟨0, 𝑏⟩, 𝐿} ∈ 𝐸 ↔ ¬ {⟨0, 𝑏⟩, ⟨1, ((𝑦 + 2) mod 5)⟩} ∈ 𝐸))
104	103	adantr 480	. . . . 5 ⊢ ((𝐿 = ⟨1, ((𝑦 + 2) mod 5)⟩ ∧ 𝐾 = ⟨1, ((𝑦 − 2) mod 5)⟩) → (¬ {⟨0, 𝑏⟩, 𝐿} ∈ 𝐸 ↔ ¬ {⟨0, 𝑏⟩, ⟨1, ((𝑦 + 2) mod 5)⟩} ∈ 𝐸))
105	100, 104	imbi12d 344	. . . 4 ⊢ ((𝐿 = ⟨1, ((𝑦 + 2) mod 5)⟩ ∧ 𝐾 = ⟨1, ((𝑦 − 2) mod 5)⟩) → (({𝐾, ⟨0, 𝑏⟩} ∈ 𝐸 → ¬ {⟨0, 𝑏⟩, 𝐿} ∈ 𝐸) ↔ ({⟨1, ((𝑦 − 2) mod 5)⟩, ⟨0, 𝑏⟩} ∈ 𝐸 → ¬ {⟨0, 𝑏⟩, ⟨1, ((𝑦 + 2) mod 5)⟩} ∈ 𝐸)))
106	105	adantr 480	. . 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 257	. 2 ⊢ (((𝐿 = ⟨1, ((𝑦 + 2) mod 5)⟩ ∧ 𝐾 = ⟨1, ((𝑦 − 2) mod 5)⟩) ∧ (𝑏 ∈ (0..^5) ∧ 𝑦 ∈ (0..^5))) → ({𝐾, ⟨0, 𝑏⟩} ∈ 𝐸 → ¬ {⟨0, 𝑏⟩, 𝐿} ∈ 𝐸))
108	107	imp 406	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 206 ∧ wa 395 ∨ w3o 1086 ∧ w3a 1087 = wceq 1542 ∈ wcel 2114 ≠ wne 2933 {cpr 4570 ⟨cop 4574 class class class wbr 5086 ‘cfv 6492 (class class class)co 7360 1^st c1st 7933 2^nd c2nd 7934 ℝcr 11028 0cc0 11029 1c1 11030 + caddc 11032 < clt 11170 ≤ cle 11171 − cmin 11368 / cdiv 11798 ℕcn 12165 2c2 12227 3c3 12228 4c4 12229 5c5 12230 ℤcz 12515 ℤ_≥cuz 12779 ℝ⁺crp 12933 ..^cfzo 13599 ⌈cceil 13741 mod cmo 13819 Vtxcvtx 29079 Edgcedg 29130 NeighbVtx cnbgr 29415 gPetersenGr cgpg 48528

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1912 ax-6 1969 ax-7 2010 ax-8 2116 ax-9 2124 ax-10 2147 ax-11 2163 ax-12 2185 ax-ext 2709 ax-rep 5212 ax-sep 5231 ax-nul 5241 ax-pow 5302 ax-pr 5370 ax-un 7682 ax-cnex 11085 ax-resscn 11086 ax-1cn 11087 ax-icn 11088 ax-addcl 11089 ax-addrcl 11090 ax-mulcl 11091 ax-mulrcl 11092 ax-mulcom 11093 ax-addass 11094 ax-mulass 11095 ax-distr 11096 ax-i2m1 11097 ax-1ne0 11098 ax-1rid 11099 ax-rnegex 11100 ax-rrecex 11101 ax-cnre 11102 ax-pre-lttri 11103 ax-pre-lttrn 11104 ax-pre-ltadd 11105 ax-pre-mulgt0 11106 ax-pre-sup 11107

This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3or 1088 df-3an 1089 df-tru 1545 df-fal 1555 df-ex 1782 df-nf 1786 df-sb 2069 df-mo 2540 df-eu 2570 df-clab 2716 df-cleq 2729 df-clel 2812 df-nfc 2886 df-ne 2934 df-nel 3038 df-ral 3053 df-rex 3063 df-rmo 3343 df-reu 3344 df-rab 3391 df-v 3432 df-sbc 3730 df-csb 3839 df-dif 3893 df-un 3895 df-in 3897 df-ss 3907 df-pss 3910 df-nul 4275 df-if 4468 df-pw 4544 df-sn 4569 df-pr 4571 df-op 4575 df-uni 4852 df-int 4891 df-iun 4936 df-br 5087 df-opab 5149 df-mpt 5168 df-tr 5194 df-id 5519 df-eprel 5524 df-po 5532 df-so 5533 df-fr 5577 df-we 5579 df-xp 5630 df-rel 5631 df-cnv 5632 df-co 5633 df-dm 5634 df-rn 5635 df-res 5636 df-ima 5637 df-pred 6259 df-ord 6320 df-on 6321 df-lim 6322 df-suc 6323 df-iota 6448 df-fun 6494 df-fn 6495 df-f 6496 df-f1 6497 df-fo 6498 df-f1o 6499 df-fv 6500 df-riota 7317 df-ov 7363 df-oprab 7364 df-mpo 7365 df-om 7811 df-1st 7935 df-2nd 7936 df-frecs 8224 df-wrecs 8255 df-recs 8304 df-rdg 8342 df-1o 8398 df-oadd 8402 df-er 8636 df-en 8887 df-dom 8888 df-sdom 8889 df-fin 8890 df-sup 9348 df-inf 9349 df-dju 9816 df-card 9854 df-pnf 11172 df-mnf 11173 df-xr 11174 df-ltxr 11175 df-le 11176 df-sub 11370 df-neg 11371 df-div 11799 df-nn 12166 df-2 12235 df-3 12236 df-4 12237 df-5 12238 df-6 12239 df-7 12240 df-8 12241 df-9 12242 df-n0 12429 df-xnn0 12502 df-z 12516 df-dec 12636 df-uz 12780 df-rp 12934 df-fz 13453 df-fzo 13600 df-fl 13742 df-ceil 13743 df-mod 13820 df-hash 14284 df-dvds 16213 df-struct 17108 df-slot 17143 df-ndx 17155 df-base 17171 df-edgf 29072 df-vtx 29081 df-iedg 29082 df-edg 29131 df-umgr 29166 df-usgr 29234 df-gpg 48529

This theorem is referenced by: pgnbgreunbgrlem2 48605

W3C validator