Metamath Proof Explorer

Theorem pgnbgreunbgrlem5

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

Ref Expression
Hypotheses pgnbgreunbgr.g ⊢ 𝐺 = ( 5 gPetersenGr 2 )
pgnbgreunbgr.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
pgnbgreunbgr.e ⊢ 𝐸 = ( Edg ‘ 𝐺 )
pgnbgreunbgr.n ⊢ 𝑁 = ( 𝐺 NeighbVtx 𝑋 )
Assertion pgnbgreunbgrlem5 ( ( 𝐿 = ⟨ 0 , ( ( ( 2nd ‘ 𝑋 ) + 1 ) mod 5 ) ⟩ ∨ 𝐿 = ⟨ 1 , ( 2nd ‘ 𝑋 ) ⟩ ∨ 𝐿 = ⟨ 0 , ( ( ( 2nd ‘ 𝑋 ) − 1 ) mod 5 ) ⟩ ) → ( ( 𝐾 = ⟨ 0 , ( ( ( 2nd ‘ 𝑋 ) + 1 ) mod 5 ) ⟩ ∨ 𝐾 = ⟨ 1 , ( 2nd ‘ 𝑋 ) ⟩ ∨ 𝐾 = ⟨ 0 , ( ( ( 2nd ‘ 𝑋 ) − 1 ) mod 5 ) ⟩ ) → ( ( 𝑋 = ⟨ 0 , 𝑦 ⟩ ∧ 𝑋 ∈ 𝑉 ) → ( ( 𝐾 ≠ 𝐿 ∧ ( 𝑏 ∈ ( 0 ..^ 5 ) ∧ 𝑦 ∈ ( 0 ..^ 5 ) ) ) → ( ( { 𝐾 , ⟨ 1 , 𝑏 ⟩ } ∈ 𝐸 ∧ { ⟨ 1 , 𝑏 ⟩ , 𝐿 } ∈ 𝐸 ) → 𝑋 = ⟨ 1 , 𝑏 ⟩ ) ) ) ) )

Proof

Step Hyp Ref Expression
1 pgnbgreunbgr.g ⊢ 𝐺 = ( 5 gPetersenGr 2 )
2 pgnbgreunbgr.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
3 pgnbgreunbgr.e ⊢ 𝐸 = ( Edg ‘ 𝐺 )
4 pgnbgreunbgr.n ⊢ 𝑁 = ( 𝐺 NeighbVtx 𝑋 )
5 c0ex ⊢ 0 ∈ V
6 vex ⊢ 𝑦 ∈ V
7 5 6 op2ndd ⊢ ( 𝑋 = ⟨ 0 , 𝑦 ⟩ → ( 2nd ‘ 𝑋 ) = 𝑦 )
8 7 adantr ⊢ ( ( 𝑋 = ⟨ 0 , 𝑦 ⟩ ∧ 𝑋 ∈ 𝑉 ) → ( 2nd ‘ 𝑋 ) = 𝑦 )
9 oveq1 ⊢ ( ( 2nd ‘ 𝑋 ) = 𝑦 → ( ( 2nd ‘ 𝑋 ) + 1 ) = ( 𝑦 + 1 ) )
10 9 oveq1d ⊢ ( ( 2nd ‘ 𝑋 ) = 𝑦 → ( ( ( 2nd ‘ 𝑋 ) + 1 ) mod 5 ) = ( ( 𝑦 + 1 ) mod 5 ) )
11 10 opeq2d ⊢ ( ( 2nd ‘ 𝑋 ) = 𝑦 → ⟨ 0 , ( ( ( 2nd ‘ 𝑋 ) + 1 ) mod 5 ) ⟩ = ⟨ 0 , ( ( 𝑦 + 1 ) mod 5 ) ⟩ )
12 11 eqeq2d ⊢ ( ( 2nd ‘ 𝑋 ) = 𝑦 → ( 𝐿 = ⟨ 0 , ( ( ( 2nd ‘ 𝑋 ) + 1 ) mod 5 ) ⟩ ↔ 𝐿 = ⟨ 0 , ( ( 𝑦 + 1 ) mod 5 ) ⟩ ) )
13 opeq2 ⊢ ( ( 2nd ‘ 𝑋 ) = 𝑦 → ⟨ 1 , ( 2nd ‘ 𝑋 ) ⟩ = ⟨ 1 , 𝑦 ⟩ )
14 13 eqeq2d ⊢ ( ( 2nd ‘ 𝑋 ) = 𝑦 → ( 𝐿 = ⟨ 1 , ( 2nd ‘ 𝑋 ) ⟩ ↔ 𝐿 = ⟨ 1 , 𝑦 ⟩ ) )
15 oveq1 ⊢ ( ( 2nd ‘ 𝑋 ) = 𝑦 → ( ( 2nd ‘ 𝑋 ) − 1 ) = ( 𝑦 − 1 ) )
16 15 oveq1d ⊢ ( ( 2nd ‘ 𝑋 ) = 𝑦 → ( ( ( 2nd ‘ 𝑋 ) − 1 ) mod 5 ) = ( ( 𝑦 − 1 ) mod 5 ) )
17 16 opeq2d ⊢ ( ( 2nd ‘ 𝑋 ) = 𝑦 → ⟨ 0 , ( ( ( 2nd ‘ 𝑋 ) − 1 ) mod 5 ) ⟩ = ⟨ 0 , ( ( 𝑦 − 1 ) mod 5 ) ⟩ )
18 17 eqeq2d ⊢ ( ( 2nd ‘ 𝑋 ) = 𝑦 → ( 𝐿 = ⟨ 0 , ( ( ( 2nd ‘ 𝑋 ) − 1 ) mod 5 ) ⟩ ↔ 𝐿 = ⟨ 0 , ( ( 𝑦 − 1 ) mod 5 ) ⟩ ) )
19 12 14 18 3orbi123d ⊢ ( ( 2nd ‘ 𝑋 ) = 𝑦 → ( ( 𝐿 = ⟨ 0 , ( ( ( 2nd ‘ 𝑋 ) + 1 ) mod 5 ) ⟩ ∨ 𝐿 = ⟨ 1 , ( 2nd ‘ 𝑋 ) ⟩ ∨ 𝐿 = ⟨ 0 , ( ( ( 2nd ‘ 𝑋 ) − 1 ) mod 5 ) ⟩ ) ↔ ( 𝐿 = ⟨ 0 , ( ( 𝑦 + 1 ) mod 5 ) ⟩ ∨ 𝐿 = ⟨ 1 , 𝑦 ⟩ ∨ 𝐿 = ⟨ 0 , ( ( 𝑦 − 1 ) mod 5 ) ⟩ ) ) )
20 11 eqeq2d ⊢ ( ( 2nd ‘ 𝑋 ) = 𝑦 → ( 𝐾 = ⟨ 0 , ( ( ( 2nd ‘ 𝑋 ) + 1 ) mod 5 ) ⟩ ↔ 𝐾 = ⟨ 0 , ( ( 𝑦 + 1 ) mod 5 ) ⟩ ) )
21 13 eqeq2d ⊢ ( ( 2nd ‘ 𝑋 ) = 𝑦 → ( 𝐾 = ⟨ 1 , ( 2nd ‘ 𝑋 ) ⟩ ↔ 𝐾 = ⟨ 1 , 𝑦 ⟩ ) )
22 17 eqeq2d ⊢ ( ( 2nd ‘ 𝑋 ) = 𝑦 → ( 𝐾 = ⟨ 0 , ( ( ( 2nd ‘ 𝑋 ) − 1 ) mod 5 ) ⟩ ↔ 𝐾 = ⟨ 0 , ( ( 𝑦 − 1 ) mod 5 ) ⟩ ) )
23 20 21 22 3orbi123d ⊢ ( ( 2nd ‘ 𝑋 ) = 𝑦 → ( ( 𝐾 = ⟨ 0 , ( ( ( 2nd ‘ 𝑋 ) + 1 ) mod 5 ) ⟩ ∨ 𝐾 = ⟨ 1 , ( 2nd ‘ 𝑋 ) ⟩ ∨ 𝐾 = ⟨ 0 , ( ( ( 2nd ‘ 𝑋 ) − 1 ) mod 5 ) ⟩ ) ↔ ( 𝐾 = ⟨ 0 , ( ( 𝑦 + 1 ) mod 5 ) ⟩ ∨ 𝐾 = ⟨ 1 , 𝑦 ⟩ ∨ 𝐾 = ⟨ 0 , ( ( 𝑦 − 1 ) mod 5 ) ⟩ ) ) )
24 19 23 anbi12d ⊢ ( ( 2nd ‘ 𝑋 ) = 𝑦 → ( ( ( 𝐿 = ⟨ 0 , ( ( ( 2nd ‘ 𝑋 ) + 1 ) mod 5 ) ⟩ ∨ 𝐿 = ⟨ 1 , ( 2nd ‘ 𝑋 ) ⟩ ∨ 𝐿 = ⟨ 0 , ( ( ( 2nd ‘ 𝑋 ) − 1 ) mod 5 ) ⟩ ) ∧ ( 𝐾 = ⟨ 0 , ( ( ( 2nd ‘ 𝑋 ) + 1 ) mod 5 ) ⟩ ∨ 𝐾 = ⟨ 1 , ( 2nd ‘ 𝑋 ) ⟩ ∨ 𝐾 = ⟨ 0 , ( ( ( 2nd ‘ 𝑋 ) − 1 ) mod 5 ) ⟩ ) ) ↔ ( ( 𝐿 = ⟨ 0 , ( ( 𝑦 + 1 ) mod 5 ) ⟩ ∨ 𝐿 = ⟨ 1 , 𝑦 ⟩ ∨ 𝐿 = ⟨ 0 , ( ( 𝑦 − 1 ) mod 5 ) ⟩ ) ∧ ( 𝐾 = ⟨ 0 , ( ( 𝑦 + 1 ) mod 5 ) ⟩ ∨ 𝐾 = ⟨ 1 , 𝑦 ⟩ ∨ 𝐾 = ⟨ 0 , ( ( 𝑦 − 1 ) mod 5 ) ⟩ ) ) ) )
25 8 24 syl ⊢ ( ( 𝑋 = ⟨ 0 , 𝑦 ⟩ ∧ 𝑋 ∈ 𝑉 ) → ( ( ( 𝐿 = ⟨ 0 , ( ( ( 2nd ‘ 𝑋 ) + 1 ) mod 5 ) ⟩ ∨ 𝐿 = ⟨ 1 , ( 2nd ‘ 𝑋 ) ⟩ ∨ 𝐿 = ⟨ 0 , ( ( ( 2nd ‘ 𝑋 ) − 1 ) mod 5 ) ⟩ ) ∧ ( 𝐾 = ⟨ 0 , ( ( ( 2nd ‘ 𝑋 ) + 1 ) mod 5 ) ⟩ ∨ 𝐾 = ⟨ 1 , ( 2nd ‘ 𝑋 ) ⟩ ∨ 𝐾 = ⟨ 0 , ( ( ( 2nd ‘ 𝑋 ) − 1 ) mod 5 ) ⟩ ) ) ↔ ( ( 𝐿 = ⟨ 0 , ( ( 𝑦 + 1 ) mod 5 ) ⟩ ∨ 𝐿 = ⟨ 1 , 𝑦 ⟩ ∨ 𝐿 = ⟨ 0 , ( ( 𝑦 − 1 ) mod 5 ) ⟩ ) ∧ ( 𝐾 = ⟨ 0 , ( ( 𝑦 + 1 ) mod 5 ) ⟩ ∨ 𝐾 = ⟨ 1 , 𝑦 ⟩ ∨ 𝐾 = ⟨ 0 , ( ( 𝑦 − 1 ) mod 5 ) ⟩ ) ) ) )
26 simpl ⊢ ( ( 𝐾 = ⟨ 0 , ( ( 𝑦 + 1 ) mod 5 ) ⟩ ∧ 𝐿 = ⟨ 0 , ( ( 𝑦 + 1 ) mod 5 ) ⟩ ) → 𝐾 = ⟨ 0 , ( ( 𝑦 + 1 ) mod 5 ) ⟩ )
27 simpr ⊢ ( ( 𝐾 = ⟨ 0 , ( ( 𝑦 + 1 ) mod 5 ) ⟩ ∧ 𝐿 = ⟨ 0 , ( ( 𝑦 + 1 ) mod 5 ) ⟩ ) → 𝐿 = ⟨ 0 , ( ( 𝑦 + 1 ) mod 5 ) ⟩ )
28 26 27 neeq12d ⊢ ( ( 𝐾 = ⟨ 0 , ( ( 𝑦 + 1 ) mod 5 ) ⟩ ∧ 𝐿 = ⟨ 0 , ( ( 𝑦 + 1 ) mod 5 ) ⟩ ) → ( 𝐾 ≠ 𝐿 ↔ ⟨ 0 , ( ( 𝑦 + 1 ) mod 5 ) ⟩ ≠ ⟨ 0 , ( ( 𝑦 + 1 ) mod 5 ) ⟩ ) )
29 28 ancoms ⊢ ( ( 𝐿 = ⟨ 0 , ( ( 𝑦 + 1 ) mod 5 ) ⟩ ∧ 𝐾 = ⟨ 0 , ( ( 𝑦 + 1 ) mod 5 ) ⟩ ) → ( 𝐾 ≠ 𝐿 ↔ ⟨ 0 , ( ( 𝑦 + 1 ) mod 5 ) ⟩ ≠ ⟨ 0 , ( ( 𝑦 + 1 ) mod 5 ) ⟩ ) )
30 eqid ⊢ ⟨ 0 , ( ( 𝑦 + 1 ) mod 5 ) ⟩ = ⟨ 0 , ( ( 𝑦 + 1 ) mod 5 ) ⟩
31 eqneqall ⊢ ( ⟨ 0 , ( ( 𝑦 + 1 ) mod 5 ) ⟩ = ⟨ 0 , ( ( 𝑦 + 1 ) mod 5 ) ⟩ → ( ⟨ 0 , ( ( 𝑦 + 1 ) mod 5 ) ⟩ ≠ ⟨ 0 , ( ( 𝑦 + 1 ) mod 5 ) ⟩ → ( ( 𝑏 ∈ ( 0 ..^ 5 ) ∧ 𝑦 ∈ ( 0 ..^ 5 ) ) → ( ( { 𝐾 , ⟨ 1 , 𝑏 ⟩ } ∈ 𝐸 ∧ { ⟨ 1 , 𝑏 ⟩ , 𝐿 } ∈ 𝐸 ) → 𝑋 = ⟨ 1 , 𝑏 ⟩ ) ) ) )
32 30 31 ax-mp ⊢ ( ⟨ 0 , ( ( 𝑦 + 1 ) mod 5 ) ⟩ ≠ ⟨ 0 , ( ( 𝑦 + 1 ) mod 5 ) ⟩ → ( ( 𝑏 ∈ ( 0 ..^ 5 ) ∧ 𝑦 ∈ ( 0 ..^ 5 ) ) → ( ( { 𝐾 , ⟨ 1 , 𝑏 ⟩ } ∈ 𝐸 ∧ { ⟨ 1 , 𝑏 ⟩ , 𝐿 } ∈ 𝐸 ) → 𝑋 = ⟨ 1 , 𝑏 ⟩ ) ) )
33 29 32 biimtrdi ⊢ ( ( 𝐿 = ⟨ 0 , ( ( 𝑦 + 1 ) mod 5 ) ⟩ ∧ 𝐾 = ⟨ 0 , ( ( 𝑦 + 1 ) mod 5 ) ⟩ ) → ( 𝐾 ≠ 𝐿 → ( ( 𝑏 ∈ ( 0 ..^ 5 ) ∧ 𝑦 ∈ ( 0 ..^ 5 ) ) → ( ( { 𝐾 , ⟨ 1 , 𝑏 ⟩ } ∈ 𝐸 ∧ { ⟨ 1 , 𝑏 ⟩ , 𝐿 } ∈ 𝐸 ) → 𝑋 = ⟨ 1 , 𝑏 ⟩ ) ) ) )
34 33 impd ⊢ ( ( 𝐿 = ⟨ 0 , ( ( 𝑦 + 1 ) mod 5 ) ⟩ ∧ 𝐾 = ⟨ 0 , ( ( 𝑦 + 1 ) mod 5 ) ⟩ ) → ( ( 𝐾 ≠ 𝐿 ∧ ( 𝑏 ∈ ( 0 ..^ 5 ) ∧ 𝑦 ∈ ( 0 ..^ 5 ) ) ) → ( ( { 𝐾 , ⟨ 1 , 𝑏 ⟩ } ∈ 𝐸 ∧ { ⟨ 1 , 𝑏 ⟩ , 𝐿 } ∈ 𝐸 ) → 𝑋 = ⟨ 1 , 𝑏 ⟩ ) ) )
35 34 ex ⊢ ( 𝐿 = ⟨ 0 , ( ( 𝑦 + 1 ) mod 5 ) ⟩ → ( 𝐾 = ⟨ 0 , ( ( 𝑦 + 1 ) mod 5 ) ⟩ → ( ( 𝐾 ≠ 𝐿 ∧ ( 𝑏 ∈ ( 0 ..^ 5 ) ∧ 𝑦 ∈ ( 0 ..^ 5 ) ) ) → ( ( { 𝐾 , ⟨ 1 , 𝑏 ⟩ } ∈ 𝐸 ∧ { ⟨ 1 , 𝑏 ⟩ , 𝐿 } ∈ 𝐸 ) → 𝑋 = ⟨ 1 , 𝑏 ⟩ ) ) ) )
36 1 2 3 4 pgnbgreunbgrlem5lem1 ⊢ ( ( ( ( 𝐿 = ⟨ 0 , ( ( 𝑦 + 1 ) mod 5 ) ⟩ ∧ 𝐾 = ⟨ 1 , 𝑦 ⟩ ) ∧ ( 𝑏 ∈ ( 0 ..^ 5 ) ∧ 𝑦 ∈ ( 0 ..^ 5 ) ) ) ∧ { 𝐾 , ⟨ 1 , 𝑏 ⟩ } ∈ 𝐸 ) → ¬ { ⟨ 1 , 𝑏 ⟩ , 𝐿 } ∈ 𝐸 )
37 36 pm2.21d ⊢ ( ( ( ( 𝐿 = ⟨ 0 , ( ( 𝑦 + 1 ) mod 5 ) ⟩ ∧ 𝐾 = ⟨ 1 , 𝑦 ⟩ ) ∧ ( 𝑏 ∈ ( 0 ..^ 5 ) ∧ 𝑦 ∈ ( 0 ..^ 5 ) ) ) ∧ { 𝐾 , ⟨ 1 , 𝑏 ⟩ } ∈ 𝐸 ) → ( { ⟨ 1 , 𝑏 ⟩ , 𝐿 } ∈ 𝐸 → 𝑋 = ⟨ 1 , 𝑏 ⟩ ) )
38 37 expimpd ⊢ ( ( ( 𝐿 = ⟨ 0 , ( ( 𝑦 + 1 ) mod 5 ) ⟩ ∧ 𝐾 = ⟨ 1 , 𝑦 ⟩ ) ∧ ( 𝑏 ∈ ( 0 ..^ 5 ) ∧ 𝑦 ∈ ( 0 ..^ 5 ) ) ) → ( ( { 𝐾 , ⟨ 1 , 𝑏 ⟩ } ∈ 𝐸 ∧ { ⟨ 1 , 𝑏 ⟩ , 𝐿 } ∈ 𝐸 ) → 𝑋 = ⟨ 1 , 𝑏 ⟩ ) )
39 38 ex ⊢ ( ( 𝐿 = ⟨ 0 , ( ( 𝑦 + 1 ) mod 5 ) ⟩ ∧ 𝐾 = ⟨ 1 , 𝑦 ⟩ ) → ( ( 𝑏 ∈ ( 0 ..^ 5 ) ∧ 𝑦 ∈ ( 0 ..^ 5 ) ) → ( ( { 𝐾 , ⟨ 1 , 𝑏 ⟩ } ∈ 𝐸 ∧ { ⟨ 1 , 𝑏 ⟩ , 𝐿 } ∈ 𝐸 ) → 𝑋 = ⟨ 1 , 𝑏 ⟩ ) ) )
40 39 adantld ⊢ ( ( 𝐿 = ⟨ 0 , ( ( 𝑦 + 1 ) mod 5 ) ⟩ ∧ 𝐾 = ⟨ 1 , 𝑦 ⟩ ) → ( ( 𝐾 ≠ 𝐿 ∧ ( 𝑏 ∈ ( 0 ..^ 5 ) ∧ 𝑦 ∈ ( 0 ..^ 5 ) ) ) → ( ( { 𝐾 , ⟨ 1 , 𝑏 ⟩ } ∈ 𝐸 ∧ { ⟨ 1 , 𝑏 ⟩ , 𝐿 } ∈ 𝐸 ) → 𝑋 = ⟨ 1 , 𝑏 ⟩ ) ) )
41 40 ex ⊢ ( 𝐿 = ⟨ 0 , ( ( 𝑦 + 1 ) mod 5 ) ⟩ → ( 𝐾 = ⟨ 1 , 𝑦 ⟩ → ( ( 𝐾 ≠ 𝐿 ∧ ( 𝑏 ∈ ( 0 ..^ 5 ) ∧ 𝑦 ∈ ( 0 ..^ 5 ) ) ) → ( ( { 𝐾 , ⟨ 1 , 𝑏 ⟩ } ∈ 𝐸 ∧ { ⟨ 1 , 𝑏 ⟩ , 𝐿 } ∈ 𝐸 ) → 𝑋 = ⟨ 1 , 𝑏 ⟩ ) ) ) )
42 1 2 3 4 pgnbgreunbgrlem5lem3 ⊢ ( ( ( ( 𝐿 = ⟨ 0 , ( ( 𝑦 + 1 ) mod 5 ) ⟩ ∧ 𝐾 = ⟨ 0 , ( ( 𝑦 − 1 ) mod 5 ) ⟩ ) ∧ ( 𝑏 ∈ ( 0 ..^ 5 ) ∧ 𝑦 ∈ ( 0 ..^ 5 ) ) ) ∧ { 𝐾 , ⟨ 1 , 𝑏 ⟩ } ∈ 𝐸 ) → ¬ { ⟨ 1 , 𝑏 ⟩ , 𝐿 } ∈ 𝐸 )
43 42 pm2.21d ⊢ ( ( ( ( 𝐿 = ⟨ 0 , ( ( 𝑦 + 1 ) mod 5 ) ⟩ ∧ 𝐾 = ⟨ 0 , ( ( 𝑦 − 1 ) mod 5 ) ⟩ ) ∧ ( 𝑏 ∈ ( 0 ..^ 5 ) ∧ 𝑦 ∈ ( 0 ..^ 5 ) ) ) ∧ { 𝐾 , ⟨ 1 , 𝑏 ⟩ } ∈ 𝐸 ) → ( { ⟨ 1 , 𝑏 ⟩ , 𝐿 } ∈ 𝐸 → 𝑋 = ⟨ 1 , 𝑏 ⟩ ) )
44 43 expimpd ⊢ ( ( ( 𝐿 = ⟨ 0 , ( ( 𝑦 + 1 ) mod 5 ) ⟩ ∧ 𝐾 = ⟨ 0 , ( ( 𝑦 − 1 ) mod 5 ) ⟩ ) ∧ ( 𝑏 ∈ ( 0 ..^ 5 ) ∧ 𝑦 ∈ ( 0 ..^ 5 ) ) ) → ( ( { 𝐾 , ⟨ 1 , 𝑏 ⟩ } ∈ 𝐸 ∧ { ⟨ 1 , 𝑏 ⟩ , 𝐿 } ∈ 𝐸 ) → 𝑋 = ⟨ 1 , 𝑏 ⟩ ) )
45 44 ex ⊢ ( ( 𝐿 = ⟨ 0 , ( ( 𝑦 + 1 ) mod 5 ) ⟩ ∧ 𝐾 = ⟨ 0 , ( ( 𝑦 − 1 ) mod 5 ) ⟩ ) → ( ( 𝑏 ∈ ( 0 ..^ 5 ) ∧ 𝑦 ∈ ( 0 ..^ 5 ) ) → ( ( { 𝐾 , ⟨ 1 , 𝑏 ⟩ } ∈ 𝐸 ∧ { ⟨ 1 , 𝑏 ⟩ , 𝐿 } ∈ 𝐸 ) → 𝑋 = ⟨ 1 , 𝑏 ⟩ ) ) )
46 45 adantld ⊢ ( ( 𝐿 = ⟨ 0 , ( ( 𝑦 + 1 ) mod 5 ) ⟩ ∧ 𝐾 = ⟨ 0 , ( ( 𝑦 − 1 ) mod 5 ) ⟩ ) → ( ( 𝐾 ≠ 𝐿 ∧ ( 𝑏 ∈ ( 0 ..^ 5 ) ∧ 𝑦 ∈ ( 0 ..^ 5 ) ) ) → ( ( { 𝐾 , ⟨ 1 , 𝑏 ⟩ } ∈ 𝐸 ∧ { ⟨ 1 , 𝑏 ⟩ , 𝐿 } ∈ 𝐸 ) → 𝑋 = ⟨ 1 , 𝑏 ⟩ ) ) )
47 46 ex ⊢ ( 𝐿 = ⟨ 0 , ( ( 𝑦 + 1 ) mod 5 ) ⟩ → ( 𝐾 = ⟨ 0 , ( ( 𝑦 − 1 ) mod 5 ) ⟩ → ( ( 𝐾 ≠ 𝐿 ∧ ( 𝑏 ∈ ( 0 ..^ 5 ) ∧ 𝑦 ∈ ( 0 ..^ 5 ) ) ) → ( ( { 𝐾 , ⟨ 1 , 𝑏 ⟩ } ∈ 𝐸 ∧ { ⟨ 1 , 𝑏 ⟩ , 𝐿 } ∈ 𝐸 ) → 𝑋 = ⟨ 1 , 𝑏 ⟩ ) ) ) )
48 35 41 47 3jaod ⊢ ( 𝐿 = ⟨ 0 , ( ( 𝑦 + 1 ) mod 5 ) ⟩ → ( ( 𝐾 = ⟨ 0 , ( ( 𝑦 + 1 ) mod 5 ) ⟩ ∨ 𝐾 = ⟨ 1 , 𝑦 ⟩ ∨ 𝐾 = ⟨ 0 , ( ( 𝑦 − 1 ) mod 5 ) ⟩ ) → ( ( 𝐾 ≠ 𝐿 ∧ ( 𝑏 ∈ ( 0 ..^ 5 ) ∧ 𝑦 ∈ ( 0 ..^ 5 ) ) ) → ( ( { 𝐾 , ⟨ 1 , 𝑏 ⟩ } ∈ 𝐸 ∧ { ⟨ 1 , 𝑏 ⟩ , 𝐿 } ∈ 𝐸 ) → 𝑋 = ⟨ 1 , 𝑏 ⟩ ) ) ) )
49 prcom ⊢ { 𝐾 , ⟨ 1 , 𝑏 ⟩ } = { ⟨ 1 , 𝑏 ⟩ , 𝐾 }
50 49 eleq1i ⊢ ( { 𝐾 , ⟨ 1 , 𝑏 ⟩ } ∈ 𝐸 ↔ { ⟨ 1 , 𝑏 ⟩ , 𝐾 } ∈ 𝐸 )
51 prcom ⊢ { ⟨ 1 , 𝑏 ⟩ , 𝐿 } = { 𝐿 , ⟨ 1 , 𝑏 ⟩ }
52 51 eleq1i ⊢ ( { ⟨ 1 , 𝑏 ⟩ , 𝐿 } ∈ 𝐸 ↔ { 𝐿 , ⟨ 1 , 𝑏 ⟩ } ∈ 𝐸 )
53 50 52 anbi12i ⊢ ( ( { 𝐾 , ⟨ 1 , 𝑏 ⟩ } ∈ 𝐸 ∧ { ⟨ 1 , 𝑏 ⟩ , 𝐿 } ∈ 𝐸 ) ↔ ( { ⟨ 1 , 𝑏 ⟩ , 𝐾 } ∈ 𝐸 ∧ { 𝐿 , ⟨ 1 , 𝑏 ⟩ } ∈ 𝐸 ) )
54 1 2 3 4 pgnbgreunbgrlem5lem1 ⊢ ( ( ( ( 𝐾 = ⟨ 0 , ( ( 𝑦 + 1 ) mod 5 ) ⟩ ∧ 𝐿 = ⟨ 1 , 𝑦 ⟩ ) ∧ ( 𝑏 ∈ ( 0 ..^ 5 ) ∧ 𝑦 ∈ ( 0 ..^ 5 ) ) ) ∧ { 𝐿 , ⟨ 1 , 𝑏 ⟩ } ∈ 𝐸 ) → ¬ { ⟨ 1 , 𝑏 ⟩ , 𝐾 } ∈ 𝐸 )
55 54 pm2.21d ⊢ ( ( ( ( 𝐾 = ⟨ 0 , ( ( 𝑦 + 1 ) mod 5 ) ⟩ ∧ 𝐿 = ⟨ 1 , 𝑦 ⟩ ) ∧ ( 𝑏 ∈ ( 0 ..^ 5 ) ∧ 𝑦 ∈ ( 0 ..^ 5 ) ) ) ∧ { 𝐿 , ⟨ 1 , 𝑏 ⟩ } ∈ 𝐸 ) → ( { ⟨ 1 , 𝑏 ⟩ , 𝐾 } ∈ 𝐸 → 𝑋 = ⟨ 1 , 𝑏 ⟩ ) )
56 55 ex ⊢ ( ( ( 𝐾 = ⟨ 0 , ( ( 𝑦 + 1 ) mod 5 ) ⟩ ∧ 𝐿 = ⟨ 1 , 𝑦 ⟩ ) ∧ ( 𝑏 ∈ ( 0 ..^ 5 ) ∧ 𝑦 ∈ ( 0 ..^ 5 ) ) ) → ( { 𝐿 , ⟨ 1 , 𝑏 ⟩ } ∈ 𝐸 → ( { ⟨ 1 , 𝑏 ⟩ , 𝐾 } ∈ 𝐸 → 𝑋 = ⟨ 1 , 𝑏 ⟩ ) ) )
57 56 impcomd ⊢ ( ( ( 𝐾 = ⟨ 0 , ( ( 𝑦 + 1 ) mod 5 ) ⟩ ∧ 𝐿 = ⟨ 1 , 𝑦 ⟩ ) ∧ ( 𝑏 ∈ ( 0 ..^ 5 ) ∧ 𝑦 ∈ ( 0 ..^ 5 ) ) ) → ( ( { ⟨ 1 , 𝑏 ⟩ , 𝐾 } ∈ 𝐸 ∧ { 𝐿 , ⟨ 1 , 𝑏 ⟩ } ∈ 𝐸 ) → 𝑋 = ⟨ 1 , 𝑏 ⟩ ) )
58 53 57 biimtrid ⊢ ( ( ( 𝐾 = ⟨ 0 , ( ( 𝑦 + 1 ) mod 5 ) ⟩ ∧ 𝐿 = ⟨ 1 , 𝑦 ⟩ ) ∧ ( 𝑏 ∈ ( 0 ..^ 5 ) ∧ 𝑦 ∈ ( 0 ..^ 5 ) ) ) → ( ( { 𝐾 , ⟨ 1 , 𝑏 ⟩ } ∈ 𝐸 ∧ { ⟨ 1 , 𝑏 ⟩ , 𝐿 } ∈ 𝐸 ) → 𝑋 = ⟨ 1 , 𝑏 ⟩ ) )
59 58 ex ⊢ ( ( 𝐾 = ⟨ 0 , ( ( 𝑦 + 1 ) mod 5 ) ⟩ ∧ 𝐿 = ⟨ 1 , 𝑦 ⟩ ) → ( ( 𝑏 ∈ ( 0 ..^ 5 ) ∧ 𝑦 ∈ ( 0 ..^ 5 ) ) → ( ( { 𝐾 , ⟨ 1 , 𝑏 ⟩ } ∈ 𝐸 ∧ { ⟨ 1 , 𝑏 ⟩ , 𝐿 } ∈ 𝐸 ) → 𝑋 = ⟨ 1 , 𝑏 ⟩ ) ) )
60 59 adantld ⊢ ( ( 𝐾 = ⟨ 0 , ( ( 𝑦 + 1 ) mod 5 ) ⟩ ∧ 𝐿 = ⟨ 1 , 𝑦 ⟩ ) → ( ( 𝐾 ≠ 𝐿 ∧ ( 𝑏 ∈ ( 0 ..^ 5 ) ∧ 𝑦 ∈ ( 0 ..^ 5 ) ) ) → ( ( { 𝐾 , ⟨ 1 , 𝑏 ⟩ } ∈ 𝐸 ∧ { ⟨ 1 , 𝑏 ⟩ , 𝐿 } ∈ 𝐸 ) → 𝑋 = ⟨ 1 , 𝑏 ⟩ ) ) )
61 60 expcom ⊢ ( 𝐿 = ⟨ 1 , 𝑦 ⟩ → ( 𝐾 = ⟨ 0 , ( ( 𝑦 + 1 ) mod 5 ) ⟩ → ( ( 𝐾 ≠ 𝐿 ∧ ( 𝑏 ∈ ( 0 ..^ 5 ) ∧ 𝑦 ∈ ( 0 ..^ 5 ) ) ) → ( ( { 𝐾 , ⟨ 1 , 𝑏 ⟩ } ∈ 𝐸 ∧ { ⟨ 1 , 𝑏 ⟩ , 𝐿 } ∈ 𝐸 ) → 𝑋 = ⟨ 1 , 𝑏 ⟩ ) ) ) )
62 simpr ⊢ ( ( 𝐿 = ⟨ 1 , 𝑦 ⟩ ∧ 𝐾 = ⟨ 1 , 𝑦 ⟩ ) → 𝐾 = ⟨ 1 , 𝑦 ⟩ )
63 simpl ⊢ ( ( 𝐿 = ⟨ 1 , 𝑦 ⟩ ∧ 𝐾 = ⟨ 1 , 𝑦 ⟩ ) → 𝐿 = ⟨ 1 , 𝑦 ⟩ )
64 62 63 neeq12d ⊢ ( ( 𝐿 = ⟨ 1 , 𝑦 ⟩ ∧ 𝐾 = ⟨ 1 , 𝑦 ⟩ ) → ( 𝐾 ≠ 𝐿 ↔ ⟨ 1 , 𝑦 ⟩ ≠ ⟨ 1 , 𝑦 ⟩ ) )
65 eqid ⊢ ⟨ 1 , 𝑦 ⟩ = ⟨ 1 , 𝑦 ⟩
66 eqneqall ⊢ ( ⟨ 1 , 𝑦 ⟩ = ⟨ 1 , 𝑦 ⟩ → ( ⟨ 1 , 𝑦 ⟩ ≠ ⟨ 1 , 𝑦 ⟩ → ( ( 𝑏 ∈ ( 0 ..^ 5 ) ∧ 𝑦 ∈ ( 0 ..^ 5 ) ) → ( ( { 𝐾 , ⟨ 1 , 𝑏 ⟩ } ∈ 𝐸 ∧ { ⟨ 1 , 𝑏 ⟩ , 𝐿 } ∈ 𝐸 ) → 𝑋 = ⟨ 1 , 𝑏 ⟩ ) ) ) )
67 65 66 ax-mp ⊢ ( ⟨ 1 , 𝑦 ⟩ ≠ ⟨ 1 , 𝑦 ⟩ → ( ( 𝑏 ∈ ( 0 ..^ 5 ) ∧ 𝑦 ∈ ( 0 ..^ 5 ) ) → ( ( { 𝐾 , ⟨ 1 , 𝑏 ⟩ } ∈ 𝐸 ∧ { ⟨ 1 , 𝑏 ⟩ , 𝐿 } ∈ 𝐸 ) → 𝑋 = ⟨ 1 , 𝑏 ⟩ ) ) )
68 64 67 biimtrdi ⊢ ( ( 𝐿 = ⟨ 1 , 𝑦 ⟩ ∧ 𝐾 = ⟨ 1 , 𝑦 ⟩ ) → ( 𝐾 ≠ 𝐿 → ( ( 𝑏 ∈ ( 0 ..^ 5 ) ∧ 𝑦 ∈ ( 0 ..^ 5 ) ) → ( ( { 𝐾 , ⟨ 1 , 𝑏 ⟩ } ∈ 𝐸 ∧ { ⟨ 1 , 𝑏 ⟩ , 𝐿 } ∈ 𝐸 ) → 𝑋 = ⟨ 1 , 𝑏 ⟩ ) ) ) )
69 68 impd ⊢ ( ( 𝐿 = ⟨ 1 , 𝑦 ⟩ ∧ 𝐾 = ⟨ 1 , 𝑦 ⟩ ) → ( ( 𝐾 ≠ 𝐿 ∧ ( 𝑏 ∈ ( 0 ..^ 5 ) ∧ 𝑦 ∈ ( 0 ..^ 5 ) ) ) → ( ( { 𝐾 , ⟨ 1 , 𝑏 ⟩ } ∈ 𝐸 ∧ { ⟨ 1 , 𝑏 ⟩ , 𝐿 } ∈ 𝐸 ) → 𝑋 = ⟨ 1 , 𝑏 ⟩ ) ) )
70 69 ex ⊢ ( 𝐿 = ⟨ 1 , 𝑦 ⟩ → ( 𝐾 = ⟨ 1 , 𝑦 ⟩ → ( ( 𝐾 ≠ 𝐿 ∧ ( 𝑏 ∈ ( 0 ..^ 5 ) ∧ 𝑦 ∈ ( 0 ..^ 5 ) ) ) → ( ( { 𝐾 , ⟨ 1 , 𝑏 ⟩ } ∈ 𝐸 ∧ { ⟨ 1 , 𝑏 ⟩ , 𝐿 } ∈ 𝐸 ) → 𝑋 = ⟨ 1 , 𝑏 ⟩ ) ) ) )
71 1 2 3 4 pgnbgreunbgrlem5lem2 ⊢ ( ( ( ( 𝐾 = ⟨ 0 , ( ( 𝑦 − 1 ) mod 5 ) ⟩ ∧ 𝐿 = ⟨ 1 , 𝑦 ⟩ ) ∧ ( 𝑏 ∈ ( 0 ..^ 5 ) ∧ 𝑦 ∈ ( 0 ..^ 5 ) ) ) ∧ { 𝐿 , ⟨ 1 , 𝑏 ⟩ } ∈ 𝐸 ) → ¬ { ⟨ 1 , 𝑏 ⟩ , 𝐾 } ∈ 𝐸 )
72 71 pm2.21d ⊢ ( ( ( ( 𝐾 = ⟨ 0 , ( ( 𝑦 − 1 ) mod 5 ) ⟩ ∧ 𝐿 = ⟨ 1 , 𝑦 ⟩ ) ∧ ( 𝑏 ∈ ( 0 ..^ 5 ) ∧ 𝑦 ∈ ( 0 ..^ 5 ) ) ) ∧ { 𝐿 , ⟨ 1 , 𝑏 ⟩ } ∈ 𝐸 ) → ( { ⟨ 1 , 𝑏 ⟩ , 𝐾 } ∈ 𝐸 → 𝑋 = ⟨ 1 , 𝑏 ⟩ ) )
73 72 ex ⊢ ( ( ( 𝐾 = ⟨ 0 , ( ( 𝑦 − 1 ) mod 5 ) ⟩ ∧ 𝐿 = ⟨ 1 , 𝑦 ⟩ ) ∧ ( 𝑏 ∈ ( 0 ..^ 5 ) ∧ 𝑦 ∈ ( 0 ..^ 5 ) ) ) → ( { 𝐿 , ⟨ 1 , 𝑏 ⟩ } ∈ 𝐸 → ( { ⟨ 1 , 𝑏 ⟩ , 𝐾 } ∈ 𝐸 → 𝑋 = ⟨ 1 , 𝑏 ⟩ ) ) )
74 73 impcomd ⊢ ( ( ( 𝐾 = ⟨ 0 , ( ( 𝑦 − 1 ) mod 5 ) ⟩ ∧ 𝐿 = ⟨ 1 , 𝑦 ⟩ ) ∧ ( 𝑏 ∈ ( 0 ..^ 5 ) ∧ 𝑦 ∈ ( 0 ..^ 5 ) ) ) → ( ( { ⟨ 1 , 𝑏 ⟩ , 𝐾 } ∈ 𝐸 ∧ { 𝐿 , ⟨ 1 , 𝑏 ⟩ } ∈ 𝐸 ) → 𝑋 = ⟨ 1 , 𝑏 ⟩ ) )
75 53 74 biimtrid ⊢ ( ( ( 𝐾 = ⟨ 0 , ( ( 𝑦 − 1 ) mod 5 ) ⟩ ∧ 𝐿 = ⟨ 1 , 𝑦 ⟩ ) ∧ ( 𝑏 ∈ ( 0 ..^ 5 ) ∧ 𝑦 ∈ ( 0 ..^ 5 ) ) ) → ( ( { 𝐾 , ⟨ 1 , 𝑏 ⟩ } ∈ 𝐸 ∧ { ⟨ 1 , 𝑏 ⟩ , 𝐿 } ∈ 𝐸 ) → 𝑋 = ⟨ 1 , 𝑏 ⟩ ) )
76 75 ex ⊢ ( ( 𝐾 = ⟨ 0 , ( ( 𝑦 − 1 ) mod 5 ) ⟩ ∧ 𝐿 = ⟨ 1 , 𝑦 ⟩ ) → ( ( 𝑏 ∈ ( 0 ..^ 5 ) ∧ 𝑦 ∈ ( 0 ..^ 5 ) ) → ( ( { 𝐾 , ⟨ 1 , 𝑏 ⟩ } ∈ 𝐸 ∧ { ⟨ 1 , 𝑏 ⟩ , 𝐿 } ∈ 𝐸 ) → 𝑋 = ⟨ 1 , 𝑏 ⟩ ) ) )
77 76 adantld ⊢ ( ( 𝐾 = ⟨ 0 , ( ( 𝑦 − 1 ) mod 5 ) ⟩ ∧ 𝐿 = ⟨ 1 , 𝑦 ⟩ ) → ( ( 𝐾 ≠ 𝐿 ∧ ( 𝑏 ∈ ( 0 ..^ 5 ) ∧ 𝑦 ∈ ( 0 ..^ 5 ) ) ) → ( ( { 𝐾 , ⟨ 1 , 𝑏 ⟩ } ∈ 𝐸 ∧ { ⟨ 1 , 𝑏 ⟩ , 𝐿 } ∈ 𝐸 ) → 𝑋 = ⟨ 1 , 𝑏 ⟩ ) ) )
78 77 expcom ⊢ ( 𝐿 = ⟨ 1 , 𝑦 ⟩ → ( 𝐾 = ⟨ 0 , ( ( 𝑦 − 1 ) mod 5 ) ⟩ → ( ( 𝐾 ≠ 𝐿 ∧ ( 𝑏 ∈ ( 0 ..^ 5 ) ∧ 𝑦 ∈ ( 0 ..^ 5 ) ) ) → ( ( { 𝐾 , ⟨ 1 , 𝑏 ⟩ } ∈ 𝐸 ∧ { ⟨ 1 , 𝑏 ⟩ , 𝐿 } ∈ 𝐸 ) → 𝑋 = ⟨ 1 , 𝑏 ⟩ ) ) ) )
79 61 70 78 3jaod ⊢ ( 𝐿 = ⟨ 1 , 𝑦 ⟩ → ( ( 𝐾 = ⟨ 0 , ( ( 𝑦 + 1 ) mod 5 ) ⟩ ∨ 𝐾 = ⟨ 1 , 𝑦 ⟩ ∨ 𝐾 = ⟨ 0 , ( ( 𝑦 − 1 ) mod 5 ) ⟩ ) → ( ( 𝐾 ≠ 𝐿 ∧ ( 𝑏 ∈ ( 0 ..^ 5 ) ∧ 𝑦 ∈ ( 0 ..^ 5 ) ) ) → ( ( { 𝐾 , ⟨ 1 , 𝑏 ⟩ } ∈ 𝐸 ∧ { ⟨ 1 , 𝑏 ⟩ , 𝐿 } ∈ 𝐸 ) → 𝑋 = ⟨ 1 , 𝑏 ⟩ ) ) ) )
80 1 2 3 4 pgnbgreunbgrlem5lem3 ⊢ ( ( ( ( 𝐾 = ⟨ 0 , ( ( 𝑦 + 1 ) mod 5 ) ⟩ ∧ 𝐿 = ⟨ 0 , ( ( 𝑦 − 1 ) mod 5 ) ⟩ ) ∧ ( 𝑏 ∈ ( 0 ..^ 5 ) ∧ 𝑦 ∈ ( 0 ..^ 5 ) ) ) ∧ { 𝐿 , ⟨ 1 , 𝑏 ⟩ } ∈ 𝐸 ) → ¬ { ⟨ 1 , 𝑏 ⟩ , 𝐾 } ∈ 𝐸 )
81 80 pm2.21d ⊢ ( ( ( ( 𝐾 = ⟨ 0 , ( ( 𝑦 + 1 ) mod 5 ) ⟩ ∧ 𝐿 = ⟨ 0 , ( ( 𝑦 − 1 ) mod 5 ) ⟩ ) ∧ ( 𝑏 ∈ ( 0 ..^ 5 ) ∧ 𝑦 ∈ ( 0 ..^ 5 ) ) ) ∧ { 𝐿 , ⟨ 1 , 𝑏 ⟩ } ∈ 𝐸 ) → ( { ⟨ 1 , 𝑏 ⟩ , 𝐾 } ∈ 𝐸 → 𝑋 = ⟨ 1 , 𝑏 ⟩ ) )
82 81 ex ⊢ ( ( ( 𝐾 = ⟨ 0 , ( ( 𝑦 + 1 ) mod 5 ) ⟩ ∧ 𝐿 = ⟨ 0 , ( ( 𝑦 − 1 ) mod 5 ) ⟩ ) ∧ ( 𝑏 ∈ ( 0 ..^ 5 ) ∧ 𝑦 ∈ ( 0 ..^ 5 ) ) ) → ( { 𝐿 , ⟨ 1 , 𝑏 ⟩ } ∈ 𝐸 → ( { ⟨ 1 , 𝑏 ⟩ , 𝐾 } ∈ 𝐸 → 𝑋 = ⟨ 1 , 𝑏 ⟩ ) ) )
83 82 impcomd ⊢ ( ( ( 𝐾 = ⟨ 0 , ( ( 𝑦 + 1 ) mod 5 ) ⟩ ∧ 𝐿 = ⟨ 0 , ( ( 𝑦 − 1 ) mod 5 ) ⟩ ) ∧ ( 𝑏 ∈ ( 0 ..^ 5 ) ∧ 𝑦 ∈ ( 0 ..^ 5 ) ) ) → ( ( { ⟨ 1 , 𝑏 ⟩ , 𝐾 } ∈ 𝐸 ∧ { 𝐿 , ⟨ 1 , 𝑏 ⟩ } ∈ 𝐸 ) → 𝑋 = ⟨ 1 , 𝑏 ⟩ ) )
84 53 83 biimtrid ⊢ ( ( ( 𝐾 = ⟨ 0 , ( ( 𝑦 + 1 ) mod 5 ) ⟩ ∧ 𝐿 = ⟨ 0 , ( ( 𝑦 − 1 ) mod 5 ) ⟩ ) ∧ ( 𝑏 ∈ ( 0 ..^ 5 ) ∧ 𝑦 ∈ ( 0 ..^ 5 ) ) ) → ( ( { 𝐾 , ⟨ 1 , 𝑏 ⟩ } ∈ 𝐸 ∧ { ⟨ 1 , 𝑏 ⟩ , 𝐿 } ∈ 𝐸 ) → 𝑋 = ⟨ 1 , 𝑏 ⟩ ) )
85 84 ex ⊢ ( ( 𝐾 = ⟨ 0 , ( ( 𝑦 + 1 ) mod 5 ) ⟩ ∧ 𝐿 = ⟨ 0 , ( ( 𝑦 − 1 ) mod 5 ) ⟩ ) → ( ( 𝑏 ∈ ( 0 ..^ 5 ) ∧ 𝑦 ∈ ( 0 ..^ 5 ) ) → ( ( { 𝐾 , ⟨ 1 , 𝑏 ⟩ } ∈ 𝐸 ∧ { ⟨ 1 , 𝑏 ⟩ , 𝐿 } ∈ 𝐸 ) → 𝑋 = ⟨ 1 , 𝑏 ⟩ ) ) )
86 85 adantld ⊢ ( ( 𝐾 = ⟨ 0 , ( ( 𝑦 + 1 ) mod 5 ) ⟩ ∧ 𝐿 = ⟨ 0 , ( ( 𝑦 − 1 ) mod 5 ) ⟩ ) → ( ( 𝐾 ≠ 𝐿 ∧ ( 𝑏 ∈ ( 0 ..^ 5 ) ∧ 𝑦 ∈ ( 0 ..^ 5 ) ) ) → ( ( { 𝐾 , ⟨ 1 , 𝑏 ⟩ } ∈ 𝐸 ∧ { ⟨ 1 , 𝑏 ⟩ , 𝐿 } ∈ 𝐸 ) → 𝑋 = ⟨ 1 , 𝑏 ⟩ ) ) )
87 86 expcom ⊢ ( 𝐿 = ⟨ 0 , ( ( 𝑦 − 1 ) mod 5 ) ⟩ → ( 𝐾 = ⟨ 0 , ( ( 𝑦 + 1 ) mod 5 ) ⟩ → ( ( 𝐾 ≠ 𝐿 ∧ ( 𝑏 ∈ ( 0 ..^ 5 ) ∧ 𝑦 ∈ ( 0 ..^ 5 ) ) ) → ( ( { 𝐾 , ⟨ 1 , 𝑏 ⟩ } ∈ 𝐸 ∧ { ⟨ 1 , 𝑏 ⟩ , 𝐿 } ∈ 𝐸 ) → 𝑋 = ⟨ 1 , 𝑏 ⟩ ) ) ) )
88 1 2 3 4 pgnbgreunbgrlem5lem2 ⊢ ( ( ( ( 𝐿 = ⟨ 0 , ( ( 𝑦 − 1 ) mod 5 ) ⟩ ∧ 𝐾 = ⟨ 1 , 𝑦 ⟩ ) ∧ ( 𝑏 ∈ ( 0 ..^ 5 ) ∧ 𝑦 ∈ ( 0 ..^ 5 ) ) ) ∧ { 𝐾 , ⟨ 1 , 𝑏 ⟩ } ∈ 𝐸 ) → ¬ { ⟨ 1 , 𝑏 ⟩ , 𝐿 } ∈ 𝐸 )
89 88 pm2.21d ⊢ ( ( ( ( 𝐿 = ⟨ 0 , ( ( 𝑦 − 1 ) mod 5 ) ⟩ ∧ 𝐾 = ⟨ 1 , 𝑦 ⟩ ) ∧ ( 𝑏 ∈ ( 0 ..^ 5 ) ∧ 𝑦 ∈ ( 0 ..^ 5 ) ) ) ∧ { 𝐾 , ⟨ 1 , 𝑏 ⟩ } ∈ 𝐸 ) → ( { ⟨ 1 , 𝑏 ⟩ , 𝐿 } ∈ 𝐸 → 𝑋 = ⟨ 1 , 𝑏 ⟩ ) )
90 89 expimpd ⊢ ( ( ( 𝐿 = ⟨ 0 , ( ( 𝑦 − 1 ) mod 5 ) ⟩ ∧ 𝐾 = ⟨ 1 , 𝑦 ⟩ ) ∧ ( 𝑏 ∈ ( 0 ..^ 5 ) ∧ 𝑦 ∈ ( 0 ..^ 5 ) ) ) → ( ( { 𝐾 , ⟨ 1 , 𝑏 ⟩ } ∈ 𝐸 ∧ { ⟨ 1 , 𝑏 ⟩ , 𝐿 } ∈ 𝐸 ) → 𝑋 = ⟨ 1 , 𝑏 ⟩ ) )
91 90 ex ⊢ ( ( 𝐿 = ⟨ 0 , ( ( 𝑦 − 1 ) mod 5 ) ⟩ ∧ 𝐾 = ⟨ 1 , 𝑦 ⟩ ) → ( ( 𝑏 ∈ ( 0 ..^ 5 ) ∧ 𝑦 ∈ ( 0 ..^ 5 ) ) → ( ( { 𝐾 , ⟨ 1 , 𝑏 ⟩ } ∈ 𝐸 ∧ { ⟨ 1 , 𝑏 ⟩ , 𝐿 } ∈ 𝐸 ) → 𝑋 = ⟨ 1 , 𝑏 ⟩ ) ) )
92 91 adantld ⊢ ( ( 𝐿 = ⟨ 0 , ( ( 𝑦 − 1 ) mod 5 ) ⟩ ∧ 𝐾 = ⟨ 1 , 𝑦 ⟩ ) → ( ( 𝐾 ≠ 𝐿 ∧ ( 𝑏 ∈ ( 0 ..^ 5 ) ∧ 𝑦 ∈ ( 0 ..^ 5 ) ) ) → ( ( { 𝐾 , ⟨ 1 , 𝑏 ⟩ } ∈ 𝐸 ∧ { ⟨ 1 , 𝑏 ⟩ , 𝐿 } ∈ 𝐸 ) → 𝑋 = ⟨ 1 , 𝑏 ⟩ ) ) )
93 92 ex ⊢ ( 𝐿 = ⟨ 0 , ( ( 𝑦 − 1 ) mod 5 ) ⟩ → ( 𝐾 = ⟨ 1 , 𝑦 ⟩ → ( ( 𝐾 ≠ 𝐿 ∧ ( 𝑏 ∈ ( 0 ..^ 5 ) ∧ 𝑦 ∈ ( 0 ..^ 5 ) ) ) → ( ( { 𝐾 , ⟨ 1 , 𝑏 ⟩ } ∈ 𝐸 ∧ { ⟨ 1 , 𝑏 ⟩ , 𝐿 } ∈ 𝐸 ) → 𝑋 = ⟨ 1 , 𝑏 ⟩ ) ) ) )
94 simpr ⊢ ( ( 𝐿 = ⟨ 0 , ( ( 𝑦 − 1 ) mod 5 ) ⟩ ∧ 𝐾 = ⟨ 0 , ( ( 𝑦 − 1 ) mod 5 ) ⟩ ) → 𝐾 = ⟨ 0 , ( ( 𝑦 − 1 ) mod 5 ) ⟩ )
95 simpl ⊢ ( ( 𝐿 = ⟨ 0 , ( ( 𝑦 − 1 ) mod 5 ) ⟩ ∧ 𝐾 = ⟨ 0 , ( ( 𝑦 − 1 ) mod 5 ) ⟩ ) → 𝐿 = ⟨ 0 , ( ( 𝑦 − 1 ) mod 5 ) ⟩ )
96 94 95 neeq12d ⊢ ( ( 𝐿 = ⟨ 0 , ( ( 𝑦 − 1 ) mod 5 ) ⟩ ∧ 𝐾 = ⟨ 0 , ( ( 𝑦 − 1 ) mod 5 ) ⟩ ) → ( 𝐾 ≠ 𝐿 ↔ ⟨ 0 , ( ( 𝑦 − 1 ) mod 5 ) ⟩ ≠ ⟨ 0 , ( ( 𝑦 − 1 ) mod 5 ) ⟩ ) )
97 eqid ⊢ ⟨ 0 , ( ( 𝑦 − 1 ) mod 5 ) ⟩ = ⟨ 0 , ( ( 𝑦 − 1 ) mod 5 ) ⟩
98 eqneqall ⊢ ( ⟨ 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 ⊢ ( ⟨ 0 , ( ( 𝑦 − 1 ) mod 5 ) ⟩ ≠ ⟨ 0 , ( ( 𝑦 − 1 ) mod 5 ) ⟩ → ( ( 𝑏 ∈ ( 0 ..^ 5 ) ∧ 𝑦 ∈ ( 0 ..^ 5 ) ) → ( ( { 𝐾 , ⟨ 1 , 𝑏 ⟩ } ∈ 𝐸 ∧ { ⟨ 1 , 𝑏 ⟩ , 𝐿 } ∈ 𝐸 ) → 𝑋 = ⟨ 1 , 𝑏 ⟩ ) ) )
100 96 99 biimtrdi ⊢ ( ( 𝐿 = ⟨ 0 , ( ( 𝑦 − 1 ) mod 5 ) ⟩ ∧ 𝐾 = ⟨ 0 , ( ( 𝑦 − 1 ) mod 5 ) ⟩ ) → ( 𝐾 ≠ 𝐿 → ( ( 𝑏 ∈ ( 0 ..^ 5 ) ∧ 𝑦 ∈ ( 0 ..^ 5 ) ) → ( ( { 𝐾 , ⟨ 1 , 𝑏 ⟩ } ∈ 𝐸 ∧ { ⟨ 1 , 𝑏 ⟩ , 𝐿 } ∈ 𝐸 ) → 𝑋 = ⟨ 1 , 𝑏 ⟩ ) ) ) )
101 100 impd ⊢ ( ( 𝐿 = ⟨ 0 , ( ( 𝑦 − 1 ) mod 5 ) ⟩ ∧ 𝐾 = ⟨ 0 , ( ( 𝑦 − 1 ) mod 5 ) ⟩ ) → ( ( 𝐾 ≠ 𝐿 ∧ ( 𝑏 ∈ ( 0 ..^ 5 ) ∧ 𝑦 ∈ ( 0 ..^ 5 ) ) ) → ( ( { 𝐾 , ⟨ 1 , 𝑏 ⟩ } ∈ 𝐸 ∧ { ⟨ 1 , 𝑏 ⟩ , 𝐿 } ∈ 𝐸 ) → 𝑋 = ⟨ 1 , 𝑏 ⟩ ) ) )
102 101 ex ⊢ ( 𝐿 = ⟨ 0 , ( ( 𝑦 − 1 ) mod 5 ) ⟩ → ( 𝐾 = ⟨ 0 , ( ( 𝑦 − 1 ) mod 5 ) ⟩ → ( ( 𝐾 ≠ 𝐿 ∧ ( 𝑏 ∈ ( 0 ..^ 5 ) ∧ 𝑦 ∈ ( 0 ..^ 5 ) ) ) → ( ( { 𝐾 , ⟨ 1 , 𝑏 ⟩ } ∈ 𝐸 ∧ { ⟨ 1 , 𝑏 ⟩ , 𝐿 } ∈ 𝐸 ) → 𝑋 = ⟨ 1 , 𝑏 ⟩ ) ) ) )
103 87 93 102 3jaod ⊢ ( 𝐿 = ⟨ 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 ⊢ ( ( 𝐿 = ⟨ 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 ⊢ ( ( ( 𝐿 = ⟨ 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 25 105 biimtrdi ⊢ ( ( 𝑋 = ⟨ 0 , 𝑦 ⟩ ∧ 𝑋 ∈ 𝑉 ) → ( ( ( 𝐿 = ⟨ 0 , ( ( ( 2nd ‘ 𝑋 ) + 1 ) mod 5 ) ⟩ ∨ 𝐿 = ⟨ 1 , ( 2nd ‘ 𝑋 ) ⟩ ∨ 𝐿 = ⟨ 0 , ( ( ( 2nd ‘ 𝑋 ) − 1 ) mod 5 ) ⟩ ) ∧ ( 𝐾 = ⟨ 0 , ( ( ( 2nd ‘ 𝑋 ) + 1 ) mod 5 ) ⟩ ∨ 𝐾 = ⟨ 1 , ( 2nd ‘ 𝑋 ) ⟩ ∨ 𝐾 = ⟨ 0 , ( ( ( 2nd ‘ 𝑋 ) − 1 ) mod 5 ) ⟩ ) ) → ( ( 𝐾 ≠ 𝐿 ∧ ( 𝑏 ∈ ( 0 ..^ 5 ) ∧ 𝑦 ∈ ( 0 ..^ 5 ) ) ) → ( ( { 𝐾 , ⟨ 1 , 𝑏 ⟩ } ∈ 𝐸 ∧ { ⟨ 1 , 𝑏 ⟩ , 𝐿 } ∈ 𝐸 ) → 𝑋 = ⟨ 1 , 𝑏 ⟩ ) ) ) )
107 106 expdcom ⊢ ( ( 𝐿 = ⟨ 0 , ( ( ( 2nd ‘ 𝑋 ) + 1 ) mod 5 ) ⟩ ∨ 𝐿 = ⟨ 1 , ( 2nd ‘ 𝑋 ) ⟩ ∨ 𝐿 = ⟨ 0 , ( ( ( 2nd ‘ 𝑋 ) − 1 ) mod 5 ) ⟩ ) → ( ( 𝐾 = ⟨ 0 , ( ( ( 2nd ‘ 𝑋 ) + 1 ) mod 5 ) ⟩ ∨ 𝐾 = ⟨ 1 , ( 2nd ‘ 𝑋 ) ⟩ ∨ 𝐾 = ⟨ 0 , ( ( ( 2nd ‘ 𝑋 ) − 1 ) mod 5 ) ⟩ ) → ( ( 𝑋 = ⟨ 0 , 𝑦 ⟩ ∧ 𝑋 ∈ 𝑉 ) → ( ( 𝐾 ≠ 𝐿 ∧ ( 𝑏 ∈ ( 0 ..^ 5 ) ∧ 𝑦 ∈ ( 0 ..^ 5 ) ) ) → ( ( { 𝐾 , ⟨ 1 , 𝑏 ⟩ } ∈ 𝐸 ∧ { ⟨ 1 , 𝑏 ⟩ , 𝐿 } ∈ 𝐸 ) → 𝑋 = ⟨ 1 , 𝑏 ⟩ ) ) ) ) )