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 48120

Description: Lemma 3 for pgnbgreunbgrlem2 48121. (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 4686	. . . . . . . 8 ⊢ {⟨1, ((𝑦 − 2) mod 5)⟩, ⟨0, 𝑏⟩} = {⟨0, 𝑏⟩, ⟨1, ((𝑦 − 2) mod 5)⟩}
2	1	eleq1i 2819	. . . . . . 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 12803	. . . . . . . 8 ⊢ 5 ∈ (ℤ_≥‘3)
5		pglem 48095	. . . . . . . 8 ⊢ 2 ∈ (1..^(⌈‘(5 / 2)))
6	4, 5	pm3.2i 470	. . . . . . 7 ⊢ (5 ∈ (ℤ_≥‘3) ∧ 2 ∈ (1..^(⌈‘(5 / 2))))
7		c0ex 11128	. . . . . . . 8 ⊢ 0 ∈ V
8		vex 3442	. . . . . . . 8 ⊢ 𝑏 ∈ V
9	7, 8	op1st 7939	. . . . . . 7 ⊢ (1^st ‘⟨0, 𝑏⟩) = 0
10		eqid 2729	. . . . . . . 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 48067	. . . . . . 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 1453	. . . . . 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 48067	. . . . . . . . 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 1453	. . . . . . . 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 11130	. . . . . . . . . . 11 ⊢ 1 ∈ V
20		ovex 7386	. . . . . . . . . . 11 ⊢ ((𝑦 + 2) mod 5) ∈ V
21	19, 20	opth 5423	. . . . . . . . . 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 11097	. . . . . . . . . . . 12 ⊢ 1 ≠ 0
23		eqneqall 2936	. . . . . . . . . . . 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 5423	. . . . . . . . . 10 ⊢ (⟨1, ((𝑦 + 2) mod 5)⟩ = ⟨1, (2^nd ‘⟨0, 𝑏⟩)⟩ ↔ (1 = 1 ∧ ((𝑦 + 2) mod 5) = (2^nd ‘⟨0, 𝑏⟩)))
28	7, 8	op2nd 7940	. . . . . . . . . . . 12 ⊢ (2^nd ‘⟨0, 𝑏⟩) = 𝑏
29	28	eqeq2i 2742	. . . . . . . . . . 11 ⊢ (((𝑦 + 2) mod 5) = (2^nd ‘⟨0, 𝑏⟩) ↔ ((𝑦 + 2) mod 5) = 𝑏)
30		ovex 7386	. . . . . . . . . . . . . . . 16 ⊢ ((𝑦 − 2) mod 5) ∈ V
31	19, 30	opth 5423	. . . . . . . . . . . . . . 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 2936	. . . . . . . . . . . . . . . . 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 5423	. . . . . . . . . . . . . . 15 ⊢ (⟨1, ((𝑦 − 2) mod 5)⟩ = ⟨1, (2^nd ‘⟨0, 𝑏⟩)⟩ ↔ (1 = 1 ∧ ((𝑦 − 2) mod 5) = (2^nd ‘⟨0, 𝑏⟩)))
37	28	eqeq2i 2742	. . . . . . . . . . . . . . . 16 ⊢ (((𝑦 − 2) mod 5) = (2^nd ‘⟨0, 𝑏⟩) ↔ ((𝑦 − 2) mod 5) = 𝑏)
38		eqeq2 2741	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑏 = ((𝑦 − 2) mod 5) → (((𝑦 + 2) mod 5) = 𝑏 ↔ ((𝑦 + 2) mod 5) = ((𝑦 − 2) mod 5)))
39	38	eqcoms 2737	. . . . . . . . . . . . . . . . . . . . 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 13581	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑦 ∈ (0..^5) → 𝑦 ∈ ℤ)
42		2z 12526	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ 2 ∈ ℤ
43	42	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑦 ∈ (0..^5) → 2 ∈ ℤ)
44	41, 43	zaddcld 12603	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑦 ∈ (0..^5) → (𝑦 + 2) ∈ ℤ)
45	41, 43	zsubcld 12604	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑦 ∈ (0..^5) → (𝑦 − 2) ∈ ℤ)
46		5nn 12233	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ 5 ∈ ℕ
47	46	a1i 11	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑦 ∈ (0..^5) → 5 ∈ ℕ)
48		difmod0 16217	. . . . . . . . . . . . . . . . . . . . . . . 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 1373	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑦 ∈ (0..^5) → (((𝑦 + 2) mod 5) = ((𝑦 − 2) mod 5) ↔ (((𝑦 + 2) − (𝑦 − 2)) mod 5) = 0))
51	41	zcnd 12600	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑦 ∈ (0..^5) → 𝑦 ∈ ℂ)
52		2cnd 12225	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑦 ∈ (0..^5) → 2 ∈ ℂ)
53	51, 52, 52	pnncand 11533	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑦 ∈ (0..^5) → ((𝑦 + 2) − (𝑦 − 2)) = (2 + 2))
54		2p2e4 12277	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (2 + 2) = 4
55	53, 54	eqtrdi 2780	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑦 ∈ (0..^5) → ((𝑦 + 2) − (𝑦 − 2)) = 4)
56	55	oveq1d 7368	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑦 ∈ (0..^5) → (((𝑦 + 2) − (𝑦 − 2)) mod 5) = (4 mod 5))
57	56	eqeq1d 2731	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑦 ∈ (0..^5) → ((((𝑦 + 2) − (𝑦 − 2)) mod 5) = 0 ↔ (4 mod 5) = 0))
58		4re 12231	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ 4 ∈ ℝ
59		5rp 12919	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ 5 ∈ ℝ⁺
60		0re 11136	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ 0 ∈ ℝ
61		4pos 12254	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ 0 < 4
62	60, 58, 61	ltleii 11258	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ 0 ≤ 4
63		4lt5 12319	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ 4 < 5
64		modid 13819	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((4 ∈ ℝ ∧ 5 ∈ ℝ⁺) ∧ (0 ≤ 4 ∧ 4 < 5)) → (4 mod 5) = 4)
65	58, 59, 62, 63, 64	mp4an 693	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (4 mod 5) = 4
66	65	eqeq1i 2734	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((4 mod 5) = 0 ↔ 4 = 0)
67		4ne0 12255	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ 4 ≠ 0
68	67	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ({⟨0, 𝑏⟩, ⟨1, ((𝑦 + 2) mod 5)⟩} ∈ 𝐸 → 4 ≠ 0)
69	68	necon2bi 2955	. . . . . . . . . . . . . . . . . . . . . . . 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 5423	. . . . . . . . . . . . . . 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 1430	. . . . . . . . . . . . 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 5423	. . . . . . . . . 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 1430	. . . . . . . 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 4687	. . . . . . 7 ⊢ (𝐾 = ⟨1, ((𝑦 − 2) mod 5)⟩ → {𝐾, ⟨0, 𝑏⟩} = {⟨1, ((𝑦 − 2) mod 5)⟩, ⟨0, 𝑏⟩})
99	98	eleq1d 2813	. . . . . 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 4688	. . . . . . . 8 ⊢ (𝐿 = ⟨1, ((𝑦 + 2) mod 5)⟩ → {⟨0, 𝑏⟩, 𝐿} = {⟨0, 𝑏⟩, ⟨1, ((𝑦 + 2) mod 5)⟩})
102	101	eleq1d 2813	. . . . . . 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 1085 ∧ w3a 1086 = wceq 1540 ∈ wcel 2109 ≠ wne 2925 {cpr 4581 ⟨cop 4585 class class class wbr 5095 ‘cfv 6486 (class class class)co 7353 1^st c1st 7929 2^nd c2nd 7930 ℝcr 11027 0cc0 11028 1c1 11029 + caddc 11031 < clt 11168 ≤ cle 11169 − cmin 11366 / cdiv 11796 ℕcn 12147 2c2 12202 3c3 12203 4c4 12204 5c5 12205 ℤcz 12490 ℤ_≥cuz 12754 ℝ⁺crp 12912 ..^cfzo 13576 ⌈cceil 13714 mod cmo 13792 Vtxcvtx 28960 Edgcedg 29011 NeighbVtx cnbgr 29296 gPetersenGr cgpg 48044

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 5221 ax-sep 5238 ax-nul 5248 ax-pow 5307 ax-pr 5374 ax-un 7675 ax-cnex 11084 ax-resscn 11085 ax-1cn 11086 ax-icn 11087 ax-addcl 11088 ax-addrcl 11089 ax-mulcl 11090 ax-mulrcl 11091 ax-mulcom 11092 ax-addass 11093 ax-mulass 11094 ax-distr 11095 ax-i2m1 11096 ax-1ne0 11097 ax-1rid 11098 ax-rnegex 11099 ax-rrecex 11100 ax-cnre 11101 ax-pre-lttri 11102 ax-pre-lttrn 11103 ax-pre-ltadd 11104 ax-pre-mulgt0 11105 ax-pre-sup 11106

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-rmo 3345 df-reu 3346 df-rab 3397 df-v 3440 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 4479 df-pw 4555 df-sn 4580 df-pr 4582 df-op 4586 df-uni 4862 df-int 4900 df-iun 4946 df-br 5096 df-opab 5158 df-mpt 5177 df-tr 5203 df-id 5518 df-eprel 5523 df-po 5531 df-so 5532 df-fr 5576 df-we 5578 df-xp 5629 df-rel 5630 df-cnv 5631 df-co 5632 df-dm 5633 df-rn 5634 df-res 5635 df-ima 5636 df-pred 6253 df-ord 6314 df-on 6315 df-lim 6316 df-suc 6317 df-iota 6442 df-fun 6488 df-fn 6489 df-f 6490 df-f1 6491 df-fo 6492 df-f1o 6493 df-fv 6494 df-riota 7310 df-ov 7356 df-oprab 7357 df-mpo 7358 df-om 7807 df-1st 7931 df-2nd 7932 df-frecs 8221 df-wrecs 8252 df-recs 8301 df-rdg 8339 df-1o 8395 df-oadd 8399 df-er 8632 df-en 8880 df-dom 8881 df-sdom 8882 df-fin 8883 df-sup 9351 df-inf 9352 df-dju 9816 df-card 9854 df-pnf 11170 df-mnf 11171 df-xr 11172 df-ltxr 11173 df-le 11174 df-sub 11368 df-neg 11369 df-div 11797 df-nn 12148 df-2 12210 df-3 12211 df-4 12212 df-5 12213 df-6 12214 df-7 12215 df-8 12216 df-9 12217 df-n0 12404 df-xnn0 12477 df-z 12491 df-dec 12611 df-uz 12755 df-rp 12913 df-fz 13430 df-fzo 13577 df-fl 13715 df-ceil 13716 df-mod 13793 df-hash 14257 df-dvds 16183 df-struct 17077 df-slot 17112 df-ndx 17124 df-base 17140 df-edgf 28953 df-vtx 28962 df-iedg 28963 df-edg 29012 df-umgr 29047 df-usgr 29115 df-gpg 48045

This theorem is referenced by: pgnbgreunbgrlem2 48121

W3C validator