Metamath Proof Explorer

Theorem pgnbgreunbgrlem2

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

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

Proof

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