pgnbgreunbgrlem5 - Mathbox for Alexander van der Vekens

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

Theorem pgnbgreunbgrlem5 48772

Description: Lemma 5 for pgnbgreunbgr 48774. Impossible cases. (Contributed by AV, 21-Nov-2025.)

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

**Assertion**
Ref	Expression
pgnbgreunbgrlem5	⊢ ((𝐿 = ⟨0, (((2^nd ‘𝑋) + 1) mod 5)⟩ ∨ 𝐿 = ⟨1, (2^nd ‘𝑋)⟩ ∨ 𝐿 = ⟨0, (((2^nd ‘𝑋) − 1) mod 5)⟩) → ((𝐾 = ⟨0, (((2^nd ‘𝑋) + 1) mod 5)⟩ ∨ 𝐾 = ⟨1, (2^nd ‘𝑋)⟩ ∨ 𝐾 = ⟨0, (((2^nd ‘𝑋) − 1) mod 5)⟩) → ((𝑋 = ⟨0, 𝑦⟩ ∧ 𝑋 ∈ 𝑉) → ((𝐾 ≠ 𝐿 ∧ (𝑏 ∈ (0..^5) ∧ 𝑦 ∈ (0..^5))) → (({𝐾, ⟨1, 𝑏⟩} ∈ 𝐸 ∧ {⟨1, 𝑏⟩, 𝐿} ∈ 𝐸) → 𝑋 = ⟨1, 𝑏⟩)))))

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

**Proof of Theorem pgnbgreunbgrlem5**
Step	Hyp	Ref	Expression
1		c0ex 11196	. . . . . 6 ⊢ 0 ∈ V
2		vex 3467	. . . . . 6 ⊢ 𝑦 ∈ V
3	1, 2	op2ndd 7993	. . . . 5 ⊢ (𝑋 = ⟨0, 𝑦⟩ → (2^nd ‘𝑋) = 𝑦)
4	3	adantr 485	. . . 4 ⊢ ((𝑋 = ⟨0, 𝑦⟩ ∧ 𝑋 ∈ 𝑉) → (2^nd ‘𝑋) = 𝑦)
5		oveq1 7415	. . . . . . . . 9 ⊢ ((2^nd ‘𝑋) = 𝑦 → ((2^nd ‘𝑋) + 1) = (𝑦 + 1))
6	5	oveq1d 7423	. . . . . . . 8 ⊢ ((2^nd ‘𝑋) = 𝑦 → (((2^nd ‘𝑋) + 1) mod 5) = ((𝑦 + 1) mod 5))
7	6	opeq2d 4846	. . . . . . 7 ⊢ ((2^nd ‘𝑋) = 𝑦 → ⟨0, (((2^nd ‘𝑋) + 1) mod 5)⟩ = ⟨0, ((𝑦 + 1) mod 5)⟩)
8	7	eqeq2d 2780	. . . . . 6 ⊢ ((2^nd ‘𝑋) = 𝑦 → (𝐿 = ⟨0, (((2^nd ‘𝑋) + 1) mod 5)⟩ ↔ 𝐿 = ⟨0, ((𝑦 + 1) mod 5)⟩))
9		opeq2 4840	. . . . . . 7 ⊢ ((2^nd ‘𝑋) = 𝑦 → ⟨1, (2^nd ‘𝑋)⟩ = ⟨1, 𝑦⟩)
10	9	eqeq2d 2780	. . . . . 6 ⊢ ((2^nd ‘𝑋) = 𝑦 → (𝐿 = ⟨1, (2^nd ‘𝑋)⟩ ↔ 𝐿 = ⟨1, 𝑦⟩))
11		oveq1 7415	. . . . . . . . 9 ⊢ ((2^nd ‘𝑋) = 𝑦 → ((2^nd ‘𝑋) − 1) = (𝑦 − 1))
12	11	oveq1d 7423	. . . . . . . 8 ⊢ ((2^nd ‘𝑋) = 𝑦 → (((2^nd ‘𝑋) − 1) mod 5) = ((𝑦 − 1) mod 5))
13	12	opeq2d 4846	. . . . . . 7 ⊢ ((2^nd ‘𝑋) = 𝑦 → ⟨0, (((2^nd ‘𝑋) − 1) mod 5)⟩ = ⟨0, ((𝑦 − 1) mod 5)⟩)
14	13	eqeq2d 2780	. . . . . 6 ⊢ ((2^nd ‘𝑋) = 𝑦 → (𝐿 = ⟨0, (((2^nd ‘𝑋) − 1) mod 5)⟩ ↔ 𝐿 = ⟨0, ((𝑦 − 1) mod 5)⟩))
15	8, 10, 14	3orbi123d 1461	. . . . 5 ⊢ ((2^nd ‘𝑋) = 𝑦 → ((𝐿 = ⟨0, (((2^nd ‘𝑋) + 1) mod 5)⟩ ∨ 𝐿 = ⟨1, (2^nd ‘𝑋)⟩ ∨ 𝐿 = ⟨0, (((2^nd ‘𝑋) − 1) mod 5)⟩) ↔ (𝐿 = ⟨0, ((𝑦 + 1) mod 5)⟩ ∨ 𝐿 = ⟨1, 𝑦⟩ ∨ 𝐿 = ⟨0, ((𝑦 − 1) mod 5)⟩)))
16	7	eqeq2d 2780	. . . . . 6 ⊢ ((2^nd ‘𝑋) = 𝑦 → (𝐾 = ⟨0, (((2^nd ‘𝑋) + 1) mod 5)⟩ ↔ 𝐾 = ⟨0, ((𝑦 + 1) mod 5)⟩))
17	9	eqeq2d 2780	. . . . . 6 ⊢ ((2^nd ‘𝑋) = 𝑦 → (𝐾 = ⟨1, (2^nd ‘𝑋)⟩ ↔ 𝐾 = ⟨1, 𝑦⟩))
18	13	eqeq2d 2780	. . . . . 6 ⊢ ((2^nd ‘𝑋) = 𝑦 → (𝐾 = ⟨0, (((2^nd ‘𝑋) − 1) mod 5)⟩ ↔ 𝐾 = ⟨0, ((𝑦 − 1) mod 5)⟩))
19	16, 17, 18	3orbi123d 1461	. . . . 5 ⊢ ((2^nd ‘𝑋) = 𝑦 → ((𝐾 = ⟨0, (((2^nd ‘𝑋) + 1) mod 5)⟩ ∨ 𝐾 = ⟨1, (2^nd ‘𝑋)⟩ ∨ 𝐾 = ⟨0, (((2^nd ‘𝑋) − 1) mod 5)⟩) ↔ (𝐾 = ⟨0, ((𝑦 + 1) mod 5)⟩ ∨ 𝐾 = ⟨1, 𝑦⟩ ∨ 𝐾 = ⟨0, ((𝑦 − 1) mod 5)⟩)))
20	15, 19	anbi12d 643	. . . 4 ⊢ ((2^nd ‘𝑋) = 𝑦 → (((𝐿 = ⟨0, (((2^nd ‘𝑋) + 1) mod 5)⟩ ∨ 𝐿 = ⟨1, (2^nd ‘𝑋)⟩ ∨ 𝐿 = ⟨0, (((2^nd ‘𝑋) − 1) mod 5)⟩) ∧ (𝐾 = ⟨0, (((2^nd ‘𝑋) + 1) mod 5)⟩ ∨ 𝐾 = ⟨1, (2^nd ‘𝑋)⟩ ∨ 𝐾 = ⟨0, (((2^nd ‘𝑋) − 1) mod 5)⟩)) ↔ ((𝐿 = ⟨0, ((𝑦 + 1) mod 5)⟩ ∨ 𝐿 = ⟨1, 𝑦⟩ ∨ 𝐿 = ⟨0, ((𝑦 − 1) mod 5)⟩) ∧ (𝐾 = ⟨0, ((𝑦 + 1) mod 5)⟩ ∨ 𝐾 = ⟨1, 𝑦⟩ ∨ 𝐾 = ⟨0, ((𝑦 − 1) mod 5)⟩))))
21	4, 20	syl 18	. . 3 ⊢ ((𝑋 = ⟨0, 𝑦⟩ ∧ 𝑋 ∈ 𝑉) → (((𝐿 = ⟨0, (((2^nd ‘𝑋) + 1) mod 5)⟩ ∨ 𝐿 = ⟨1, (2^nd ‘𝑋)⟩ ∨ 𝐿 = ⟨0, (((2^nd ‘𝑋) − 1) mod 5)⟩) ∧ (𝐾 = ⟨0, (((2^nd ‘𝑋) + 1) mod 5)⟩ ∨ 𝐾 = ⟨1, (2^nd ‘𝑋)⟩ ∨ 𝐾 = ⟨0, (((2^nd ‘𝑋) − 1) mod 5)⟩)) ↔ ((𝐿 = ⟨0, ((𝑦 + 1) mod 5)⟩ ∨ 𝐿 = ⟨1, 𝑦⟩ ∨ 𝐿 = ⟨0, ((𝑦 − 1) mod 5)⟩) ∧ (𝐾 = ⟨0, ((𝑦 + 1) mod 5)⟩ ∨ 𝐾 = ⟨1, 𝑦⟩ ∨ 𝐾 = ⟨0, ((𝑦 − 1) mod 5)⟩))))
22		simpl 487	. . . . . . . . . . 11 ⊢ ((𝐾 = ⟨0, ((𝑦 + 1) mod 5)⟩ ∧ 𝐿 = ⟨0, ((𝑦 + 1) mod 5)⟩) → 𝐾 = ⟨0, ((𝑦 + 1) mod 5)⟩)
23		simpr 489	. . . . . . . . . . 11 ⊢ ((𝐾 = ⟨0, ((𝑦 + 1) mod 5)⟩ ∧ 𝐿 = ⟨0, ((𝑦 + 1) mod 5)⟩) → 𝐿 = ⟨0, ((𝑦 + 1) mod 5)⟩)
24	22, 23	neeq12d 3025	. . . . . . . . . 10 ⊢ ((𝐾 = ⟨0, ((𝑦 + 1) mod 5)⟩ ∧ 𝐿 = ⟨0, ((𝑦 + 1) mod 5)⟩) → (𝐾 ≠ 𝐿 ↔ ⟨0, ((𝑦 + 1) mod 5)⟩ ≠ ⟨0, ((𝑦 + 1) mod 5)⟩))
25	24	ancoms 463	. . . . . . . . 9 ⊢ ((𝐿 = ⟨0, ((𝑦 + 1) mod 5)⟩ ∧ 𝐾 = ⟨0, ((𝑦 + 1) mod 5)⟩) → (𝐾 ≠ 𝐿 ↔ ⟨0, ((𝑦 + 1) mod 5)⟩ ≠ ⟨0, ((𝑦 + 1) mod 5)⟩))
26		eqid 2769	. . . . . . . . . 10 ⊢ ⟨0, ((𝑦 + 1) mod 5)⟩ = ⟨0, ((𝑦 + 1) mod 5)⟩
27		eqneqall 2975	. . . . . . . . . 10 ⊢ (⟨0, ((𝑦 + 1) mod 5)⟩ = ⟨0, ((𝑦 + 1) mod 5)⟩ → (⟨0, ((𝑦 + 1) mod 5)⟩ ≠ ⟨0, ((𝑦 + 1) mod 5)⟩ → ((𝑏 ∈ (0..^5) ∧ 𝑦 ∈ (0..^5)) → (({𝐾, ⟨1, 𝑏⟩} ∈ 𝐸 ∧ {⟨1, 𝑏⟩, 𝐿} ∈ 𝐸) → 𝑋 = ⟨1, 𝑏⟩))))
28	26, 27	ax-mp 5	. . . . . . . . 9 ⊢ (⟨0, ((𝑦 + 1) mod 5)⟩ ≠ ⟨0, ((𝑦 + 1) mod 5)⟩ → ((𝑏 ∈ (0..^5) ∧ 𝑦 ∈ (0..^5)) → (({𝐾, ⟨1, 𝑏⟩} ∈ 𝐸 ∧ {⟨1, 𝑏⟩, 𝐿} ∈ 𝐸) → 𝑋 = ⟨1, 𝑏⟩)))
29	25, 28	biimtrdi 256	. . . . . . . 8 ⊢ ((𝐿 = ⟨0, ((𝑦 + 1) mod 5)⟩ ∧ 𝐾 = ⟨0, ((𝑦 + 1) mod 5)⟩) → (𝐾 ≠ 𝐿 → ((𝑏 ∈ (0..^5) ∧ 𝑦 ∈ (0..^5)) → (({𝐾, ⟨1, 𝑏⟩} ∈ 𝐸 ∧ {⟨1, 𝑏⟩, 𝐿} ∈ 𝐸) → 𝑋 = ⟨1, 𝑏⟩))))
30	29	impd 415	. . . . . . 7 ⊢ ((𝐿 = ⟨0, ((𝑦 + 1) mod 5)⟩ ∧ 𝐾 = ⟨0, ((𝑦 + 1) mod 5)⟩) → ((𝐾 ≠ 𝐿 ∧ (𝑏 ∈ (0..^5) ∧ 𝑦 ∈ (0..^5))) → (({𝐾, ⟨1, 𝑏⟩} ∈ 𝐸 ∧ {⟨1, 𝑏⟩, 𝐿} ∈ 𝐸) → 𝑋 = ⟨1, 𝑏⟩)))
31	30	ex 417	. . . . . 6 ⊢ (𝐿 = ⟨0, ((𝑦 + 1) mod 5)⟩ → (𝐾 = ⟨0, ((𝑦 + 1) mod 5)⟩ → ((𝐾 ≠ 𝐿 ∧ (𝑏 ∈ (0..^5) ∧ 𝑦 ∈ (0..^5))) → (({𝐾, ⟨1, 𝑏⟩} ∈ 𝐸 ∧ {⟨1, 𝑏⟩, 𝐿} ∈ 𝐸) → 𝑋 = ⟨1, 𝑏⟩))))
32		pgnbgreunbgr.g	. . . . . . . . . . . 12 ⊢ 𝐺 = (5 gPetersenGr 2)
33		pgnbgreunbgr.v	. . . . . . . . . . . 12 ⊢ 𝑉 = (Vtx‘𝐺)
34		pgnbgreunbgr.e	. . . . . . . . . . . 12 ⊢ 𝐸 = (Edg‘𝐺)
35		pgnbgreunbgr.n	. . . . . . . . . . . 12 ⊢ 𝑁 = (𝐺 NeighbVtx 𝑋)
36	32, 33, 34, 35	pgnbgreunbgrlem5lem1 48769	. . . . . . . . . . 11 ⊢ ((((𝐿 = ⟨0, ((𝑦 + 1) mod 5)⟩ ∧ 𝐾 = ⟨1, 𝑦⟩) ∧ (𝑏 ∈ (0..^5) ∧ 𝑦 ∈ (0..^5))) ∧ {𝐾, ⟨1, 𝑏⟩} ∈ 𝐸) → ¬ {⟨1, 𝑏⟩, 𝐿} ∈ 𝐸)
37	36	pm2.21d 122	. . . . . . . . . 10 ⊢ ((((𝐿 = ⟨0, ((𝑦 + 1) mod 5)⟩ ∧ 𝐾 = ⟨1, 𝑦⟩) ∧ (𝑏 ∈ (0..^5) ∧ 𝑦 ∈ (0..^5))) ∧ {𝐾, ⟨1, 𝑏⟩} ∈ 𝐸) → ({⟨1, 𝑏⟩, 𝐿} ∈ 𝐸 → 𝑋 = ⟨1, 𝑏⟩))
38	37	expimpd 458	. . . . . . . . 9 ⊢ (((𝐿 = ⟨0, ((𝑦 + 1) mod 5)⟩ ∧ 𝐾 = ⟨1, 𝑦⟩) ∧ (𝑏 ∈ (0..^5) ∧ 𝑦 ∈ (0..^5))) → (({𝐾, ⟨1, 𝑏⟩} ∈ 𝐸 ∧ {⟨1, 𝑏⟩, 𝐿} ∈ 𝐸) → 𝑋 = ⟨1, 𝑏⟩))
39	38	ex 417	. . . . . . . 8 ⊢ ((𝐿 = ⟨0, ((𝑦 + 1) mod 5)⟩ ∧ 𝐾 = ⟨1, 𝑦⟩) → ((𝑏 ∈ (0..^5) ∧ 𝑦 ∈ (0..^5)) → (({𝐾, ⟨1, 𝑏⟩} ∈ 𝐸 ∧ {⟨1, 𝑏⟩, 𝐿} ∈ 𝐸) → 𝑋 = ⟨1, 𝑏⟩)))
40	39	adantld 495	. . . . . . 7 ⊢ ((𝐿 = ⟨0, ((𝑦 + 1) mod 5)⟩ ∧ 𝐾 = ⟨1, 𝑦⟩) → ((𝐾 ≠ 𝐿 ∧ (𝑏 ∈ (0..^5) ∧ 𝑦 ∈ (0..^5))) → (({𝐾, ⟨1, 𝑏⟩} ∈ 𝐸 ∧ {⟨1, 𝑏⟩, 𝐿} ∈ 𝐸) → 𝑋 = ⟨1, 𝑏⟩)))
41	40	ex 417	. . . . . 6 ⊢ (𝐿 = ⟨0, ((𝑦 + 1) mod 5)⟩ → (𝐾 = ⟨1, 𝑦⟩ → ((𝐾 ≠ 𝐿 ∧ (𝑏 ∈ (0..^5) ∧ 𝑦 ∈ (0..^5))) → (({𝐾, ⟨1, 𝑏⟩} ∈ 𝐸 ∧ {⟨1, 𝑏⟩, 𝐿} ∈ 𝐸) → 𝑋 = ⟨1, 𝑏⟩))))
42	32, 33, 34, 35	pgnbgreunbgrlem5lem3 48771	. . . . . . . . . . 11 ⊢ ((((𝐿 = ⟨0, ((𝑦 + 1) mod 5)⟩ ∧ 𝐾 = ⟨0, ((𝑦 − 1) mod 5)⟩) ∧ (𝑏 ∈ (0..^5) ∧ 𝑦 ∈ (0..^5))) ∧ {𝐾, ⟨1, 𝑏⟩} ∈ 𝐸) → ¬ {⟨1, 𝑏⟩, 𝐿} ∈ 𝐸)
43	42	pm2.21d 122	. . . . . . . . . 10 ⊢ ((((𝐿 = ⟨0, ((𝑦 + 1) mod 5)⟩ ∧ 𝐾 = ⟨0, ((𝑦 − 1) mod 5)⟩) ∧ (𝑏 ∈ (0..^5) ∧ 𝑦 ∈ (0..^5))) ∧ {𝐾, ⟨1, 𝑏⟩} ∈ 𝐸) → ({⟨1, 𝑏⟩, 𝐿} ∈ 𝐸 → 𝑋 = ⟨1, 𝑏⟩))
44	43	expimpd 458	. . . . . . . . 9 ⊢ (((𝐿 = ⟨0, ((𝑦 + 1) mod 5)⟩ ∧ 𝐾 = ⟨0, ((𝑦 − 1) mod 5)⟩) ∧ (𝑏 ∈ (0..^5) ∧ 𝑦 ∈ (0..^5))) → (({𝐾, ⟨1, 𝑏⟩} ∈ 𝐸 ∧ {⟨1, 𝑏⟩, 𝐿} ∈ 𝐸) → 𝑋 = ⟨1, 𝑏⟩))
45	44	ex 417	. . . . . . . 8 ⊢ ((𝐿 = ⟨0, ((𝑦 + 1) mod 5)⟩ ∧ 𝐾 = ⟨0, ((𝑦 − 1) mod 5)⟩) → ((𝑏 ∈ (0..^5) ∧ 𝑦 ∈ (0..^5)) → (({𝐾, ⟨1, 𝑏⟩} ∈ 𝐸 ∧ {⟨1, 𝑏⟩, 𝐿} ∈ 𝐸) → 𝑋 = ⟨1, 𝑏⟩)))
46	45	adantld 495	. . . . . . 7 ⊢ ((𝐿 = ⟨0, ((𝑦 + 1) mod 5)⟩ ∧ 𝐾 = ⟨0, ((𝑦 − 1) mod 5)⟩) → ((𝐾 ≠ 𝐿 ∧ (𝑏 ∈ (0..^5) ∧ 𝑦 ∈ (0..^5))) → (({𝐾, ⟨1, 𝑏⟩} ∈ 𝐸 ∧ {⟨1, 𝑏⟩, 𝐿} ∈ 𝐸) → 𝑋 = ⟨1, 𝑏⟩)))
47	46	ex 417	. . . . . 6 ⊢ (𝐿 = ⟨0, ((𝑦 + 1) mod 5)⟩ → (𝐾 = ⟨0, ((𝑦 − 1) mod 5)⟩ → ((𝐾 ≠ 𝐿 ∧ (𝑏 ∈ (0..^5) ∧ 𝑦 ∈ (0..^5))) → (({𝐾, ⟨1, 𝑏⟩} ∈ 𝐸 ∧ {⟨1, 𝑏⟩, 𝐿} ∈ 𝐸) → 𝑋 = ⟨1, 𝑏⟩))))
48	31, 41, 47	3jaod 1454	. . . . 5 ⊢ (𝐿 = ⟨0, ((𝑦 + 1) mod 5)⟩ → ((𝐾 = ⟨0, ((𝑦 + 1) mod 5)⟩ ∨ 𝐾 = ⟨1, 𝑦⟩ ∨ 𝐾 = ⟨0, ((𝑦 − 1) mod 5)⟩) → ((𝐾 ≠ 𝐿 ∧ (𝑏 ∈ (0..^5) ∧ 𝑦 ∈ (0..^5))) → (({𝐾, ⟨1, 𝑏⟩} ∈ 𝐸 ∧ {⟨1, 𝑏⟩, 𝐿} ∈ 𝐸) → 𝑋 = ⟨1, 𝑏⟩))))
49		prcom 4700	. . . . . . . . . . . 12 ⊢ {𝐾, ⟨1, 𝑏⟩} = {⟨1, 𝑏⟩, 𝐾}
50	49	eleq1i 2860	. . . . . . . . . . 11 ⊢ ({𝐾, ⟨1, 𝑏⟩} ∈ 𝐸 ↔ {⟨1, 𝑏⟩, 𝐾} ∈ 𝐸)
51		prcom 4700	. . . . . . . . . . . 12 ⊢ {⟨1, 𝑏⟩, 𝐿} = {𝐿, ⟨1, 𝑏⟩}
52	51	eleq1i 2860	. . . . . . . . . . 11 ⊢ ({⟨1, 𝑏⟩, 𝐿} ∈ 𝐸 ↔ {𝐿, ⟨1, 𝑏⟩} ∈ 𝐸)
53	50, 52	anbi12i 639	. . . . . . . . . 10 ⊢ (({𝐾, ⟨1, 𝑏⟩} ∈ 𝐸 ∧ {⟨1, 𝑏⟩, 𝐿} ∈ 𝐸) ↔ ({⟨1, 𝑏⟩, 𝐾} ∈ 𝐸 ∧ {𝐿, ⟨1, 𝑏⟩} ∈ 𝐸))
54	32, 33, 34, 35	pgnbgreunbgrlem5lem1 48769	. . . . . . . . . . . . 13 ⊢ ((((𝐾 = ⟨0, ((𝑦 + 1) mod 5)⟩ ∧ 𝐿 = ⟨1, 𝑦⟩) ∧ (𝑏 ∈ (0..^5) ∧ 𝑦 ∈ (0..^5))) ∧ {𝐿, ⟨1, 𝑏⟩} ∈ 𝐸) → ¬ {⟨1, 𝑏⟩, 𝐾} ∈ 𝐸)
55	54	pm2.21d 122	. . . . . . . . . . . 12 ⊢ ((((𝐾 = ⟨0, ((𝑦 + 1) mod 5)⟩ ∧ 𝐿 = ⟨1, 𝑦⟩) ∧ (𝑏 ∈ (0..^5) ∧ 𝑦 ∈ (0..^5))) ∧ {𝐿, ⟨1, 𝑏⟩} ∈ 𝐸) → ({⟨1, 𝑏⟩, 𝐾} ∈ 𝐸 → 𝑋 = ⟨1, 𝑏⟩))
56	55	ex 417	. . . . . . . . . . 11 ⊢ (((𝐾 = ⟨0, ((𝑦 + 1) mod 5)⟩ ∧ 𝐿 = ⟨1, 𝑦⟩) ∧ (𝑏 ∈ (0..^5) ∧ 𝑦 ∈ (0..^5))) → ({𝐿, ⟨1, 𝑏⟩} ∈ 𝐸 → ({⟨1, 𝑏⟩, 𝐾} ∈ 𝐸 → 𝑋 = ⟨1, 𝑏⟩)))
57	56	impcomd 416	. . . . . . . . . 10 ⊢ (((𝐾 = ⟨0, ((𝑦 + 1) mod 5)⟩ ∧ 𝐿 = ⟨1, 𝑦⟩) ∧ (𝑏 ∈ (0..^5) ∧ 𝑦 ∈ (0..^5))) → (({⟨1, 𝑏⟩, 𝐾} ∈ 𝐸 ∧ {𝐿, ⟨1, 𝑏⟩} ∈ 𝐸) → 𝑋 = ⟨1, 𝑏⟩))
58	53, 57	biimtrid 245	. . . . . . . . 9 ⊢ (((𝐾 = ⟨0, ((𝑦 + 1) mod 5)⟩ ∧ 𝐿 = ⟨1, 𝑦⟩) ∧ (𝑏 ∈ (0..^5) ∧ 𝑦 ∈ (0..^5))) → (({𝐾, ⟨1, 𝑏⟩} ∈ 𝐸 ∧ {⟨1, 𝑏⟩, 𝐿} ∈ 𝐸) → 𝑋 = ⟨1, 𝑏⟩))
59	58	ex 417	. . . . . . . 8 ⊢ ((𝐾 = ⟨0, ((𝑦 + 1) mod 5)⟩ ∧ 𝐿 = ⟨1, 𝑦⟩) → ((𝑏 ∈ (0..^5) ∧ 𝑦 ∈ (0..^5)) → (({𝐾, ⟨1, 𝑏⟩} ∈ 𝐸 ∧ {⟨1, 𝑏⟩, 𝐿} ∈ 𝐸) → 𝑋 = ⟨1, 𝑏⟩)))
60	59	adantld 495	. . . . . . 7 ⊢ ((𝐾 = ⟨0, ((𝑦 + 1) mod 5)⟩ ∧ 𝐿 = ⟨1, 𝑦⟩) → ((𝐾 ≠ 𝐿 ∧ (𝑏 ∈ (0..^5) ∧ 𝑦 ∈ (0..^5))) → (({𝐾, ⟨1, 𝑏⟩} ∈ 𝐸 ∧ {⟨1, 𝑏⟩, 𝐿} ∈ 𝐸) → 𝑋 = ⟨1, 𝑏⟩)))
61	60	expcom 418	. . . . . 6 ⊢ (𝐿 = ⟨1, 𝑦⟩ → (𝐾 = ⟨0, ((𝑦 + 1) mod 5)⟩ → ((𝐾 ≠ 𝐿 ∧ (𝑏 ∈ (0..^5) ∧ 𝑦 ∈ (0..^5))) → (({𝐾, ⟨1, 𝑏⟩} ∈ 𝐸 ∧ {⟨1, 𝑏⟩, 𝐿} ∈ 𝐸) → 𝑋 = ⟨1, 𝑏⟩))))
62		simpr 489	. . . . . . . . . 10 ⊢ ((𝐿 = ⟨1, 𝑦⟩ ∧ 𝐾 = ⟨1, 𝑦⟩) → 𝐾 = ⟨1, 𝑦⟩)
63		simpl 487	. . . . . . . . . 10 ⊢ ((𝐿 = ⟨1, 𝑦⟩ ∧ 𝐾 = ⟨1, 𝑦⟩) → 𝐿 = ⟨1, 𝑦⟩)
64	62, 63	neeq12d 3025	. . . . . . . . 9 ⊢ ((𝐿 = ⟨1, 𝑦⟩ ∧ 𝐾 = ⟨1, 𝑦⟩) → (𝐾 ≠ 𝐿 ↔ ⟨1, 𝑦⟩ ≠ ⟨1, 𝑦⟩))
65		eqid 2769	. . . . . . . . . 10 ⊢ ⟨1, 𝑦⟩ = ⟨1, 𝑦⟩
66		eqneqall 2975	. . . . . . . . . 10 ⊢ (⟨1, 𝑦⟩ = ⟨1, 𝑦⟩ → (⟨1, 𝑦⟩ ≠ ⟨1, 𝑦⟩ → ((𝑏 ∈ (0..^5) ∧ 𝑦 ∈ (0..^5)) → (({𝐾, ⟨1, 𝑏⟩} ∈ 𝐸 ∧ {⟨1, 𝑏⟩, 𝐿} ∈ 𝐸) → 𝑋 = ⟨1, 𝑏⟩))))
67	65, 66	ax-mp 5	. . . . . . . . 9 ⊢ (⟨1, 𝑦⟩ ≠ ⟨1, 𝑦⟩ → ((𝑏 ∈ (0..^5) ∧ 𝑦 ∈ (0..^5)) → (({𝐾, ⟨1, 𝑏⟩} ∈ 𝐸 ∧ {⟨1, 𝑏⟩, 𝐿} ∈ 𝐸) → 𝑋 = ⟨1, 𝑏⟩)))
68	64, 67	biimtrdi 256	. . . . . . . 8 ⊢ ((𝐿 = ⟨1, 𝑦⟩ ∧ 𝐾 = ⟨1, 𝑦⟩) → (𝐾 ≠ 𝐿 → ((𝑏 ∈ (0..^5) ∧ 𝑦 ∈ (0..^5)) → (({𝐾, ⟨1, 𝑏⟩} ∈ 𝐸 ∧ {⟨1, 𝑏⟩, 𝐿} ∈ 𝐸) → 𝑋 = ⟨1, 𝑏⟩))))
69	68	impd 415	. . . . . . 7 ⊢ ((𝐿 = ⟨1, 𝑦⟩ ∧ 𝐾 = ⟨1, 𝑦⟩) → ((𝐾 ≠ 𝐿 ∧ (𝑏 ∈ (0..^5) ∧ 𝑦 ∈ (0..^5))) → (({𝐾, ⟨1, 𝑏⟩} ∈ 𝐸 ∧ {⟨1, 𝑏⟩, 𝐿} ∈ 𝐸) → 𝑋 = ⟨1, 𝑏⟩)))
70	69	ex 417	. . . . . 6 ⊢ (𝐿 = ⟨1, 𝑦⟩ → (𝐾 = ⟨1, 𝑦⟩ → ((𝐾 ≠ 𝐿 ∧ (𝑏 ∈ (0..^5) ∧ 𝑦 ∈ (0..^5))) → (({𝐾, ⟨1, 𝑏⟩} ∈ 𝐸 ∧ {⟨1, 𝑏⟩, 𝐿} ∈ 𝐸) → 𝑋 = ⟨1, 𝑏⟩))))
71	32, 33, 34, 35	pgnbgreunbgrlem5lem2 48770	. . . . . . . . . . . . 13 ⊢ ((((𝐾 = ⟨0, ((𝑦 − 1) mod 5)⟩ ∧ 𝐿 = ⟨1, 𝑦⟩) ∧ (𝑏 ∈ (0..^5) ∧ 𝑦 ∈ (0..^5))) ∧ {𝐿, ⟨1, 𝑏⟩} ∈ 𝐸) → ¬ {⟨1, 𝑏⟩, 𝐾} ∈ 𝐸)
72	71	pm2.21d 122	. . . . . . . . . . . 12 ⊢ ((((𝐾 = ⟨0, ((𝑦 − 1) mod 5)⟩ ∧ 𝐿 = ⟨1, 𝑦⟩) ∧ (𝑏 ∈ (0..^5) ∧ 𝑦 ∈ (0..^5))) ∧ {𝐿, ⟨1, 𝑏⟩} ∈ 𝐸) → ({⟨1, 𝑏⟩, 𝐾} ∈ 𝐸 → 𝑋 = ⟨1, 𝑏⟩))
73	72	ex 417	. . . . . . . . . . 11 ⊢ (((𝐾 = ⟨0, ((𝑦 − 1) mod 5)⟩ ∧ 𝐿 = ⟨1, 𝑦⟩) ∧ (𝑏 ∈ (0..^5) ∧ 𝑦 ∈ (0..^5))) → ({𝐿, ⟨1, 𝑏⟩} ∈ 𝐸 → ({⟨1, 𝑏⟩, 𝐾} ∈ 𝐸 → 𝑋 = ⟨1, 𝑏⟩)))
74	73	impcomd 416	. . . . . . . . . 10 ⊢ (((𝐾 = ⟨0, ((𝑦 − 1) mod 5)⟩ ∧ 𝐿 = ⟨1, 𝑦⟩) ∧ (𝑏 ∈ (0..^5) ∧ 𝑦 ∈ (0..^5))) → (({⟨1, 𝑏⟩, 𝐾} ∈ 𝐸 ∧ {𝐿, ⟨1, 𝑏⟩} ∈ 𝐸) → 𝑋 = ⟨1, 𝑏⟩))
75	53, 74	biimtrid 245	. . . . . . . . 9 ⊢ (((𝐾 = ⟨0, ((𝑦 − 1) mod 5)⟩ ∧ 𝐿 = ⟨1, 𝑦⟩) ∧ (𝑏 ∈ (0..^5) ∧ 𝑦 ∈ (0..^5))) → (({𝐾, ⟨1, 𝑏⟩} ∈ 𝐸 ∧ {⟨1, 𝑏⟩, 𝐿} ∈ 𝐸) → 𝑋 = ⟨1, 𝑏⟩))
76	75	ex 417	. . . . . . . 8 ⊢ ((𝐾 = ⟨0, ((𝑦 − 1) mod 5)⟩ ∧ 𝐿 = ⟨1, 𝑦⟩) → ((𝑏 ∈ (0..^5) ∧ 𝑦 ∈ (0..^5)) → (({𝐾, ⟨1, 𝑏⟩} ∈ 𝐸 ∧ {⟨1, 𝑏⟩, 𝐿} ∈ 𝐸) → 𝑋 = ⟨1, 𝑏⟩)))
77	76	adantld 495	. . . . . . 7 ⊢ ((𝐾 = ⟨0, ((𝑦 − 1) mod 5)⟩ ∧ 𝐿 = ⟨1, 𝑦⟩) → ((𝐾 ≠ 𝐿 ∧ (𝑏 ∈ (0..^5) ∧ 𝑦 ∈ (0..^5))) → (({𝐾, ⟨1, 𝑏⟩} ∈ 𝐸 ∧ {⟨1, 𝑏⟩, 𝐿} ∈ 𝐸) → 𝑋 = ⟨1, 𝑏⟩)))
78	77	expcom 418	. . . . . 6 ⊢ (𝐿 = ⟨1, 𝑦⟩ → (𝐾 = ⟨0, ((𝑦 − 1) mod 5)⟩ → ((𝐾 ≠ 𝐿 ∧ (𝑏 ∈ (0..^5) ∧ 𝑦 ∈ (0..^5))) → (({𝐾, ⟨1, 𝑏⟩} ∈ 𝐸 ∧ {⟨1, 𝑏⟩, 𝐿} ∈ 𝐸) → 𝑋 = ⟨1, 𝑏⟩))))
79	61, 70, 78	3jaod 1454	. . . . 5 ⊢ (𝐿 = ⟨1, 𝑦⟩ → ((𝐾 = ⟨0, ((𝑦 + 1) mod 5)⟩ ∨ 𝐾 = ⟨1, 𝑦⟩ ∨ 𝐾 = ⟨0, ((𝑦 − 1) mod 5)⟩) → ((𝐾 ≠ 𝐿 ∧ (𝑏 ∈ (0..^5) ∧ 𝑦 ∈ (0..^5))) → (({𝐾, ⟨1, 𝑏⟩} ∈ 𝐸 ∧ {⟨1, 𝑏⟩, 𝐿} ∈ 𝐸) → 𝑋 = ⟨1, 𝑏⟩))))
80	32, 33, 34, 35	pgnbgreunbgrlem5lem3 48771	. . . . . . . . . . . . 13 ⊢ ((((𝐾 = ⟨0, ((𝑦 + 1) mod 5)⟩ ∧ 𝐿 = ⟨0, ((𝑦 − 1) mod 5)⟩) ∧ (𝑏 ∈ (0..^5) ∧ 𝑦 ∈ (0..^5))) ∧ {𝐿, ⟨1, 𝑏⟩} ∈ 𝐸) → ¬ {⟨1, 𝑏⟩, 𝐾} ∈ 𝐸)
81	80	pm2.21d 122	. . . . . . . . . . . 12 ⊢ ((((𝐾 = ⟨0, ((𝑦 + 1) mod 5)⟩ ∧ 𝐿 = ⟨0, ((𝑦 − 1) mod 5)⟩) ∧ (𝑏 ∈ (0..^5) ∧ 𝑦 ∈ (0..^5))) ∧ {𝐿, ⟨1, 𝑏⟩} ∈ 𝐸) → ({⟨1, 𝑏⟩, 𝐾} ∈ 𝐸 → 𝑋 = ⟨1, 𝑏⟩))
82	81	ex 417	. . . . . . . . . . 11 ⊢ (((𝐾 = ⟨0, ((𝑦 + 1) mod 5)⟩ ∧ 𝐿 = ⟨0, ((𝑦 − 1) mod 5)⟩) ∧ (𝑏 ∈ (0..^5) ∧ 𝑦 ∈ (0..^5))) → ({𝐿, ⟨1, 𝑏⟩} ∈ 𝐸 → ({⟨1, 𝑏⟩, 𝐾} ∈ 𝐸 → 𝑋 = ⟨1, 𝑏⟩)))
83	82	impcomd 416	. . . . . . . . . 10 ⊢ (((𝐾 = ⟨0, ((𝑦 + 1) mod 5)⟩ ∧ 𝐿 = ⟨0, ((𝑦 − 1) mod 5)⟩) ∧ (𝑏 ∈ (0..^5) ∧ 𝑦 ∈ (0..^5))) → (({⟨1, 𝑏⟩, 𝐾} ∈ 𝐸 ∧ {𝐿, ⟨1, 𝑏⟩} ∈ 𝐸) → 𝑋 = ⟨1, 𝑏⟩))
84	53, 83	biimtrid 245	. . . . . . . . 9 ⊢ (((𝐾 = ⟨0, ((𝑦 + 1) mod 5)⟩ ∧ 𝐿 = ⟨0, ((𝑦 − 1) mod 5)⟩) ∧ (𝑏 ∈ (0..^5) ∧ 𝑦 ∈ (0..^5))) → (({𝐾, ⟨1, 𝑏⟩} ∈ 𝐸 ∧ {⟨1, 𝑏⟩, 𝐿} ∈ 𝐸) → 𝑋 = ⟨1, 𝑏⟩))
85	84	ex 417	. . . . . . . 8 ⊢ ((𝐾 = ⟨0, ((𝑦 + 1) mod 5)⟩ ∧ 𝐿 = ⟨0, ((𝑦 − 1) mod 5)⟩) → ((𝑏 ∈ (0..^5) ∧ 𝑦 ∈ (0..^5)) → (({𝐾, ⟨1, 𝑏⟩} ∈ 𝐸 ∧ {⟨1, 𝑏⟩, 𝐿} ∈ 𝐸) → 𝑋 = ⟨1, 𝑏⟩)))
86	85	adantld 495	. . . . . . 7 ⊢ ((𝐾 = ⟨0, ((𝑦 + 1) mod 5)⟩ ∧ 𝐿 = ⟨0, ((𝑦 − 1) mod 5)⟩) → ((𝐾 ≠ 𝐿 ∧ (𝑏 ∈ (0..^5) ∧ 𝑦 ∈ (0..^5))) → (({𝐾, ⟨1, 𝑏⟩} ∈ 𝐸 ∧ {⟨1, 𝑏⟩, 𝐿} ∈ 𝐸) → 𝑋 = ⟨1, 𝑏⟩)))
87	86	expcom 418	. . . . . 6 ⊢ (𝐿 = ⟨0, ((𝑦 − 1) mod 5)⟩ → (𝐾 = ⟨0, ((𝑦 + 1) mod 5)⟩ → ((𝐾 ≠ 𝐿 ∧ (𝑏 ∈ (0..^5) ∧ 𝑦 ∈ (0..^5))) → (({𝐾, ⟨1, 𝑏⟩} ∈ 𝐸 ∧ {⟨1, 𝑏⟩, 𝐿} ∈ 𝐸) → 𝑋 = ⟨1, 𝑏⟩))))
88	32, 33, 34, 35	pgnbgreunbgrlem5lem2 48770	. . . . . . . . . . 11 ⊢ ((((𝐿 = ⟨0, ((𝑦 − 1) mod 5)⟩ ∧ 𝐾 = ⟨1, 𝑦⟩) ∧ (𝑏 ∈ (0..^5) ∧ 𝑦 ∈ (0..^5))) ∧ {𝐾, ⟨1, 𝑏⟩} ∈ 𝐸) → ¬ {⟨1, 𝑏⟩, 𝐿} ∈ 𝐸)
89	88	pm2.21d 122	. . . . . . . . . 10 ⊢ ((((𝐿 = ⟨0, ((𝑦 − 1) mod 5)⟩ ∧ 𝐾 = ⟨1, 𝑦⟩) ∧ (𝑏 ∈ (0..^5) ∧ 𝑦 ∈ (0..^5))) ∧ {𝐾, ⟨1, 𝑏⟩} ∈ 𝐸) → ({⟨1, 𝑏⟩, 𝐿} ∈ 𝐸 → 𝑋 = ⟨1, 𝑏⟩))
90	89	expimpd 458	. . . . . . . . 9 ⊢ (((𝐿 = ⟨0, ((𝑦 − 1) mod 5)⟩ ∧ 𝐾 = ⟨1, 𝑦⟩) ∧ (𝑏 ∈ (0..^5) ∧ 𝑦 ∈ (0..^5))) → (({𝐾, ⟨1, 𝑏⟩} ∈ 𝐸 ∧ {⟨1, 𝑏⟩, 𝐿} ∈ 𝐸) → 𝑋 = ⟨1, 𝑏⟩))
91	90	ex 417	. . . . . . . 8 ⊢ ((𝐿 = ⟨0, ((𝑦 − 1) mod 5)⟩ ∧ 𝐾 = ⟨1, 𝑦⟩) → ((𝑏 ∈ (0..^5) ∧ 𝑦 ∈ (0..^5)) → (({𝐾, ⟨1, 𝑏⟩} ∈ 𝐸 ∧ {⟨1, 𝑏⟩, 𝐿} ∈ 𝐸) → 𝑋 = ⟨1, 𝑏⟩)))
92	91	adantld 495	. . . . . . 7 ⊢ ((𝐿 = ⟨0, ((𝑦 − 1) mod 5)⟩ ∧ 𝐾 = ⟨1, 𝑦⟩) → ((𝐾 ≠ 𝐿 ∧ (𝑏 ∈ (0..^5) ∧ 𝑦 ∈ (0..^5))) → (({𝐾, ⟨1, 𝑏⟩} ∈ 𝐸 ∧ {⟨1, 𝑏⟩, 𝐿} ∈ 𝐸) → 𝑋 = ⟨1, 𝑏⟩)))
93	92	ex 417	. . . . . 6 ⊢ (𝐿 = ⟨0, ((𝑦 − 1) mod 5)⟩ → (𝐾 = ⟨1, 𝑦⟩ → ((𝐾 ≠ 𝐿 ∧ (𝑏 ∈ (0..^5) ∧ 𝑦 ∈ (0..^5))) → (({𝐾, ⟨1, 𝑏⟩} ∈ 𝐸 ∧ {⟨1, 𝑏⟩, 𝐿} ∈ 𝐸) → 𝑋 = ⟨1, 𝑏⟩))))
94		simpr 489	. . . . . . . . . 10 ⊢ ((𝐿 = ⟨0, ((𝑦 − 1) mod 5)⟩ ∧ 𝐾 = ⟨0, ((𝑦 − 1) mod 5)⟩) → 𝐾 = ⟨0, ((𝑦 − 1) mod 5)⟩)
95		simpl 487	. . . . . . . . . 10 ⊢ ((𝐿 = ⟨0, ((𝑦 − 1) mod 5)⟩ ∧ 𝐾 = ⟨0, ((𝑦 − 1) mod 5)⟩) → 𝐿 = ⟨0, ((𝑦 − 1) mod 5)⟩)
96	94, 95	neeq12d 3025	. . . . . . . . 9 ⊢ ((𝐿 = ⟨0, ((𝑦 − 1) mod 5)⟩ ∧ 𝐾 = ⟨0, ((𝑦 − 1) mod 5)⟩) → (𝐾 ≠ 𝐿 ↔ ⟨0, ((𝑦 − 1) mod 5)⟩ ≠ ⟨0, ((𝑦 − 1) mod 5)⟩))
97		eqid 2769	. . . . . . . . . 10 ⊢ ⟨0, ((𝑦 − 1) mod 5)⟩ = ⟨0, ((𝑦 − 1) mod 5)⟩
98		eqneqall 2975	. . . . . . . . . 10 ⊢ (⟨0, ((𝑦 − 1) mod 5)⟩ = ⟨0, ((𝑦 − 1) mod 5)⟩ → (⟨0, ((𝑦 − 1) mod 5)⟩ ≠ ⟨0, ((𝑦 − 1) mod 5)⟩ → ((𝑏 ∈ (0..^5) ∧ 𝑦 ∈ (0..^5)) → (({𝐾, ⟨1, 𝑏⟩} ∈ 𝐸 ∧ {⟨1, 𝑏⟩, 𝐿} ∈ 𝐸) → 𝑋 = ⟨1, 𝑏⟩))))
99	97, 98	ax-mp 5	. . . . . . . . 9 ⊢ (⟨0, ((𝑦 − 1) mod 5)⟩ ≠ ⟨0, ((𝑦 − 1) mod 5)⟩ → ((𝑏 ∈ (0..^5) ∧ 𝑦 ∈ (0..^5)) → (({𝐾, ⟨1, 𝑏⟩} ∈ 𝐸 ∧ {⟨1, 𝑏⟩, 𝐿} ∈ 𝐸) → 𝑋 = ⟨1, 𝑏⟩)))
100	96, 99	biimtrdi 256	. . . . . . . 8 ⊢ ((𝐿 = ⟨0, ((𝑦 − 1) mod 5)⟩ ∧ 𝐾 = ⟨0, ((𝑦 − 1) mod 5)⟩) → (𝐾 ≠ 𝐿 → ((𝑏 ∈ (0..^5) ∧ 𝑦 ∈ (0..^5)) → (({𝐾, ⟨1, 𝑏⟩} ∈ 𝐸 ∧ {⟨1, 𝑏⟩, 𝐿} ∈ 𝐸) → 𝑋 = ⟨1, 𝑏⟩))))
101	100	impd 415	. . . . . . 7 ⊢ ((𝐿 = ⟨0, ((𝑦 − 1) mod 5)⟩ ∧ 𝐾 = ⟨0, ((𝑦 − 1) mod 5)⟩) → ((𝐾 ≠ 𝐿 ∧ (𝑏 ∈ (0..^5) ∧ 𝑦 ∈ (0..^5))) → (({𝐾, ⟨1, 𝑏⟩} ∈ 𝐸 ∧ {⟨1, 𝑏⟩, 𝐿} ∈ 𝐸) → 𝑋 = ⟨1, 𝑏⟩)))
102	101	ex 417	. . . . . 6 ⊢ (𝐿 = ⟨0, ((𝑦 − 1) mod 5)⟩ → (𝐾 = ⟨0, ((𝑦 − 1) mod 5)⟩ → ((𝐾 ≠ 𝐿 ∧ (𝑏 ∈ (0..^5) ∧ 𝑦 ∈ (0..^5))) → (({𝐾, ⟨1, 𝑏⟩} ∈ 𝐸 ∧ {⟨1, 𝑏⟩, 𝐿} ∈ 𝐸) → 𝑋 = ⟨1, 𝑏⟩))))
103	87, 93, 102	3jaod 1454	. . . . 5 ⊢ (𝐿 = ⟨0, ((𝑦 − 1) mod 5)⟩ → ((𝐾 = ⟨0, ((𝑦 + 1) mod 5)⟩ ∨ 𝐾 = ⟨1, 𝑦⟩ ∨ 𝐾 = ⟨0, ((𝑦 − 1) mod 5)⟩) → ((𝐾 ≠ 𝐿 ∧ (𝑏 ∈ (0..^5) ∧ 𝑦 ∈ (0..^5))) → (({𝐾, ⟨1, 𝑏⟩} ∈ 𝐸 ∧ {⟨1, 𝑏⟩, 𝐿} ∈ 𝐸) → 𝑋 = ⟨1, 𝑏⟩))))
104	48, 79, 103	3jaoi 1452	. . . 4 ⊢ ((𝐿 = ⟨0, ((𝑦 + 1) mod 5)⟩ ∨ 𝐿 = ⟨1, 𝑦⟩ ∨ 𝐿 = ⟨0, ((𝑦 − 1) mod 5)⟩) → ((𝐾 = ⟨0, ((𝑦 + 1) mod 5)⟩ ∨ 𝐾 = ⟨1, 𝑦⟩ ∨ 𝐾 = ⟨0, ((𝑦 − 1) mod 5)⟩) → ((𝐾 ≠ 𝐿 ∧ (𝑏 ∈ (0..^5) ∧ 𝑦 ∈ (0..^5))) → (({𝐾, ⟨1, 𝑏⟩} ∈ 𝐸 ∧ {⟨1, 𝑏⟩, 𝐿} ∈ 𝐸) → 𝑋 = ⟨1, 𝑏⟩))))
105	104	imp 411	. . 3 ⊢ (((𝐿 = ⟨0, ((𝑦 + 1) mod 5)⟩ ∨ 𝐿 = ⟨1, 𝑦⟩ ∨ 𝐿 = ⟨0, ((𝑦 − 1) mod 5)⟩) ∧ (𝐾 = ⟨0, ((𝑦 + 1) mod 5)⟩ ∨ 𝐾 = ⟨1, 𝑦⟩ ∨ 𝐾 = ⟨0, ((𝑦 − 1) mod 5)⟩)) → ((𝐾 ≠ 𝐿 ∧ (𝑏 ∈ (0..^5) ∧ 𝑦 ∈ (0..^5))) → (({𝐾, ⟨1, 𝑏⟩} ∈ 𝐸 ∧ {⟨1, 𝑏⟩, 𝐿} ∈ 𝐸) → 𝑋 = ⟨1, 𝑏⟩)))
106	21, 105	biimtrdi 256	. 2 ⊢ ((𝑋 = ⟨0, 𝑦⟩ ∧ 𝑋 ∈ 𝑉) → (((𝐿 = ⟨0, (((2^nd ‘𝑋) + 1) mod 5)⟩ ∨ 𝐿 = ⟨1, (2^nd ‘𝑋)⟩ ∨ 𝐿 = ⟨0, (((2^nd ‘𝑋) − 1) mod 5)⟩) ∧ (𝐾 = ⟨0, (((2^nd ‘𝑋) + 1) mod 5)⟩ ∨ 𝐾 = ⟨1, (2^nd ‘𝑋)⟩ ∨ 𝐾 = ⟨0, (((2^nd ‘𝑋) − 1) mod 5)⟩)) → ((𝐾 ≠ 𝐿 ∧ (𝑏 ∈ (0..^5) ∧ 𝑦 ∈ (0..^5))) → (({𝐾, ⟨1, 𝑏⟩} ∈ 𝐸 ∧ {⟨1, 𝑏⟩, 𝐿} ∈ 𝐸) → 𝑋 = ⟨1, 𝑏⟩))))
107	106	expdcom 419	1 ⊢ ((𝐿 = ⟨0, (((2^nd ‘𝑋) + 1) mod 5)⟩ ∨ 𝐿 = ⟨1, (2^nd ‘𝑋)⟩ ∨ 𝐿 = ⟨0, (((2^nd ‘𝑋) − 1) mod 5)⟩) → ((𝐾 = ⟨0, (((2^nd ‘𝑋) + 1) mod 5)⟩ ∨ 𝐾 = ⟨1, (2^nd ‘𝑋)⟩ ∨ 𝐾 = ⟨0, (((2^nd ‘𝑋) − 1) mod 5)⟩) → ((𝑋 = ⟨0, 𝑦⟩ ∧ 𝑋 ∈ 𝑉) → ((𝐾 ≠ 𝐿 ∧ (𝑏 ∈ (0..^5) ∧ 𝑦 ∈ (0..^5))) → (({𝐾, ⟨1, 𝑏⟩} ∈ 𝐸 ∧ {⟨1, 𝑏⟩, 𝐿} ∈ 𝐸) → 𝑋 = ⟨1, 𝑏⟩)))))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 209 ∧ wa 400 ∨ w3o 1100 = wceq 1567 ∈ wcel 2149 ≠ wne 2964 {cpr 4593 ⟨cop 4597 ‘cfv 6534 (class class class)co 7408 2^nd c2nd 7981 0cc0 11096 1c1 11097 + caddc 11099 − cmin 11437 2c2 12291 5c5 12294 ..^cfzo 13678 mod cmo 13898 Vtxcvtx 29283 Edgcedg 29334 NeighbVtx cnbgr 29619 gPetersenGr cgpg 48689

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1822 ax-4 1836 ax-5 1937 ax-6 1994 ax-7 2035 ax-8 2151 ax-9 2159 ax-10 2182 ax-11 2198 ax-12 2219 ax-ext 2741 ax-rep 5239 ax-sep 5258 ax-nul 5268 ax-pow 5334 ax-pr 5402 ax-un 7730 ax-cnex 11152 ax-resscn 11153 ax-1cn 11154 ax-icn 11155 ax-addcl 11156 ax-addrcl 11157 ax-mulcl 11158 ax-mulrcl 11159 ax-mulcom 11160 ax-addass 11161 ax-mulass 11162 ax-distr 11163 ax-i2m1 11164 ax-1ne0 11165 ax-1rid 11166 ax-rnegex 11167 ax-rrecex 11168 ax-cnre 11169 ax-pre-lttri 11170 ax-pre-lttrn 11171 ax-pre-ltadd 11172 ax-pre-mulgt0 11173 ax-pre-sup 11174

This theorem depends on definitions: df-bi 210 df-an 401 df-or 861 df-3or 1102 df-3an 1103 df-tru 1570 df-fal 1580 df-ex 1807 df-nf 1811 df-sb 2098 df-mo 2573 df-eu 2603 df-clab 2748 df-cleq 2761 df-clel 2844 df-nfc 2918 df-ne 2965 df-nel 3071 df-ral 3086 df-rex 3096 df-rmo 3376 df-reu 3377 df-rab 3424 df-v 3465 df-sbc 3754 df-csb 3862 df-dif 3916 df-un 3918 df-in 3920 df-ss 3930 df-pss 3933 df-nul 4295 df-if 4490 df-pw 4566 df-sn 4592 df-pr 4594 df-op 4598 df-uni 4874 df-int 4914 df-iun 4959 df-br 5111 df-opab 5175 df-mpt 5194 df-tr 5220 df-id 5554 df-eprel 5559 df-po 5567 df-so 5568 df-fr 5612 df-we 5614 df-xp 5665 df-rel 5666 df-cnv 5667 df-co 5668 df-dm 5669 df-rn 5670 df-res 5671 df-ima 5672 df-pred 6300 df-ord 6361 df-on 6362 df-lim 6363 df-suc 6364 df-iota 6490 df-fun 6536 df-fn 6537 df-f 6538 df-f1 6539 df-fo 6540 df-f1o 6541 df-fv 6542 df-riota 7365 df-ov 7411 df-oprab 7412 df-mpo 7413 df-om 7859 df-1st 7982 df-2nd 7983 df-frecs 8274 df-wrecs 8305 df-recs 8354 df-rdg 8393 df-1o 8449 df-oadd 8453 df-er 8690 df-en 8940 df-dom 8941 df-sdom 8942 df-fin 8943 df-sup 9398 df-inf 9399 df-dju 9883 df-card 9921 df-pnf 11241 df-mnf 11242 df-xr 11243 df-ltxr 11244 df-le 11245 df-sub 11439 df-neg 11440 df-div 11868 df-nn 12230 df-2 12299 df-3 12300 df-4 12301 df-5 12302 df-6 12303 df-7 12304 df-8 12305 df-9 12306 df-n0 12501 df-xnn0 12574 df-z 12588 df-dec 12708 df-uz 12859 df-rp 13013 df-ico 13374 df-fz 13532 df-fzo 13679 df-fl 13821 df-ceil 13822 df-mod 13899 df-seq 14034 df-exp 14094 df-hash 14363 df-cj 15146 df-re 15147 df-im 15148 df-sqrt 15282 df-abs 15283 df-dvds 16307 df-struct 17203 df-slot 17238 df-ndx 17250 df-base 17266 df-edgf 29276 df-vtx 29285 df-iedg 29286 df-edg 29335 df-umgr 29370 df-usgr 29438 df-gpg 48690

This theorem is referenced by: pgnbgreunbgrlem6 48773

W3C validator