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 48285

Description: Lemma 5 for pgnbgreunbgr 48287. 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 11117	. . . . . 6 ⊢ 0 ∈ V
2		vex 3441	. . . . . 6 ⊢ 𝑦 ∈ V
3	1, 2	op2ndd 7941	. . . . 5 ⊢ (𝑋 = ⟨0, 𝑦⟩ → (2^nd ‘𝑋) = 𝑦)
4	3	adantr 480	. . . 4 ⊢ ((𝑋 = ⟨0, 𝑦⟩ ∧ 𝑋 ∈ 𝑉) → (2^nd ‘𝑋) = 𝑦)
5		oveq1 7362	. . . . . . . . 9 ⊢ ((2^nd ‘𝑋) = 𝑦 → ((2^nd ‘𝑋) + 1) = (𝑦 + 1))
6	5	oveq1d 7370	. . . . . . . 8 ⊢ ((2^nd ‘𝑋) = 𝑦 → (((2^nd ‘𝑋) + 1) mod 5) = ((𝑦 + 1) mod 5))
7	6	opeq2d 4833	. . . . . . 7 ⊢ ((2^nd ‘𝑋) = 𝑦 → ⟨0, (((2^nd ‘𝑋) + 1) mod 5)⟩ = ⟨0, ((𝑦 + 1) mod 5)⟩)
8	7	eqeq2d 2744	. . . . . 6 ⊢ ((2^nd ‘𝑋) = 𝑦 → (𝐿 = ⟨0, (((2^nd ‘𝑋) + 1) mod 5)⟩ ↔ 𝐿 = ⟨0, ((𝑦 + 1) mod 5)⟩))
9		opeq2 4827	. . . . . . 7 ⊢ ((2^nd ‘𝑋) = 𝑦 → ⟨1, (2^nd ‘𝑋)⟩ = ⟨1, 𝑦⟩)
10	9	eqeq2d 2744	. . . . . 6 ⊢ ((2^nd ‘𝑋) = 𝑦 → (𝐿 = ⟨1, (2^nd ‘𝑋)⟩ ↔ 𝐿 = ⟨1, 𝑦⟩))
11		oveq1 7362	. . . . . . . . 9 ⊢ ((2^nd ‘𝑋) = 𝑦 → ((2^nd ‘𝑋) − 1) = (𝑦 − 1))
12	11	oveq1d 7370	. . . . . . . 8 ⊢ ((2^nd ‘𝑋) = 𝑦 → (((2^nd ‘𝑋) − 1) mod 5) = ((𝑦 − 1) mod 5))
13	12	opeq2d 4833	. . . . . . 7 ⊢ ((2^nd ‘𝑋) = 𝑦 → ⟨0, (((2^nd ‘𝑋) − 1) mod 5)⟩ = ⟨0, ((𝑦 − 1) mod 5)⟩)
14	13	eqeq2d 2744	. . . . . 6 ⊢ ((2^nd ‘𝑋) = 𝑦 → (𝐿 = ⟨0, (((2^nd ‘𝑋) − 1) mod 5)⟩ ↔ 𝐿 = ⟨0, ((𝑦 − 1) mod 5)⟩))
15	8, 10, 14	3orbi123d 1437	. . . . 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 2744	. . . . . 6 ⊢ ((2^nd ‘𝑋) = 𝑦 → (𝐾 = ⟨0, (((2^nd ‘𝑋) + 1) mod 5)⟩ ↔ 𝐾 = ⟨0, ((𝑦 + 1) mod 5)⟩))
17	9	eqeq2d 2744	. . . . . 6 ⊢ ((2^nd ‘𝑋) = 𝑦 → (𝐾 = ⟨1, (2^nd ‘𝑋)⟩ ↔ 𝐾 = ⟨1, 𝑦⟩))
18	13	eqeq2d 2744	. . . . . 6 ⊢ ((2^nd ‘𝑋) = 𝑦 → (𝐾 = ⟨0, (((2^nd ‘𝑋) − 1) mod 5)⟩ ↔ 𝐾 = ⟨0, ((𝑦 − 1) mod 5)⟩))
19	16, 17, 18	3orbi123d 1437	. . . . 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 632	. . . 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 17	. . 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 482	. . . . . . . . . . 11 ⊢ ((𝐾 = ⟨0, ((𝑦 + 1) mod 5)⟩ ∧ 𝐿 = ⟨0, ((𝑦 + 1) mod 5)⟩) → 𝐾 = ⟨0, ((𝑦 + 1) mod 5)⟩)
23		simpr 484	. . . . . . . . . . 11 ⊢ ((𝐾 = ⟨0, ((𝑦 + 1) mod 5)⟩ ∧ 𝐿 = ⟨0, ((𝑦 + 1) mod 5)⟩) → 𝐿 = ⟨0, ((𝑦 + 1) mod 5)⟩)
24	22, 23	neeq12d 2990	. . . . . . . . . 10 ⊢ ((𝐾 = ⟨0, ((𝑦 + 1) mod 5)⟩ ∧ 𝐿 = ⟨0, ((𝑦 + 1) mod 5)⟩) → (𝐾 ≠ 𝐿 ↔ ⟨0, ((𝑦 + 1) mod 5)⟩ ≠ ⟨0, ((𝑦 + 1) mod 5)⟩))
25	24	ancoms 458	. . . . . . . . 9 ⊢ ((𝐿 = ⟨0, ((𝑦 + 1) mod 5)⟩ ∧ 𝐾 = ⟨0, ((𝑦 + 1) mod 5)⟩) → (𝐾 ≠ 𝐿 ↔ ⟨0, ((𝑦 + 1) mod 5)⟩ ≠ ⟨0, ((𝑦 + 1) mod 5)⟩))
26		eqid 2733	. . . . . . . . . 10 ⊢ ⟨0, ((𝑦 + 1) mod 5)⟩ = ⟨0, ((𝑦 + 1) mod 5)⟩
27		eqneqall 2940	. . . . . . . . . 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 253	. . . . . . . 8 ⊢ ((𝐿 = ⟨0, ((𝑦 + 1) mod 5)⟩ ∧ 𝐾 = ⟨0, ((𝑦 + 1) mod 5)⟩) → (𝐾 ≠ 𝐿 → ((𝑏 ∈ (0..^5) ∧ 𝑦 ∈ (0..^5)) → (({𝐾, ⟨1, 𝑏⟩} ∈ 𝐸 ∧ {⟨1, 𝑏⟩, 𝐿} ∈ 𝐸) → 𝑋 = ⟨1, 𝑏⟩))))
30	29	impd 410	. . . . . . 7 ⊢ ((𝐿 = ⟨0, ((𝑦 + 1) mod 5)⟩ ∧ 𝐾 = ⟨0, ((𝑦 + 1) mod 5)⟩) → ((𝐾 ≠ 𝐿 ∧ (𝑏 ∈ (0..^5) ∧ 𝑦 ∈ (0..^5))) → (({𝐾, ⟨1, 𝑏⟩} ∈ 𝐸 ∧ {⟨1, 𝑏⟩, 𝐿} ∈ 𝐸) → 𝑋 = ⟨1, 𝑏⟩)))
31	30	ex 412	. . . . . 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 48282	. . . . . . . . . . 11 ⊢ ((((𝐿 = ⟨0, ((𝑦 + 1) mod 5)⟩ ∧ 𝐾 = ⟨1, 𝑦⟩) ∧ (𝑏 ∈ (0..^5) ∧ 𝑦 ∈ (0..^5))) ∧ {𝐾, ⟨1, 𝑏⟩} ∈ 𝐸) → ¬ {⟨1, 𝑏⟩, 𝐿} ∈ 𝐸)
37	36	pm2.21d 121	. . . . . . . . . 10 ⊢ ((((𝐿 = ⟨0, ((𝑦 + 1) mod 5)⟩ ∧ 𝐾 = ⟨1, 𝑦⟩) ∧ (𝑏 ∈ (0..^5) ∧ 𝑦 ∈ (0..^5))) ∧ {𝐾, ⟨1, 𝑏⟩} ∈ 𝐸) → ({⟨1, 𝑏⟩, 𝐿} ∈ 𝐸 → 𝑋 = ⟨1, 𝑏⟩))
38	37	expimpd 453	. . . . . . . . 9 ⊢ (((𝐿 = ⟨0, ((𝑦 + 1) mod 5)⟩ ∧ 𝐾 = ⟨1, 𝑦⟩) ∧ (𝑏 ∈ (0..^5) ∧ 𝑦 ∈ (0..^5))) → (({𝐾, ⟨1, 𝑏⟩} ∈ 𝐸 ∧ {⟨1, 𝑏⟩, 𝐿} ∈ 𝐸) → 𝑋 = ⟨1, 𝑏⟩))
39	38	ex 412	. . . . . . . 8 ⊢ ((𝐿 = ⟨0, ((𝑦 + 1) mod 5)⟩ ∧ 𝐾 = ⟨1, 𝑦⟩) → ((𝑏 ∈ (0..^5) ∧ 𝑦 ∈ (0..^5)) → (({𝐾, ⟨1, 𝑏⟩} ∈ 𝐸 ∧ {⟨1, 𝑏⟩, 𝐿} ∈ 𝐸) → 𝑋 = ⟨1, 𝑏⟩)))
40	39	adantld 490	. . . . . . 7 ⊢ ((𝐿 = ⟨0, ((𝑦 + 1) mod 5)⟩ ∧ 𝐾 = ⟨1, 𝑦⟩) → ((𝐾 ≠ 𝐿 ∧ (𝑏 ∈ (0..^5) ∧ 𝑦 ∈ (0..^5))) → (({𝐾, ⟨1, 𝑏⟩} ∈ 𝐸 ∧ {⟨1, 𝑏⟩, 𝐿} ∈ 𝐸) → 𝑋 = ⟨1, 𝑏⟩)))
41	40	ex 412	. . . . . 6 ⊢ (𝐿 = ⟨0, ((𝑦 + 1) mod 5)⟩ → (𝐾 = ⟨1, 𝑦⟩ → ((𝐾 ≠ 𝐿 ∧ (𝑏 ∈ (0..^5) ∧ 𝑦 ∈ (0..^5))) → (({𝐾, ⟨1, 𝑏⟩} ∈ 𝐸 ∧ {⟨1, 𝑏⟩, 𝐿} ∈ 𝐸) → 𝑋 = ⟨1, 𝑏⟩))))
42	32, 33, 34, 35	pgnbgreunbgrlem5lem3 48284	. . . . . . . . . . 11 ⊢ ((((𝐿 = ⟨0, ((𝑦 + 1) mod 5)⟩ ∧ 𝐾 = ⟨0, ((𝑦 − 1) mod 5)⟩) ∧ (𝑏 ∈ (0..^5) ∧ 𝑦 ∈ (0..^5))) ∧ {𝐾, ⟨1, 𝑏⟩} ∈ 𝐸) → ¬ {⟨1, 𝑏⟩, 𝐿} ∈ 𝐸)
43	42	pm2.21d 121	. . . . . . . . . 10 ⊢ ((((𝐿 = ⟨0, ((𝑦 + 1) mod 5)⟩ ∧ 𝐾 = ⟨0, ((𝑦 − 1) mod 5)⟩) ∧ (𝑏 ∈ (0..^5) ∧ 𝑦 ∈ (0..^5))) ∧ {𝐾, ⟨1, 𝑏⟩} ∈ 𝐸) → ({⟨1, 𝑏⟩, 𝐿} ∈ 𝐸 → 𝑋 = ⟨1, 𝑏⟩))
44	43	expimpd 453	. . . . . . . . 9 ⊢ (((𝐿 = ⟨0, ((𝑦 + 1) mod 5)⟩ ∧ 𝐾 = ⟨0, ((𝑦 − 1) mod 5)⟩) ∧ (𝑏 ∈ (0..^5) ∧ 𝑦 ∈ (0..^5))) → (({𝐾, ⟨1, 𝑏⟩} ∈ 𝐸 ∧ {⟨1, 𝑏⟩, 𝐿} ∈ 𝐸) → 𝑋 = ⟨1, 𝑏⟩))
45	44	ex 412	. . . . . . . 8 ⊢ ((𝐿 = ⟨0, ((𝑦 + 1) mod 5)⟩ ∧ 𝐾 = ⟨0, ((𝑦 − 1) mod 5)⟩) → ((𝑏 ∈ (0..^5) ∧ 𝑦 ∈ (0..^5)) → (({𝐾, ⟨1, 𝑏⟩} ∈ 𝐸 ∧ {⟨1, 𝑏⟩, 𝐿} ∈ 𝐸) → 𝑋 = ⟨1, 𝑏⟩)))
46	45	adantld 490	. . . . . . 7 ⊢ ((𝐿 = ⟨0, ((𝑦 + 1) mod 5)⟩ ∧ 𝐾 = ⟨0, ((𝑦 − 1) mod 5)⟩) → ((𝐾 ≠ 𝐿 ∧ (𝑏 ∈ (0..^5) ∧ 𝑦 ∈ (0..^5))) → (({𝐾, ⟨1, 𝑏⟩} ∈ 𝐸 ∧ {⟨1, 𝑏⟩, 𝐿} ∈ 𝐸) → 𝑋 = ⟨1, 𝑏⟩)))
47	46	ex 412	. . . . . 6 ⊢ (𝐿 = ⟨0, ((𝑦 + 1) mod 5)⟩ → (𝐾 = ⟨0, ((𝑦 − 1) mod 5)⟩ → ((𝐾 ≠ 𝐿 ∧ (𝑏 ∈ (0..^5) ∧ 𝑦 ∈ (0..^5))) → (({𝐾, ⟨1, 𝑏⟩} ∈ 𝐸 ∧ {⟨1, 𝑏⟩, 𝐿} ∈ 𝐸) → 𝑋 = ⟨1, 𝑏⟩))))
48	31, 41, 47	3jaod 1431	. . . . 5 ⊢ (𝐿 = ⟨0, ((𝑦 + 1) mod 5)⟩ → ((𝐾 = ⟨0, ((𝑦 + 1) mod 5)⟩ ∨ 𝐾 = ⟨1, 𝑦⟩ ∨ 𝐾 = ⟨0, ((𝑦 − 1) mod 5)⟩) → ((𝐾 ≠ 𝐿 ∧ (𝑏 ∈ (0..^5) ∧ 𝑦 ∈ (0..^5))) → (({𝐾, ⟨1, 𝑏⟩} ∈ 𝐸 ∧ {⟨1, 𝑏⟩, 𝐿} ∈ 𝐸) → 𝑋 = ⟨1, 𝑏⟩))))
49		prcom 4686	. . . . . . . . . . . 12 ⊢ {𝐾, ⟨1, 𝑏⟩} = {⟨1, 𝑏⟩, 𝐾}
50	49	eleq1i 2824	. . . . . . . . . . 11 ⊢ ({𝐾, ⟨1, 𝑏⟩} ∈ 𝐸 ↔ {⟨1, 𝑏⟩, 𝐾} ∈ 𝐸)
51		prcom 4686	. . . . . . . . . . . 12 ⊢ {⟨1, 𝑏⟩, 𝐿} = {𝐿, ⟨1, 𝑏⟩}
52	51	eleq1i 2824	. . . . . . . . . . 11 ⊢ ({⟨1, 𝑏⟩, 𝐿} ∈ 𝐸 ↔ {𝐿, ⟨1, 𝑏⟩} ∈ 𝐸)
53	50, 52	anbi12i 628	. . . . . . . . . 10 ⊢ (({𝐾, ⟨1, 𝑏⟩} ∈ 𝐸 ∧ {⟨1, 𝑏⟩, 𝐿} ∈ 𝐸) ↔ ({⟨1, 𝑏⟩, 𝐾} ∈ 𝐸 ∧ {𝐿, ⟨1, 𝑏⟩} ∈ 𝐸))
54	32, 33, 34, 35	pgnbgreunbgrlem5lem1 48282	. . . . . . . . . . . . 13 ⊢ ((((𝐾 = ⟨0, ((𝑦 + 1) mod 5)⟩ ∧ 𝐿 = ⟨1, 𝑦⟩) ∧ (𝑏 ∈ (0..^5) ∧ 𝑦 ∈ (0..^5))) ∧ {𝐿, ⟨1, 𝑏⟩} ∈ 𝐸) → ¬ {⟨1, 𝑏⟩, 𝐾} ∈ 𝐸)
55	54	pm2.21d 121	. . . . . . . . . . . 12 ⊢ ((((𝐾 = ⟨0, ((𝑦 + 1) mod 5)⟩ ∧ 𝐿 = ⟨1, 𝑦⟩) ∧ (𝑏 ∈ (0..^5) ∧ 𝑦 ∈ (0..^5))) ∧ {𝐿, ⟨1, 𝑏⟩} ∈ 𝐸) → ({⟨1, 𝑏⟩, 𝐾} ∈ 𝐸 → 𝑋 = ⟨1, 𝑏⟩))
56	55	ex 412	. . . . . . . . . . 11 ⊢ (((𝐾 = ⟨0, ((𝑦 + 1) mod 5)⟩ ∧ 𝐿 = ⟨1, 𝑦⟩) ∧ (𝑏 ∈ (0..^5) ∧ 𝑦 ∈ (0..^5))) → ({𝐿, ⟨1, 𝑏⟩} ∈ 𝐸 → ({⟨1, 𝑏⟩, 𝐾} ∈ 𝐸 → 𝑋 = ⟨1, 𝑏⟩)))
57	56	impcomd 411	. . . . . . . . . 10 ⊢ (((𝐾 = ⟨0, ((𝑦 + 1) mod 5)⟩ ∧ 𝐿 = ⟨1, 𝑦⟩) ∧ (𝑏 ∈ (0..^5) ∧ 𝑦 ∈ (0..^5))) → (({⟨1, 𝑏⟩, 𝐾} ∈ 𝐸 ∧ {𝐿, ⟨1, 𝑏⟩} ∈ 𝐸) → 𝑋 = ⟨1, 𝑏⟩))
58	53, 57	biimtrid 242	. . . . . . . . 9 ⊢ (((𝐾 = ⟨0, ((𝑦 + 1) mod 5)⟩ ∧ 𝐿 = ⟨1, 𝑦⟩) ∧ (𝑏 ∈ (0..^5) ∧ 𝑦 ∈ (0..^5))) → (({𝐾, ⟨1, 𝑏⟩} ∈ 𝐸 ∧ {⟨1, 𝑏⟩, 𝐿} ∈ 𝐸) → 𝑋 = ⟨1, 𝑏⟩))
59	58	ex 412	. . . . . . . 8 ⊢ ((𝐾 = ⟨0, ((𝑦 + 1) mod 5)⟩ ∧ 𝐿 = ⟨1, 𝑦⟩) → ((𝑏 ∈ (0..^5) ∧ 𝑦 ∈ (0..^5)) → (({𝐾, ⟨1, 𝑏⟩} ∈ 𝐸 ∧ {⟨1, 𝑏⟩, 𝐿} ∈ 𝐸) → 𝑋 = ⟨1, 𝑏⟩)))
60	59	adantld 490	. . . . . . 7 ⊢ ((𝐾 = ⟨0, ((𝑦 + 1) mod 5)⟩ ∧ 𝐿 = ⟨1, 𝑦⟩) → ((𝐾 ≠ 𝐿 ∧ (𝑏 ∈ (0..^5) ∧ 𝑦 ∈ (0..^5))) → (({𝐾, ⟨1, 𝑏⟩} ∈ 𝐸 ∧ {⟨1, 𝑏⟩, 𝐿} ∈ 𝐸) → 𝑋 = ⟨1, 𝑏⟩)))
61	60	expcom 413	. . . . . 6 ⊢ (𝐿 = ⟨1, 𝑦⟩ → (𝐾 = ⟨0, ((𝑦 + 1) mod 5)⟩ → ((𝐾 ≠ 𝐿 ∧ (𝑏 ∈ (0..^5) ∧ 𝑦 ∈ (0..^5))) → (({𝐾, ⟨1, 𝑏⟩} ∈ 𝐸 ∧ {⟨1, 𝑏⟩, 𝐿} ∈ 𝐸) → 𝑋 = ⟨1, 𝑏⟩))))
62		simpr 484	. . . . . . . . . 10 ⊢ ((𝐿 = ⟨1, 𝑦⟩ ∧ 𝐾 = ⟨1, 𝑦⟩) → 𝐾 = ⟨1, 𝑦⟩)
63		simpl 482	. . . . . . . . . 10 ⊢ ((𝐿 = ⟨1, 𝑦⟩ ∧ 𝐾 = ⟨1, 𝑦⟩) → 𝐿 = ⟨1, 𝑦⟩)
64	62, 63	neeq12d 2990	. . . . . . . . 9 ⊢ ((𝐿 = ⟨1, 𝑦⟩ ∧ 𝐾 = ⟨1, 𝑦⟩) → (𝐾 ≠ 𝐿 ↔ ⟨1, 𝑦⟩ ≠ ⟨1, 𝑦⟩))
65		eqid 2733	. . . . . . . . . 10 ⊢ ⟨1, 𝑦⟩ = ⟨1, 𝑦⟩
66		eqneqall 2940	. . . . . . . . . 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 253	. . . . . . . 8 ⊢ ((𝐿 = ⟨1, 𝑦⟩ ∧ 𝐾 = ⟨1, 𝑦⟩) → (𝐾 ≠ 𝐿 → ((𝑏 ∈ (0..^5) ∧ 𝑦 ∈ (0..^5)) → (({𝐾, ⟨1, 𝑏⟩} ∈ 𝐸 ∧ {⟨1, 𝑏⟩, 𝐿} ∈ 𝐸) → 𝑋 = ⟨1, 𝑏⟩))))
69	68	impd 410	. . . . . . 7 ⊢ ((𝐿 = ⟨1, 𝑦⟩ ∧ 𝐾 = ⟨1, 𝑦⟩) → ((𝐾 ≠ 𝐿 ∧ (𝑏 ∈ (0..^5) ∧ 𝑦 ∈ (0..^5))) → (({𝐾, ⟨1, 𝑏⟩} ∈ 𝐸 ∧ {⟨1, 𝑏⟩, 𝐿} ∈ 𝐸) → 𝑋 = ⟨1, 𝑏⟩)))
70	69	ex 412	. . . . . 6 ⊢ (𝐿 = ⟨1, 𝑦⟩ → (𝐾 = ⟨1, 𝑦⟩ → ((𝐾 ≠ 𝐿 ∧ (𝑏 ∈ (0..^5) ∧ 𝑦 ∈ (0..^5))) → (({𝐾, ⟨1, 𝑏⟩} ∈ 𝐸 ∧ {⟨1, 𝑏⟩, 𝐿} ∈ 𝐸) → 𝑋 = ⟨1, 𝑏⟩))))
71	32, 33, 34, 35	pgnbgreunbgrlem5lem2 48283	. . . . . . . . . . . . 13 ⊢ ((((𝐾 = ⟨0, ((𝑦 − 1) mod 5)⟩ ∧ 𝐿 = ⟨1, 𝑦⟩) ∧ (𝑏 ∈ (0..^5) ∧ 𝑦 ∈ (0..^5))) ∧ {𝐿, ⟨1, 𝑏⟩} ∈ 𝐸) → ¬ {⟨1, 𝑏⟩, 𝐾} ∈ 𝐸)
72	71	pm2.21d 121	. . . . . . . . . . . 12 ⊢ ((((𝐾 = ⟨0, ((𝑦 − 1) mod 5)⟩ ∧ 𝐿 = ⟨1, 𝑦⟩) ∧ (𝑏 ∈ (0..^5) ∧ 𝑦 ∈ (0..^5))) ∧ {𝐿, ⟨1, 𝑏⟩} ∈ 𝐸) → ({⟨1, 𝑏⟩, 𝐾} ∈ 𝐸 → 𝑋 = ⟨1, 𝑏⟩))
73	72	ex 412	. . . . . . . . . . 11 ⊢ (((𝐾 = ⟨0, ((𝑦 − 1) mod 5)⟩ ∧ 𝐿 = ⟨1, 𝑦⟩) ∧ (𝑏 ∈ (0..^5) ∧ 𝑦 ∈ (0..^5))) → ({𝐿, ⟨1, 𝑏⟩} ∈ 𝐸 → ({⟨1, 𝑏⟩, 𝐾} ∈ 𝐸 → 𝑋 = ⟨1, 𝑏⟩)))
74	73	impcomd 411	. . . . . . . . . 10 ⊢ (((𝐾 = ⟨0, ((𝑦 − 1) mod 5)⟩ ∧ 𝐿 = ⟨1, 𝑦⟩) ∧ (𝑏 ∈ (0..^5) ∧ 𝑦 ∈ (0..^5))) → (({⟨1, 𝑏⟩, 𝐾} ∈ 𝐸 ∧ {𝐿, ⟨1, 𝑏⟩} ∈ 𝐸) → 𝑋 = ⟨1, 𝑏⟩))
75	53, 74	biimtrid 242	. . . . . . . . 9 ⊢ (((𝐾 = ⟨0, ((𝑦 − 1) mod 5)⟩ ∧ 𝐿 = ⟨1, 𝑦⟩) ∧ (𝑏 ∈ (0..^5) ∧ 𝑦 ∈ (0..^5))) → (({𝐾, ⟨1, 𝑏⟩} ∈ 𝐸 ∧ {⟨1, 𝑏⟩, 𝐿} ∈ 𝐸) → 𝑋 = ⟨1, 𝑏⟩))
76	75	ex 412	. . . . . . . 8 ⊢ ((𝐾 = ⟨0, ((𝑦 − 1) mod 5)⟩ ∧ 𝐿 = ⟨1, 𝑦⟩) → ((𝑏 ∈ (0..^5) ∧ 𝑦 ∈ (0..^5)) → (({𝐾, ⟨1, 𝑏⟩} ∈ 𝐸 ∧ {⟨1, 𝑏⟩, 𝐿} ∈ 𝐸) → 𝑋 = ⟨1, 𝑏⟩)))
77	76	adantld 490	. . . . . . 7 ⊢ ((𝐾 = ⟨0, ((𝑦 − 1) mod 5)⟩ ∧ 𝐿 = ⟨1, 𝑦⟩) → ((𝐾 ≠ 𝐿 ∧ (𝑏 ∈ (0..^5) ∧ 𝑦 ∈ (0..^5))) → (({𝐾, ⟨1, 𝑏⟩} ∈ 𝐸 ∧ {⟨1, 𝑏⟩, 𝐿} ∈ 𝐸) → 𝑋 = ⟨1, 𝑏⟩)))
78	77	expcom 413	. . . . . 6 ⊢ (𝐿 = ⟨1, 𝑦⟩ → (𝐾 = ⟨0, ((𝑦 − 1) mod 5)⟩ → ((𝐾 ≠ 𝐿 ∧ (𝑏 ∈ (0..^5) ∧ 𝑦 ∈ (0..^5))) → (({𝐾, ⟨1, 𝑏⟩} ∈ 𝐸 ∧ {⟨1, 𝑏⟩, 𝐿} ∈ 𝐸) → 𝑋 = ⟨1, 𝑏⟩))))
79	61, 70, 78	3jaod 1431	. . . . 5 ⊢ (𝐿 = ⟨1, 𝑦⟩ → ((𝐾 = ⟨0, ((𝑦 + 1) mod 5)⟩ ∨ 𝐾 = ⟨1, 𝑦⟩ ∨ 𝐾 = ⟨0, ((𝑦 − 1) mod 5)⟩) → ((𝐾 ≠ 𝐿 ∧ (𝑏 ∈ (0..^5) ∧ 𝑦 ∈ (0..^5))) → (({𝐾, ⟨1, 𝑏⟩} ∈ 𝐸 ∧ {⟨1, 𝑏⟩, 𝐿} ∈ 𝐸) → 𝑋 = ⟨1, 𝑏⟩))))
80	32, 33, 34, 35	pgnbgreunbgrlem5lem3 48284	. . . . . . . . . . . . 13 ⊢ ((((𝐾 = ⟨0, ((𝑦 + 1) mod 5)⟩ ∧ 𝐿 = ⟨0, ((𝑦 − 1) mod 5)⟩) ∧ (𝑏 ∈ (0..^5) ∧ 𝑦 ∈ (0..^5))) ∧ {𝐿, ⟨1, 𝑏⟩} ∈ 𝐸) → ¬ {⟨1, 𝑏⟩, 𝐾} ∈ 𝐸)
81	80	pm2.21d 121	. . . . . . . . . . . 12 ⊢ ((((𝐾 = ⟨0, ((𝑦 + 1) mod 5)⟩ ∧ 𝐿 = ⟨0, ((𝑦 − 1) mod 5)⟩) ∧ (𝑏 ∈ (0..^5) ∧ 𝑦 ∈ (0..^5))) ∧ {𝐿, ⟨1, 𝑏⟩} ∈ 𝐸) → ({⟨1, 𝑏⟩, 𝐾} ∈ 𝐸 → 𝑋 = ⟨1, 𝑏⟩))
82	81	ex 412	. . . . . . . . . . 11 ⊢ (((𝐾 = ⟨0, ((𝑦 + 1) mod 5)⟩ ∧ 𝐿 = ⟨0, ((𝑦 − 1) mod 5)⟩) ∧ (𝑏 ∈ (0..^5) ∧ 𝑦 ∈ (0..^5))) → ({𝐿, ⟨1, 𝑏⟩} ∈ 𝐸 → ({⟨1, 𝑏⟩, 𝐾} ∈ 𝐸 → 𝑋 = ⟨1, 𝑏⟩)))
83	82	impcomd 411	. . . . . . . . . 10 ⊢ (((𝐾 = ⟨0, ((𝑦 + 1) mod 5)⟩ ∧ 𝐿 = ⟨0, ((𝑦 − 1) mod 5)⟩) ∧ (𝑏 ∈ (0..^5) ∧ 𝑦 ∈ (0..^5))) → (({⟨1, 𝑏⟩, 𝐾} ∈ 𝐸 ∧ {𝐿, ⟨1, 𝑏⟩} ∈ 𝐸) → 𝑋 = ⟨1, 𝑏⟩))
84	53, 83	biimtrid 242	. . . . . . . . 9 ⊢ (((𝐾 = ⟨0, ((𝑦 + 1) mod 5)⟩ ∧ 𝐿 = ⟨0, ((𝑦 − 1) mod 5)⟩) ∧ (𝑏 ∈ (0..^5) ∧ 𝑦 ∈ (0..^5))) → (({𝐾, ⟨1, 𝑏⟩} ∈ 𝐸 ∧ {⟨1, 𝑏⟩, 𝐿} ∈ 𝐸) → 𝑋 = ⟨1, 𝑏⟩))
85	84	ex 412	. . . . . . . 8 ⊢ ((𝐾 = ⟨0, ((𝑦 + 1) mod 5)⟩ ∧ 𝐿 = ⟨0, ((𝑦 − 1) mod 5)⟩) → ((𝑏 ∈ (0..^5) ∧ 𝑦 ∈ (0..^5)) → (({𝐾, ⟨1, 𝑏⟩} ∈ 𝐸 ∧ {⟨1, 𝑏⟩, 𝐿} ∈ 𝐸) → 𝑋 = ⟨1, 𝑏⟩)))
86	85	adantld 490	. . . . . . 7 ⊢ ((𝐾 = ⟨0, ((𝑦 + 1) mod 5)⟩ ∧ 𝐿 = ⟨0, ((𝑦 − 1) mod 5)⟩) → ((𝐾 ≠ 𝐿 ∧ (𝑏 ∈ (0..^5) ∧ 𝑦 ∈ (0..^5))) → (({𝐾, ⟨1, 𝑏⟩} ∈ 𝐸 ∧ {⟨1, 𝑏⟩, 𝐿} ∈ 𝐸) → 𝑋 = ⟨1, 𝑏⟩)))
87	86	expcom 413	. . . . . 6 ⊢ (𝐿 = ⟨0, ((𝑦 − 1) mod 5)⟩ → (𝐾 = ⟨0, ((𝑦 + 1) mod 5)⟩ → ((𝐾 ≠ 𝐿 ∧ (𝑏 ∈ (0..^5) ∧ 𝑦 ∈ (0..^5))) → (({𝐾, ⟨1, 𝑏⟩} ∈ 𝐸 ∧ {⟨1, 𝑏⟩, 𝐿} ∈ 𝐸) → 𝑋 = ⟨1, 𝑏⟩))))
88	32, 33, 34, 35	pgnbgreunbgrlem5lem2 48283	. . . . . . . . . . 11 ⊢ ((((𝐿 = ⟨0, ((𝑦 − 1) mod 5)⟩ ∧ 𝐾 = ⟨1, 𝑦⟩) ∧ (𝑏 ∈ (0..^5) ∧ 𝑦 ∈ (0..^5))) ∧ {𝐾, ⟨1, 𝑏⟩} ∈ 𝐸) → ¬ {⟨1, 𝑏⟩, 𝐿} ∈ 𝐸)
89	88	pm2.21d 121	. . . . . . . . . 10 ⊢ ((((𝐿 = ⟨0, ((𝑦 − 1) mod 5)⟩ ∧ 𝐾 = ⟨1, 𝑦⟩) ∧ (𝑏 ∈ (0..^5) ∧ 𝑦 ∈ (0..^5))) ∧ {𝐾, ⟨1, 𝑏⟩} ∈ 𝐸) → ({⟨1, 𝑏⟩, 𝐿} ∈ 𝐸 → 𝑋 = ⟨1, 𝑏⟩))
90	89	expimpd 453	. . . . . . . . 9 ⊢ (((𝐿 = ⟨0, ((𝑦 − 1) mod 5)⟩ ∧ 𝐾 = ⟨1, 𝑦⟩) ∧ (𝑏 ∈ (0..^5) ∧ 𝑦 ∈ (0..^5))) → (({𝐾, ⟨1, 𝑏⟩} ∈ 𝐸 ∧ {⟨1, 𝑏⟩, 𝐿} ∈ 𝐸) → 𝑋 = ⟨1, 𝑏⟩))
91	90	ex 412	. . . . . . . 8 ⊢ ((𝐿 = ⟨0, ((𝑦 − 1) mod 5)⟩ ∧ 𝐾 = ⟨1, 𝑦⟩) → ((𝑏 ∈ (0..^5) ∧ 𝑦 ∈ (0..^5)) → (({𝐾, ⟨1, 𝑏⟩} ∈ 𝐸 ∧ {⟨1, 𝑏⟩, 𝐿} ∈ 𝐸) → 𝑋 = ⟨1, 𝑏⟩)))
92	91	adantld 490	. . . . . . 7 ⊢ ((𝐿 = ⟨0, ((𝑦 − 1) mod 5)⟩ ∧ 𝐾 = ⟨1, 𝑦⟩) → ((𝐾 ≠ 𝐿 ∧ (𝑏 ∈ (0..^5) ∧ 𝑦 ∈ (0..^5))) → (({𝐾, ⟨1, 𝑏⟩} ∈ 𝐸 ∧ {⟨1, 𝑏⟩, 𝐿} ∈ 𝐸) → 𝑋 = ⟨1, 𝑏⟩)))
93	92	ex 412	. . . . . 6 ⊢ (𝐿 = ⟨0, ((𝑦 − 1) mod 5)⟩ → (𝐾 = ⟨1, 𝑦⟩ → ((𝐾 ≠ 𝐿 ∧ (𝑏 ∈ (0..^5) ∧ 𝑦 ∈ (0..^5))) → (({𝐾, ⟨1, 𝑏⟩} ∈ 𝐸 ∧ {⟨1, 𝑏⟩, 𝐿} ∈ 𝐸) → 𝑋 = ⟨1, 𝑏⟩))))
94		simpr 484	. . . . . . . . . 10 ⊢ ((𝐿 = ⟨0, ((𝑦 − 1) mod 5)⟩ ∧ 𝐾 = ⟨0, ((𝑦 − 1) mod 5)⟩) → 𝐾 = ⟨0, ((𝑦 − 1) mod 5)⟩)
95		simpl 482	. . . . . . . . . 10 ⊢ ((𝐿 = ⟨0, ((𝑦 − 1) mod 5)⟩ ∧ 𝐾 = ⟨0, ((𝑦 − 1) mod 5)⟩) → 𝐿 = ⟨0, ((𝑦 − 1) mod 5)⟩)
96	94, 95	neeq12d 2990	. . . . . . . . 9 ⊢ ((𝐿 = ⟨0, ((𝑦 − 1) mod 5)⟩ ∧ 𝐾 = ⟨0, ((𝑦 − 1) mod 5)⟩) → (𝐾 ≠ 𝐿 ↔ ⟨0, ((𝑦 − 1) mod 5)⟩ ≠ ⟨0, ((𝑦 − 1) mod 5)⟩))
97		eqid 2733	. . . . . . . . . 10 ⊢ ⟨0, ((𝑦 − 1) mod 5)⟩ = ⟨0, ((𝑦 − 1) mod 5)⟩
98		eqneqall 2940	. . . . . . . . . 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 253	. . . . . . . 8 ⊢ ((𝐿 = ⟨0, ((𝑦 − 1) mod 5)⟩ ∧ 𝐾 = ⟨0, ((𝑦 − 1) mod 5)⟩) → (𝐾 ≠ 𝐿 → ((𝑏 ∈ (0..^5) ∧ 𝑦 ∈ (0..^5)) → (({𝐾, ⟨1, 𝑏⟩} ∈ 𝐸 ∧ {⟨1, 𝑏⟩, 𝐿} ∈ 𝐸) → 𝑋 = ⟨1, 𝑏⟩))))
101	100	impd 410	. . . . . . 7 ⊢ ((𝐿 = ⟨0, ((𝑦 − 1) mod 5)⟩ ∧ 𝐾 = ⟨0, ((𝑦 − 1) mod 5)⟩) → ((𝐾 ≠ 𝐿 ∧ (𝑏 ∈ (0..^5) ∧ 𝑦 ∈ (0..^5))) → (({𝐾, ⟨1, 𝑏⟩} ∈ 𝐸 ∧ {⟨1, 𝑏⟩, 𝐿} ∈ 𝐸) → 𝑋 = ⟨1, 𝑏⟩)))
102	101	ex 412	. . . . . 6 ⊢ (𝐿 = ⟨0, ((𝑦 − 1) mod 5)⟩ → (𝐾 = ⟨0, ((𝑦 − 1) mod 5)⟩ → ((𝐾 ≠ 𝐿 ∧ (𝑏 ∈ (0..^5) ∧ 𝑦 ∈ (0..^5))) → (({𝐾, ⟨1, 𝑏⟩} ∈ 𝐸 ∧ {⟨1, 𝑏⟩, 𝐿} ∈ 𝐸) → 𝑋 = ⟨1, 𝑏⟩))))
103	87, 93, 102	3jaod 1431	. . . . 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 1430	. . . 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 406	. . 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 253	. 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 414	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 206 ∧ wa 395 ∨ w3o 1085 = wceq 1541 ∈ wcel 2113 ≠ wne 2929 {cpr 4579 ⟨cop 4583 ‘cfv 6489 (class class class)co 7355 2^nd c2nd 7929 0cc0 11017 1c1 11018 + caddc 11020 − cmin 11355 2c2 12191 5c5 12194 ..^cfzo 13561 mod cmo 13780 Vtxcvtx 28995 Edgcedg 29046 NeighbVtx cnbgr 29331 gPetersenGr cgpg 48202

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1968 ax-7 2009 ax-8 2115 ax-9 2123 ax-10 2146 ax-11 2162 ax-12 2182 ax-ext 2705 ax-rep 5221 ax-sep 5238 ax-nul 5248 ax-pow 5307 ax-pr 5374 ax-un 7677 ax-cnex 11073 ax-resscn 11074 ax-1cn 11075 ax-icn 11076 ax-addcl 11077 ax-addrcl 11078 ax-mulcl 11079 ax-mulrcl 11080 ax-mulcom 11081 ax-addass 11082 ax-mulass 11083 ax-distr 11084 ax-i2m1 11085 ax-1ne0 11086 ax-1rid 11087 ax-rnegex 11088 ax-rrecex 11089 ax-cnre 11090 ax-pre-lttri 11091 ax-pre-lttrn 11092 ax-pre-ltadd 11093 ax-pre-mulgt0 11094 ax-pre-sup 11095

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1544 df-fal 1554 df-ex 1781 df-nf 1785 df-sb 2068 df-mo 2537 df-eu 2566 df-clab 2712 df-cleq 2725 df-clel 2808 df-nfc 2882 df-ne 2930 df-nel 3034 df-ral 3049 df-rex 3058 df-rmo 3347 df-reu 3348 df-rab 3397 df-v 3439 df-sbc 3738 df-csb 3847 df-dif 3901 df-un 3903 df-in 3905 df-ss 3915 df-pss 3918 df-nul 4283 df-if 4477 df-pw 4553 df-sn 4578 df-pr 4580 df-op 4584 df-uni 4861 df-int 4900 df-iun 4945 df-br 5096 df-opab 5158 df-mpt 5177 df-tr 5203 df-id 5516 df-eprel 5521 df-po 5529 df-so 5530 df-fr 5574 df-we 5576 df-xp 5627 df-rel 5628 df-cnv 5629 df-co 5630 df-dm 5631 df-rn 5632 df-res 5633 df-ima 5634 df-pred 6256 df-ord 6317 df-on 6318 df-lim 6319 df-suc 6320 df-iota 6445 df-fun 6491 df-fn 6492 df-f 6493 df-f1 6494 df-fo 6495 df-f1o 6496 df-fv 6497 df-riota 7312 df-ov 7358 df-oprab 7359 df-mpo 7360 df-om 7806 df-1st 7930 df-2nd 7931 df-frecs 8220 df-wrecs 8251 df-recs 8300 df-rdg 8338 df-1o 8394 df-oadd 8398 df-er 8631 df-en 8880 df-dom 8881 df-sdom 8882 df-fin 8883 df-sup 9337 df-inf 9338 df-dju 9805 df-card 9843 df-pnf 11159 df-mnf 11160 df-xr 11161 df-ltxr 11162 df-le 11163 df-sub 11357 df-neg 11358 df-div 11786 df-nn 12137 df-2 12199 df-3 12200 df-4 12201 df-5 12202 df-6 12203 df-7 12204 df-8 12205 df-9 12206 df-n0 12393 df-xnn0 12466 df-z 12480 df-dec 12599 df-uz 12743 df-rp 12897 df-ico 13258 df-fz 13415 df-fzo 13562 df-fl 13703 df-ceil 13704 df-mod 13781 df-seq 13916 df-exp 13976 df-hash 14245 df-cj 15013 df-re 15014 df-im 15015 df-sqrt 15149 df-abs 15150 df-dvds 16171 df-struct 17065 df-slot 17100 df-ndx 17112 df-base 17128 df-edgf 28988 df-vtx 28997 df-iedg 28998 df-edg 29047 df-umgr 29082 df-usgr 29150 df-gpg 48203

This theorem is referenced by: pgnbgreunbgrlem6 48286

W3C validator