Metamath Proof Explorer

Theorem pgnbgreunbgrlem2lem2

Description: Lemma 2 for pgnbgreunbgrlem2 . (Contributed by AV, 16-Nov-2025)

Ref Expression
Hypotheses pgnbgreunbgr.g ⊢ 𝐺 = ( 5 gPetersenGr 2 )
pgnbgreunbgr.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
pgnbgreunbgr.e ⊢ 𝐸 = ( Edg ‘ 𝐺 )
pgnbgreunbgr.n ⊢ 𝑁 = ( 𝐺 NeighbVtx 𝑋 )
Assertion pgnbgreunbgrlem2lem2 ( ( ( ( 𝐿 = ⟨ 1 , ( ( 𝑦 − 2 ) mod 5 ) ⟩ ∧ 𝐾 = ⟨ 0 , 𝑦 ⟩ ) ∧ ( 𝑏 ∈ ( 0 ..^ 5 ) ∧ 𝑦 ∈ ( 0 ..^ 5 ) ) ) ∧ { 𝐾 , ⟨ 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 5eluz3 ⊢ 5 ∈ ( ℤ≥ ‘ 3 )
6 pglem ⊢ 2 ∈ ( 1 ..^ ( ⌈ ‘ ( 5 / 2 ) ) )
7 5 6 pm3.2i ⊢ ( 5 ∈ ( ℤ≥ ‘ 3 ) ∧ 2 ∈ ( 1 ..^ ( ⌈ ‘ ( 5 / 2 ) ) ) )
8 c0ex ⊢ 0 ∈ V
9 vex ⊢ 𝑦 ∈ V
10 8 9 op1st ⊢ ( 1st ‘ ⟨ 0 , 𝑦 ⟩ ) = 0
11 simpr ⊢ ( ( ( 𝑏 ∈ ( 0 ..^ 5 ) ∧ 𝑦 ∈ ( 0 ..^ 5 ) ) ∧ { ⟨ 0 , 𝑦 ⟩ , ⟨ 0 , 𝑏 ⟩ } ∈ 𝐸 ) → { ⟨ 0 , 𝑦 ⟩ , ⟨ 0 , 𝑏 ⟩ } ∈ 𝐸 )
12 eqid ⊢ ( 1 ..^ ( ⌈ ‘ ( 5 / 2 ) ) ) = ( 1 ..^ ( ⌈ ‘ ( 5 / 2 ) ) )
13 12 1 2 3 gpgvtxedg0 ⊢ ( ( ( 5 ∈ ( ℤ≥ ‘ 3 ) ∧ 2 ∈ ( 1 ..^ ( ⌈ ‘ ( 5 / 2 ) ) ) ) ∧ ( 1st ‘ ⟨ 0 , 𝑦 ⟩ ) = 0 ∧ { ⟨ 0 , 𝑦 ⟩ , ⟨ 0 , 𝑏 ⟩ } ∈ 𝐸 ) → ( ⟨ 0 , 𝑏 ⟩ = ⟨ 0 , ( ( ( 2nd ‘ ⟨ 0 , 𝑦 ⟩ ) + 1 ) mod 5 ) ⟩ ∨ ⟨ 0 , 𝑏 ⟩ = ⟨ 1 , ( 2nd ‘ ⟨ 0 , 𝑦 ⟩ ) ⟩ ∨ ⟨ 0 , 𝑏 ⟩ = ⟨ 0 , ( ( ( 2nd ‘ ⟨ 0 , 𝑦 ⟩ ) − 1 ) mod 5 ) ⟩ ) )
14 7 10 11 13 mp3an12i ⊢ ( ( ( 𝑏 ∈ ( 0 ..^ 5 ) ∧ 𝑦 ∈ ( 0 ..^ 5 ) ) ∧ { ⟨ 0 , 𝑦 ⟩ , ⟨ 0 , 𝑏 ⟩ } ∈ 𝐸 ) → ( ⟨ 0 , 𝑏 ⟩ = ⟨ 0 , ( ( ( 2nd ‘ ⟨ 0 , 𝑦 ⟩ ) + 1 ) mod 5 ) ⟩ ∨ ⟨ 0 , 𝑏 ⟩ = ⟨ 1 , ( 2nd ‘ ⟨ 0 , 𝑦 ⟩ ) ⟩ ∨ ⟨ 0 , 𝑏 ⟩ = ⟨ 0 , ( ( ( 2nd ‘ ⟨ 0 , 𝑦 ⟩ ) − 1 ) mod 5 ) ⟩ ) )
15 14 ex ⊢ ( ( 𝑏 ∈ ( 0 ..^ 5 ) ∧ 𝑦 ∈ ( 0 ..^ 5 ) ) → ( { ⟨ 0 , 𝑦 ⟩ , ⟨ 0 , 𝑏 ⟩ } ∈ 𝐸 → ( ⟨ 0 , 𝑏 ⟩ = ⟨ 0 , ( ( ( 2nd ‘ ⟨ 0 , 𝑦 ⟩ ) + 1 ) mod 5 ) ⟩ ∨ ⟨ 0 , 𝑏 ⟩ = ⟨ 1 , ( 2nd ‘ ⟨ 0 , 𝑦 ⟩ ) ⟩ ∨ ⟨ 0 , 𝑏 ⟩ = ⟨ 0 , ( ( ( 2nd ‘ ⟨ 0 , 𝑦 ⟩ ) − 1 ) mod 5 ) ⟩ ) ) )
16 vex ⊢ 𝑏 ∈ V
17 8 16 op1st ⊢ ( 1st ‘ ⟨ 0 , 𝑏 ⟩ ) = 0
18 12 1 2 3 gpgvtxedg0 ⊢ ( ( ( 5 ∈ ( ℤ≥ ‘ 3 ) ∧ 2 ∈ ( 1 ..^ ( ⌈ ‘ ( 5 / 2 ) ) ) ) ∧ ( 1st ‘ ⟨ 0 , 𝑏 ⟩ ) = 0 ∧ { ⟨ 0 , 𝑏 ⟩ , ⟨ 1 , ( ( 𝑦 − 2 ) mod 5 ) ⟩ } ∈ 𝐸 ) → ( ⟨ 1 , ( ( 𝑦 − 2 ) mod 5 ) ⟩ = ⟨ 0 , ( ( ( 2nd ‘ ⟨ 0 , 𝑏 ⟩ ) + 1 ) mod 5 ) ⟩ ∨ ⟨ 1 , ( ( 𝑦 − 2 ) mod 5 ) ⟩ = ⟨ 1 , ( 2nd ‘ ⟨ 0 , 𝑏 ⟩ ) ⟩ ∨ ⟨ 1 , ( ( 𝑦 − 2 ) mod 5 ) ⟩ = ⟨ 0 , ( ( ( 2nd ‘ ⟨ 0 , 𝑏 ⟩ ) − 1 ) mod 5 ) ⟩ ) )
19 7 17 18 mp3an12 ⊢ ( { ⟨ 0 , 𝑏 ⟩ , ⟨ 1 , ( ( 𝑦 − 2 ) mod 5 ) ⟩ } ∈ 𝐸 → ( ⟨ 1 , ( ( 𝑦 − 2 ) mod 5 ) ⟩ = ⟨ 0 , ( ( ( 2nd ‘ ⟨ 0 , 𝑏 ⟩ ) + 1 ) mod 5 ) ⟩ ∨ ⟨ 1 , ( ( 𝑦 − 2 ) mod 5 ) ⟩ = ⟨ 1 , ( 2nd ‘ ⟨ 0 , 𝑏 ⟩ ) ⟩ ∨ ⟨ 1 , ( ( 𝑦 − 2 ) mod 5 ) ⟩ = ⟨ 0 , ( ( ( 2nd ‘ ⟨ 0 , 𝑏 ⟩ ) − 1 ) mod 5 ) ⟩ ) )
20 1ex ⊢ 1 ∈ V
21 ovex ⊢ ( ( 𝑦 − 2 ) mod 5 ) ∈ V
22 20 21 opth ⊢ ( ⟨ 1 , ( ( 𝑦 − 2 ) mod 5 ) ⟩ = ⟨ 0 , ( ( ( 2nd ‘ ⟨ 0 , 𝑏 ⟩ ) + 1 ) mod 5 ) ⟩ ↔ ( 1 = 0 ∧ ( ( 𝑦 − 2 ) mod 5 ) = ( ( ( 2nd ‘ ⟨ 0 , 𝑏 ⟩ ) + 1 ) mod 5 ) ) )
23 ax-1ne0 ⊢ 1 ≠ 0
24 eqneqall ⊢ ( 1 = 0 → ( 1 ≠ 0 → ( ( ( 𝑏 ∈ ( 0 ..^ 5 ) ∧ 𝑦 ∈ ( 0 ..^ 5 ) ) ∧ ( ⟨ 0 , 𝑏 ⟩ = ⟨ 0 , ( ( ( 2nd ‘ ⟨ 0 , 𝑦 ⟩ ) + 1 ) mod 5 ) ⟩ ∨ ⟨ 0 , 𝑏 ⟩ = ⟨ 1 , ( 2nd ‘ ⟨ 0 , 𝑦 ⟩ ) ⟩ ∨ ⟨ 0 , 𝑏 ⟩ = ⟨ 0 , ( ( ( 2nd ‘ ⟨ 0 , 𝑦 ⟩ ) − 1 ) mod 5 ) ⟩ ) ) → ¬ { ⟨ 0 , 𝑏 ⟩ , ⟨ 1 , ( ( 𝑦 − 2 ) mod 5 ) ⟩ } ∈ 𝐸 ) ) )
25 23 24 mpi ⊢ ( 1 = 0 → ( ( ( 𝑏 ∈ ( 0 ..^ 5 ) ∧ 𝑦 ∈ ( 0 ..^ 5 ) ) ∧ ( ⟨ 0 , 𝑏 ⟩ = ⟨ 0 , ( ( ( 2nd ‘ ⟨ 0 , 𝑦 ⟩ ) + 1 ) mod 5 ) ⟩ ∨ ⟨ 0 , 𝑏 ⟩ = ⟨ 1 , ( 2nd ‘ ⟨ 0 , 𝑦 ⟩ ) ⟩ ∨ ⟨ 0 , 𝑏 ⟩ = ⟨ 0 , ( ( ( 2nd ‘ ⟨ 0 , 𝑦 ⟩ ) − 1 ) mod 5 ) ⟩ ) ) → ¬ { ⟨ 0 , 𝑏 ⟩ , ⟨ 1 , ( ( 𝑦 − 2 ) mod 5 ) ⟩ } ∈ 𝐸 ) )
26 25 adantr ⊢ ( ( 1 = 0 ∧ ( ( 𝑦 − 2 ) mod 5 ) = ( ( ( 2nd ‘ ⟨ 0 , 𝑏 ⟩ ) + 1 ) mod 5 ) ) → ( ( ( 𝑏 ∈ ( 0 ..^ 5 ) ∧ 𝑦 ∈ ( 0 ..^ 5 ) ) ∧ ( ⟨ 0 , 𝑏 ⟩ = ⟨ 0 , ( ( ( 2nd ‘ ⟨ 0 , 𝑦 ⟩ ) + 1 ) mod 5 ) ⟩ ∨ ⟨ 0 , 𝑏 ⟩ = ⟨ 1 , ( 2nd ‘ ⟨ 0 , 𝑦 ⟩ ) ⟩ ∨ ⟨ 0 , 𝑏 ⟩ = ⟨ 0 , ( ( ( 2nd ‘ ⟨ 0 , 𝑦 ⟩ ) − 1 ) mod 5 ) ⟩ ) ) → ¬ { ⟨ 0 , 𝑏 ⟩ , ⟨ 1 , ( ( 𝑦 − 2 ) mod 5 ) ⟩ } ∈ 𝐸 ) )
27 22 26 sylbi ⊢ ( ⟨ 1 , ( ( 𝑦 − 2 ) mod 5 ) ⟩ = ⟨ 0 , ( ( ( 2nd ‘ ⟨ 0 , 𝑏 ⟩ ) + 1 ) mod 5 ) ⟩ → ( ( ( 𝑏 ∈ ( 0 ..^ 5 ) ∧ 𝑦 ∈ ( 0 ..^ 5 ) ) ∧ ( ⟨ 0 , 𝑏 ⟩ = ⟨ 0 , ( ( ( 2nd ‘ ⟨ 0 , 𝑦 ⟩ ) + 1 ) mod 5 ) ⟩ ∨ ⟨ 0 , 𝑏 ⟩ = ⟨ 1 , ( 2nd ‘ ⟨ 0 , 𝑦 ⟩ ) ⟩ ∨ ⟨ 0 , 𝑏 ⟩ = ⟨ 0 , ( ( ( 2nd ‘ ⟨ 0 , 𝑦 ⟩ ) − 1 ) mod 5 ) ⟩ ) ) → ¬ { ⟨ 0 , 𝑏 ⟩ , ⟨ 1 , ( ( 𝑦 − 2 ) mod 5 ) ⟩ } ∈ 𝐸 ) )
28 20 21 opth ⊢ ( ⟨ 1 , ( ( 𝑦 − 2 ) mod 5 ) ⟩ = ⟨ 1 , ( 2nd ‘ ⟨ 0 , 𝑏 ⟩ ) ⟩ ↔ ( 1 = 1 ∧ ( ( 𝑦 − 2 ) mod 5 ) = ( 2nd ‘ ⟨ 0 , 𝑏 ⟩ ) ) )
29 8 16 op2nd ⊢ ( 2nd ‘ ⟨ 0 , 𝑏 ⟩ ) = 𝑏
30 29 eqeq2i ⊢ ( ( ( 𝑦 − 2 ) mod 5 ) = ( 2nd ‘ ⟨ 0 , 𝑏 ⟩ ) ↔ ( ( 𝑦 − 2 ) mod 5 ) = 𝑏 )
31 eqcom ⊢ ( ( ( 𝑦 − 2 ) mod 5 ) = 𝑏 ↔ 𝑏 = ( ( 𝑦 − 2 ) mod 5 ) )
32 30 31 bitri ⊢ ( ( ( 𝑦 − 2 ) mod 5 ) = ( 2nd ‘ ⟨ 0 , 𝑏 ⟩ ) ↔ 𝑏 = ( ( 𝑦 − 2 ) mod 5 ) )
33 8 9 op2nd ⊢ ( 2nd ‘ ⟨ 0 , 𝑦 ⟩ ) = 𝑦
34 33 oveq1i ⊢ ( ( 2nd ‘ ⟨ 0 , 𝑦 ⟩ ) + 1 ) = ( 𝑦 + 1 )
35 34 oveq1i ⊢ ( ( ( 2nd ‘ ⟨ 0 , 𝑦 ⟩ ) + 1 ) mod 5 ) = ( ( 𝑦 + 1 ) mod 5 )
36 35 opeq2i ⊢ ⟨ 0 , ( ( ( 2nd ‘ ⟨ 0 , 𝑦 ⟩ ) + 1 ) mod 5 ) ⟩ = ⟨ 0 , ( ( 𝑦 + 1 ) mod 5 ) ⟩
37 36 eqeq2i ⊢ ( ⟨ 0 , 𝑏 ⟩ = ⟨ 0 , ( ( ( 2nd ‘ ⟨ 0 , 𝑦 ⟩ ) + 1 ) mod 5 ) ⟩ ↔ ⟨ 0 , 𝑏 ⟩ = ⟨ 0 , ( ( 𝑦 + 1 ) mod 5 ) ⟩ )
38 8 16 opth ⊢ ( ⟨ 0 , 𝑏 ⟩ = ⟨ 0 , ( ( 𝑦 + 1 ) mod 5 ) ⟩ ↔ ( 0 = 0 ∧ 𝑏 = ( ( 𝑦 + 1 ) mod 5 ) ) )
39 37 38 bitri ⊢ ( ⟨ 0 , 𝑏 ⟩ = ⟨ 0 , ( ( ( 2nd ‘ ⟨ 0 , 𝑦 ⟩ ) + 1 ) mod 5 ) ⟩ ↔ ( 0 = 0 ∧ 𝑏 = ( ( 𝑦 + 1 ) mod 5 ) ) )
40 eqeq1 ⊢ ( 𝑏 = ( ( 𝑦 + 1 ) mod 5 ) → ( 𝑏 = ( ( 𝑦 − 2 ) mod 5 ) ↔ ( ( 𝑦 + 1 ) mod 5 ) = ( ( 𝑦 − 2 ) mod 5 ) ) )
41 40 adantr ⊢ ( ( 𝑏 = ( ( 𝑦 + 1 ) mod 5 ) ∧ ( 𝑏 ∈ ( 0 ..^ 5 ) ∧ 𝑦 ∈ ( 0 ..^ 5 ) ) ) → ( 𝑏 = ( ( 𝑦 − 2 ) mod 5 ) ↔ ( ( 𝑦 + 1 ) mod 5 ) = ( ( 𝑦 − 2 ) mod 5 ) ) )
42 eqcom ⊢ ( ( ( 𝑦 + 1 ) mod 5 ) = ( ( 𝑦 − 2 ) mod 5 ) ↔ ( ( 𝑦 − 2 ) mod 5 ) = ( ( 𝑦 + 1 ) mod 5 ) )
43 42 a1i ⊢ ( 𝑦 ∈ ( 0 ..^ 5 ) → ( ( ( 𝑦 + 1 ) mod 5 ) = ( ( 𝑦 − 2 ) mod 5 ) ↔ ( ( 𝑦 − 2 ) mod 5 ) = ( ( 𝑦 + 1 ) mod 5 ) ) )
44 elfzoelz ⊢ ( 𝑦 ∈ ( 0 ..^ 5 ) → 𝑦 ∈ ℤ )
45 2z ⊢ 2 ∈ ℤ
46 45 a1i ⊢ ( 𝑦 ∈ ( 0 ..^ 5 ) → 2 ∈ ℤ )
47 44 46 zsubcld ⊢ ( 𝑦 ∈ ( 0 ..^ 5 ) → ( 𝑦 − 2 ) ∈ ℤ )
48 44 peano2zd ⊢ ( 𝑦 ∈ ( 0 ..^ 5 ) → ( 𝑦 + 1 ) ∈ ℤ )
49 5nn ⊢ 5 ∈ ℕ
50 49 a1i ⊢ ( 𝑦 ∈ ( 0 ..^ 5 ) → 5 ∈ ℕ )
51 difmod0 ⊢ ( ( ( 𝑦 − 2 ) ∈ ℤ ∧ ( 𝑦 + 1 ) ∈ ℤ ∧ 5 ∈ ℕ ) → ( ( ( ( 𝑦 − 2 ) − ( 𝑦 + 1 ) ) mod 5 ) = 0 ↔ ( ( 𝑦 − 2 ) mod 5 ) = ( ( 𝑦 + 1 ) mod 5 ) ) )
52 47 48 50 51 syl3anc ⊢ ( 𝑦 ∈ ( 0 ..^ 5 ) → ( ( ( ( 𝑦 − 2 ) − ( 𝑦 + 1 ) ) mod 5 ) = 0 ↔ ( ( 𝑦 − 2 ) mod 5 ) = ( ( 𝑦 + 1 ) mod 5 ) ) )
53 44 zcnd ⊢ ( 𝑦 ∈ ( 0 ..^ 5 ) → 𝑦 ∈ ℂ )
54 2cnd ⊢ ( 𝑦 ∈ ( 0 ..^ 5 ) → 2 ∈ ℂ )
55 1cnd ⊢ ( 𝑦 ∈ ( 0 ..^ 5 ) → 1 ∈ ℂ )
56 53 54 53 55 subsubadd23 ⊢ ( 𝑦 ∈ ( 0 ..^ 5 ) → ( ( 𝑦 − 2 ) − ( 𝑦 + 1 ) ) = ( ( 𝑦 − 𝑦 ) − ( 2 + 1 ) ) )
57 53 subidd ⊢ ( 𝑦 ∈ ( 0 ..^ 5 ) → ( 𝑦 − 𝑦 ) = 0 )
58 2p1e3 ⊢ ( 2 + 1 ) = 3
59 58 a1i ⊢ ( 𝑦 ∈ ( 0 ..^ 5 ) → ( 2 + 1 ) = 3 )
60 57 59 oveq12d ⊢ ( 𝑦 ∈ ( 0 ..^ 5 ) → ( ( 𝑦 − 𝑦 ) − ( 2 + 1 ) ) = ( 0 − 3 ) )
61 df-neg ⊢ - 3 = ( 0 − 3 )
62 60 61 eqtr4di ⊢ ( 𝑦 ∈ ( 0 ..^ 5 ) → ( ( 𝑦 − 𝑦 ) − ( 2 + 1 ) ) = - 3 )
63 56 62 eqtrd ⊢ ( 𝑦 ∈ ( 0 ..^ 5 ) → ( ( 𝑦 − 2 ) − ( 𝑦 + 1 ) ) = - 3 )
64 63 oveq1d ⊢ ( 𝑦 ∈ ( 0 ..^ 5 ) → ( ( ( 𝑦 − 2 ) − ( 𝑦 + 1 ) ) mod 5 ) = ( - 3 mod 5 ) )
65 64 eqeq1d ⊢ ( 𝑦 ∈ ( 0 ..^ 5 ) → ( ( ( ( 𝑦 − 2 ) − ( 𝑦 + 1 ) ) mod 5 ) = 0 ↔ ( - 3 mod 5 ) = 0 ) )
66 43 52 65 3bitr2d ⊢ ( 𝑦 ∈ ( 0 ..^ 5 ) → ( ( ( 𝑦 + 1 ) mod 5 ) = ( ( 𝑦 − 2 ) mod 5 ) ↔ ( - 3 mod 5 ) = 0 ) )
67 3re ⊢ 3 ∈ ℝ
68 5rp ⊢ 5 ∈ ℝ+
69 negmod0 ⊢ ( ( 3 ∈ ℝ ∧ 5 ∈ ℝ+ ) → ( ( 3 mod 5 ) = 0 ↔ ( - 3 mod 5 ) = 0 ) )
70 67 68 69 mp2an ⊢ ( ( 3 mod 5 ) = 0 ↔ ( - 3 mod 5 ) = 0 )
71 0re ⊢ 0 ∈ ℝ
72 3pos ⊢ 0 < 3
73 71 67 72 ltleii ⊢ 0 ≤ 3
74 3lt5 ⊢ 3 < 5
75 modid ⊢ ( ( ( 3 ∈ ℝ ∧ 5 ∈ ℝ+ ) ∧ ( 0 ≤ 3 ∧ 3 < 5 ) ) → ( 3 mod 5 ) = 3 )
76 67 68 73 74 75 mp4an ⊢ ( 3 mod 5 ) = 3
77 76 eqeq1i ⊢ ( ( 3 mod 5 ) = 0 ↔ 3 = 0 )
78 70 77 bitr3i ⊢ ( ( - 3 mod 5 ) = 0 ↔ 3 = 0 )
79 3ne0 ⊢ 3 ≠ 0
80 eqneqall ⊢ ( 3 = 0 → ( 3 ≠ 0 → ¬ { ⟨ 0 , 𝑏 ⟩ , ⟨ 1 , ( ( 𝑦 − 2 ) mod 5 ) ⟩ } ∈ 𝐸 ) )
81 79 80 mpi ⊢ ( 3 = 0 → ¬ { ⟨ 0 , 𝑏 ⟩ , ⟨ 1 , ( ( 𝑦 − 2 ) mod 5 ) ⟩ } ∈ 𝐸 )
82 78 81 sylbi ⊢ ( ( - 3 mod 5 ) = 0 → ¬ { ⟨ 0 , 𝑏 ⟩ , ⟨ 1 , ( ( 𝑦 − 2 ) mod 5 ) ⟩ } ∈ 𝐸 )
83 66 82 biimtrdi ⊢ ( 𝑦 ∈ ( 0 ..^ 5 ) → ( ( ( 𝑦 + 1 ) mod 5 ) = ( ( 𝑦 − 2 ) mod 5 ) → ¬ { ⟨ 0 , 𝑏 ⟩ , ⟨ 1 , ( ( 𝑦 − 2 ) mod 5 ) ⟩ } ∈ 𝐸 ) )
84 83 ad2antll ⊢ ( ( 𝑏 = ( ( 𝑦 + 1 ) mod 5 ) ∧ ( 𝑏 ∈ ( 0 ..^ 5 ) ∧ 𝑦 ∈ ( 0 ..^ 5 ) ) ) → ( ( ( 𝑦 + 1 ) mod 5 ) = ( ( 𝑦 − 2 ) mod 5 ) → ¬ { ⟨ 0 , 𝑏 ⟩ , ⟨ 1 , ( ( 𝑦 − 2 ) mod 5 ) ⟩ } ∈ 𝐸 ) )
85 41 84 sylbid ⊢ ( ( 𝑏 = ( ( 𝑦 + 1 ) mod 5 ) ∧ ( 𝑏 ∈ ( 0 ..^ 5 ) ∧ 𝑦 ∈ ( 0 ..^ 5 ) ) ) → ( 𝑏 = ( ( 𝑦 − 2 ) mod 5 ) → ¬ { ⟨ 0 , 𝑏 ⟩ , ⟨ 1 , ( ( 𝑦 − 2 ) mod 5 ) ⟩ } ∈ 𝐸 ) )
86 85 ex ⊢ ( 𝑏 = ( ( 𝑦 + 1 ) mod 5 ) → ( ( 𝑏 ∈ ( 0 ..^ 5 ) ∧ 𝑦 ∈ ( 0 ..^ 5 ) ) → ( 𝑏 = ( ( 𝑦 − 2 ) mod 5 ) → ¬ { ⟨ 0 , 𝑏 ⟩ , ⟨ 1 , ( ( 𝑦 − 2 ) mod 5 ) ⟩ } ∈ 𝐸 ) ) )
87 39 86 simplbiim ⊢ ( ⟨ 0 , 𝑏 ⟩ = ⟨ 0 , ( ( ( 2nd ‘ ⟨ 0 , 𝑦 ⟩ ) + 1 ) mod 5 ) ⟩ → ( ( 𝑏 ∈ ( 0 ..^ 5 ) ∧ 𝑦 ∈ ( 0 ..^ 5 ) ) → ( 𝑏 = ( ( 𝑦 − 2 ) mod 5 ) → ¬ { ⟨ 0 , 𝑏 ⟩ , ⟨ 1 , ( ( 𝑦 − 2 ) mod 5 ) ⟩ } ∈ 𝐸 ) ) )
88 8 16 opth ⊢ ( ⟨ 0 , 𝑏 ⟩ = ⟨ 1 , ( 2nd ‘ ⟨ 0 , 𝑦 ⟩ ) ⟩ ↔ ( 0 = 1 ∧ 𝑏 = ( 2nd ‘ ⟨ 0 , 𝑦 ⟩ ) ) )
89 0ne1 ⊢ 0 ≠ 1
90 eqneqall ⊢ ( 0 = 1 → ( 0 ≠ 1 → ( ( 𝑏 ∈ ( 0 ..^ 5 ) ∧ 𝑦 ∈ ( 0 ..^ 5 ) ) → ( 𝑏 = ( ( 𝑦 − 2 ) mod 5 ) → ¬ { ⟨ 0 , 𝑏 ⟩ , ⟨ 1 , ( ( 𝑦 − 2 ) mod 5 ) ⟩ } ∈ 𝐸 ) ) ) )
91 89 90 mpi ⊢ ( 0 = 1 → ( ( 𝑏 ∈ ( 0 ..^ 5 ) ∧ 𝑦 ∈ ( 0 ..^ 5 ) ) → ( 𝑏 = ( ( 𝑦 − 2 ) mod 5 ) → ¬ { ⟨ 0 , 𝑏 ⟩ , ⟨ 1 , ( ( 𝑦 − 2 ) mod 5 ) ⟩ } ∈ 𝐸 ) ) )
92 91 adantr ⊢ ( ( 0 = 1 ∧ 𝑏 = ( 2nd ‘ ⟨ 0 , 𝑦 ⟩ ) ) → ( ( 𝑏 ∈ ( 0 ..^ 5 ) ∧ 𝑦 ∈ ( 0 ..^ 5 ) ) → ( 𝑏 = ( ( 𝑦 − 2 ) mod 5 ) → ¬ { ⟨ 0 , 𝑏 ⟩ , ⟨ 1 , ( ( 𝑦 − 2 ) mod 5 ) ⟩ } ∈ 𝐸 ) ) )
93 88 92 sylbi ⊢ ( ⟨ 0 , 𝑏 ⟩ = ⟨ 1 , ( 2nd ‘ ⟨ 0 , 𝑦 ⟩ ) ⟩ → ( ( 𝑏 ∈ ( 0 ..^ 5 ) ∧ 𝑦 ∈ ( 0 ..^ 5 ) ) → ( 𝑏 = ( ( 𝑦 − 2 ) mod 5 ) → ¬ { ⟨ 0 , 𝑏 ⟩ , ⟨ 1 , ( ( 𝑦 − 2 ) mod 5 ) ⟩ } ∈ 𝐸 ) ) )
94 33 oveq1i ⊢ ( ( 2nd ‘ ⟨ 0 , 𝑦 ⟩ ) − 1 ) = ( 𝑦 − 1 )
95 94 oveq1i ⊢ ( ( ( 2nd ‘ ⟨ 0 , 𝑦 ⟩ ) − 1 ) mod 5 ) = ( ( 𝑦 − 1 ) mod 5 )
96 95 opeq2i ⊢ ⟨ 0 , ( ( ( 2nd ‘ ⟨ 0 , 𝑦 ⟩ ) − 1 ) mod 5 ) ⟩ = ⟨ 0 , ( ( 𝑦 − 1 ) mod 5 ) ⟩
97 96 eqeq2i ⊢ ( ⟨ 0 , 𝑏 ⟩ = ⟨ 0 , ( ( ( 2nd ‘ ⟨ 0 , 𝑦 ⟩ ) − 1 ) mod 5 ) ⟩ ↔ ⟨ 0 , 𝑏 ⟩ = ⟨ 0 , ( ( 𝑦 − 1 ) mod 5 ) ⟩ )
98 8 16 opth ⊢ ( ⟨ 0 , 𝑏 ⟩ = ⟨ 0 , ( ( 𝑦 − 1 ) mod 5 ) ⟩ ↔ ( 0 = 0 ∧ 𝑏 = ( ( 𝑦 − 1 ) mod 5 ) ) )
99 eqeq1 ⊢ ( 𝑏 = ( ( 𝑦 − 1 ) mod 5 ) → ( 𝑏 = ( ( 𝑦 − 2 ) mod 5 ) ↔ ( ( 𝑦 − 1 ) mod 5 ) = ( ( 𝑦 − 2 ) mod 5 ) ) )
100 99 adantr ⊢ ( ( 𝑏 = ( ( 𝑦 − 1 ) mod 5 ) ∧ ( 𝑏 ∈ ( 0 ..^ 5 ) ∧ 𝑦 ∈ ( 0 ..^ 5 ) ) ) → ( 𝑏 = ( ( 𝑦 − 2 ) mod 5 ) ↔ ( ( 𝑦 − 1 ) mod 5 ) = ( ( 𝑦 − 2 ) mod 5 ) ) )
101 1zzd ⊢ ( 𝑦 ∈ ( 0 ..^ 5 ) → 1 ∈ ℤ )
102 44 101 zsubcld ⊢ ( 𝑦 ∈ ( 0 ..^ 5 ) → ( 𝑦 − 1 ) ∈ ℤ )
103 difmod0 ⊢ ( ( ( 𝑦 − 1 ) ∈ ℤ ∧ ( 𝑦 − 2 ) ∈ ℤ ∧ 5 ∈ ℕ ) → ( ( ( ( 𝑦 − 1 ) − ( 𝑦 − 2 ) ) mod 5 ) = 0 ↔ ( ( 𝑦 − 1 ) mod 5 ) = ( ( 𝑦 − 2 ) mod 5 ) ) )
104 103 bicomd ⊢ ( ( ( 𝑦 − 1 ) ∈ ℤ ∧ ( 𝑦 − 2 ) ∈ ℤ ∧ 5 ∈ ℕ ) → ( ( ( 𝑦 − 1 ) mod 5 ) = ( ( 𝑦 − 2 ) mod 5 ) ↔ ( ( ( 𝑦 − 1 ) − ( 𝑦 − 2 ) ) mod 5 ) = 0 ) )
105 102 47 50 104 syl3anc ⊢ ( 𝑦 ∈ ( 0 ..^ 5 ) → ( ( ( 𝑦 − 1 ) mod 5 ) = ( ( 𝑦 − 2 ) mod 5 ) ↔ ( ( ( 𝑦 − 1 ) − ( 𝑦 − 2 ) ) mod 5 ) = 0 ) )
106 53 55 54 nnncan1d ⊢ ( 𝑦 ∈ ( 0 ..^ 5 ) → ( ( 𝑦 − 1 ) − ( 𝑦 − 2 ) ) = ( 2 − 1 ) )
107 2m1e1 ⊢ ( 2 − 1 ) = 1
108 106 107 eqtrdi ⊢ ( 𝑦 ∈ ( 0 ..^ 5 ) → ( ( 𝑦 − 1 ) − ( 𝑦 − 2 ) ) = 1 )
109 108 oveq1d ⊢ ( 𝑦 ∈ ( 0 ..^ 5 ) → ( ( ( 𝑦 − 1 ) − ( 𝑦 − 2 ) ) mod 5 ) = ( 1 mod 5 ) )
110 109 eqeq1d ⊢ ( 𝑦 ∈ ( 0 ..^ 5 ) → ( ( ( ( 𝑦 − 1 ) − ( 𝑦 − 2 ) ) mod 5 ) = 0 ↔ ( 1 mod 5 ) = 0 ) )
111 1re ⊢ 1 ∈ ℝ
112 0le1 ⊢ 0 ≤ 1
113 1lt5 ⊢ 1 < 5
114 modid ⊢ ( ( ( 1 ∈ ℝ ∧ 5 ∈ ℝ+ ) ∧ ( 0 ≤ 1 ∧ 1 < 5 ) ) → ( 1 mod 5 ) = 1 )
115 111 68 112 113 114 mp4an ⊢ ( 1 mod 5 ) = 1
116 115 eqeq1i ⊢ ( ( 1 mod 5 ) = 0 ↔ 1 = 0 )
117 eqneqall ⊢ ( 1 = 0 → ( 1 ≠ 0 → ¬ { ⟨ 0 , 𝑏 ⟩ , ⟨ 1 , ( ( 𝑦 − 2 ) mod 5 ) ⟩ } ∈ 𝐸 ) )
118 23 117 mpi ⊢ ( 1 = 0 → ¬ { ⟨ 0 , 𝑏 ⟩ , ⟨ 1 , ( ( 𝑦 − 2 ) mod 5 ) ⟩ } ∈ 𝐸 )
119 116 118 sylbi ⊢ ( ( 1 mod 5 ) = 0 → ¬ { ⟨ 0 , 𝑏 ⟩ , ⟨ 1 , ( ( 𝑦 − 2 ) mod 5 ) ⟩ } ∈ 𝐸 )
120 110 119 biimtrdi ⊢ ( 𝑦 ∈ ( 0 ..^ 5 ) → ( ( ( ( 𝑦 − 1 ) − ( 𝑦 − 2 ) ) mod 5 ) = 0 → ¬ { ⟨ 0 , 𝑏 ⟩ , ⟨ 1 , ( ( 𝑦 − 2 ) mod 5 ) ⟩ } ∈ 𝐸 ) )
121 105 120 sylbid ⊢ ( 𝑦 ∈ ( 0 ..^ 5 ) → ( ( ( 𝑦 − 1 ) mod 5 ) = ( ( 𝑦 − 2 ) mod 5 ) → ¬ { ⟨ 0 , 𝑏 ⟩ , ⟨ 1 , ( ( 𝑦 − 2 ) mod 5 ) ⟩ } ∈ 𝐸 ) )
122 121 ad2antll ⊢ ( ( 𝑏 = ( ( 𝑦 − 1 ) mod 5 ) ∧ ( 𝑏 ∈ ( 0 ..^ 5 ) ∧ 𝑦 ∈ ( 0 ..^ 5 ) ) ) → ( ( ( 𝑦 − 1 ) mod 5 ) = ( ( 𝑦 − 2 ) mod 5 ) → ¬ { ⟨ 0 , 𝑏 ⟩ , ⟨ 1 , ( ( 𝑦 − 2 ) mod 5 ) ⟩ } ∈ 𝐸 ) )
123 100 122 sylbid ⊢ ( ( 𝑏 = ( ( 𝑦 − 1 ) mod 5 ) ∧ ( 𝑏 ∈ ( 0 ..^ 5 ) ∧ 𝑦 ∈ ( 0 ..^ 5 ) ) ) → ( 𝑏 = ( ( 𝑦 − 2 ) mod 5 ) → ¬ { ⟨ 0 , 𝑏 ⟩ , ⟨ 1 , ( ( 𝑦 − 2 ) mod 5 ) ⟩ } ∈ 𝐸 ) )
124 123 ex ⊢ ( 𝑏 = ( ( 𝑦 − 1 ) mod 5 ) → ( ( 𝑏 ∈ ( 0 ..^ 5 ) ∧ 𝑦 ∈ ( 0 ..^ 5 ) ) → ( 𝑏 = ( ( 𝑦 − 2 ) mod 5 ) → ¬ { ⟨ 0 , 𝑏 ⟩ , ⟨ 1 , ( ( 𝑦 − 2 ) mod 5 ) ⟩ } ∈ 𝐸 ) ) )
125 98 124 simplbiim ⊢ ( ⟨ 0 , 𝑏 ⟩ = ⟨ 0 , ( ( 𝑦 − 1 ) mod 5 ) ⟩ → ( ( 𝑏 ∈ ( 0 ..^ 5 ) ∧ 𝑦 ∈ ( 0 ..^ 5 ) ) → ( 𝑏 = ( ( 𝑦 − 2 ) mod 5 ) → ¬ { ⟨ 0 , 𝑏 ⟩ , ⟨ 1 , ( ( 𝑦 − 2 ) mod 5 ) ⟩ } ∈ 𝐸 ) ) )
126 97 125 sylbi ⊢ ( ⟨ 0 , 𝑏 ⟩ = ⟨ 0 , ( ( ( 2nd ‘ ⟨ 0 , 𝑦 ⟩ ) − 1 ) mod 5 ) ⟩ → ( ( 𝑏 ∈ ( 0 ..^ 5 ) ∧ 𝑦 ∈ ( 0 ..^ 5 ) ) → ( 𝑏 = ( ( 𝑦 − 2 ) mod 5 ) → ¬ { ⟨ 0 , 𝑏 ⟩ , ⟨ 1 , ( ( 𝑦 − 2 ) mod 5 ) ⟩ } ∈ 𝐸 ) ) )
127 87 93 126 3jaoi ⊢ ( ( ⟨ 0 , 𝑏 ⟩ = ⟨ 0 , ( ( ( 2nd ‘ ⟨ 0 , 𝑦 ⟩ ) + 1 ) mod 5 ) ⟩ ∨ ⟨ 0 , 𝑏 ⟩ = ⟨ 1 , ( 2nd ‘ ⟨ 0 , 𝑦 ⟩ ) ⟩ ∨ ⟨ 0 , 𝑏 ⟩ = ⟨ 0 , ( ( ( 2nd ‘ ⟨ 0 , 𝑦 ⟩ ) − 1 ) mod 5 ) ⟩ ) → ( ( 𝑏 ∈ ( 0 ..^ 5 ) ∧ 𝑦 ∈ ( 0 ..^ 5 ) ) → ( 𝑏 = ( ( 𝑦 − 2 ) mod 5 ) → ¬ { ⟨ 0 , 𝑏 ⟩ , ⟨ 1 , ( ( 𝑦 − 2 ) mod 5 ) ⟩ } ∈ 𝐸 ) ) )
128 127 com13 ⊢ ( 𝑏 = ( ( 𝑦 − 2 ) mod 5 ) → ( ( 𝑏 ∈ ( 0 ..^ 5 ) ∧ 𝑦 ∈ ( 0 ..^ 5 ) ) → ( ( ⟨ 0 , 𝑏 ⟩ = ⟨ 0 , ( ( ( 2nd ‘ ⟨ 0 , 𝑦 ⟩ ) + 1 ) mod 5 ) ⟩ ∨ ⟨ 0 , 𝑏 ⟩ = ⟨ 1 , ( 2nd ‘ ⟨ 0 , 𝑦 ⟩ ) ⟩ ∨ ⟨ 0 , 𝑏 ⟩ = ⟨ 0 , ( ( ( 2nd ‘ ⟨ 0 , 𝑦 ⟩ ) − 1 ) mod 5 ) ⟩ ) → ¬ { ⟨ 0 , 𝑏 ⟩ , ⟨ 1 , ( ( 𝑦 − 2 ) mod 5 ) ⟩ } ∈ 𝐸 ) ) )
129 128 impd ⊢ ( 𝑏 = ( ( 𝑦 − 2 ) mod 5 ) → ( ( ( 𝑏 ∈ ( 0 ..^ 5 ) ∧ 𝑦 ∈ ( 0 ..^ 5 ) ) ∧ ( ⟨ 0 , 𝑏 ⟩ = ⟨ 0 , ( ( ( 2nd ‘ ⟨ 0 , 𝑦 ⟩ ) + 1 ) mod 5 ) ⟩ ∨ ⟨ 0 , 𝑏 ⟩ = ⟨ 1 , ( 2nd ‘ ⟨ 0 , 𝑦 ⟩ ) ⟩ ∨ ⟨ 0 , 𝑏 ⟩ = ⟨ 0 , ( ( ( 2nd ‘ ⟨ 0 , 𝑦 ⟩ ) − 1 ) mod 5 ) ⟩ ) ) → ¬ { ⟨ 0 , 𝑏 ⟩ , ⟨ 1 , ( ( 𝑦 − 2 ) mod 5 ) ⟩ } ∈ 𝐸 ) )
130 32 129 sylbi ⊢ ( ( ( 𝑦 − 2 ) mod 5 ) = ( 2nd ‘ ⟨ 0 , 𝑏 ⟩ ) → ( ( ( 𝑏 ∈ ( 0 ..^ 5 ) ∧ 𝑦 ∈ ( 0 ..^ 5 ) ) ∧ ( ⟨ 0 , 𝑏 ⟩ = ⟨ 0 , ( ( ( 2nd ‘ ⟨ 0 , 𝑦 ⟩ ) + 1 ) mod 5 ) ⟩ ∨ ⟨ 0 , 𝑏 ⟩ = ⟨ 1 , ( 2nd ‘ ⟨ 0 , 𝑦 ⟩ ) ⟩ ∨ ⟨ 0 , 𝑏 ⟩ = ⟨ 0 , ( ( ( 2nd ‘ ⟨ 0 , 𝑦 ⟩ ) − 1 ) mod 5 ) ⟩ ) ) → ¬ { ⟨ 0 , 𝑏 ⟩ , ⟨ 1 , ( ( 𝑦 − 2 ) mod 5 ) ⟩ } ∈ 𝐸 ) )
131 28 130 simplbiim ⊢ ( ⟨ 1 , ( ( 𝑦 − 2 ) mod 5 ) ⟩ = ⟨ 1 , ( 2nd ‘ ⟨ 0 , 𝑏 ⟩ ) ⟩ → ( ( ( 𝑏 ∈ ( 0 ..^ 5 ) ∧ 𝑦 ∈ ( 0 ..^ 5 ) ) ∧ ( ⟨ 0 , 𝑏 ⟩ = ⟨ 0 , ( ( ( 2nd ‘ ⟨ 0 , 𝑦 ⟩ ) + 1 ) mod 5 ) ⟩ ∨ ⟨ 0 , 𝑏 ⟩ = ⟨ 1 , ( 2nd ‘ ⟨ 0 , 𝑦 ⟩ ) ⟩ ∨ ⟨ 0 , 𝑏 ⟩ = ⟨ 0 , ( ( ( 2nd ‘ ⟨ 0 , 𝑦 ⟩ ) − 1 ) mod 5 ) ⟩ ) ) → ¬ { ⟨ 0 , 𝑏 ⟩ , ⟨ 1 , ( ( 𝑦 − 2 ) mod 5 ) ⟩ } ∈ 𝐸 ) )
132 20 21 opth ⊢ ( ⟨ 1 , ( ( 𝑦 − 2 ) mod 5 ) ⟩ = ⟨ 0 , ( ( ( 2nd ‘ ⟨ 0 , 𝑏 ⟩ ) − 1 ) mod 5 ) ⟩ ↔ ( 1 = 0 ∧ ( ( 𝑦 − 2 ) mod 5 ) = ( ( ( 2nd ‘ ⟨ 0 , 𝑏 ⟩ ) − 1 ) mod 5 ) ) )
133 25 adantr ⊢ ( ( 1 = 0 ∧ ( ( 𝑦 − 2 ) mod 5 ) = ( ( ( 2nd ‘ ⟨ 0 , 𝑏 ⟩ ) − 1 ) mod 5 ) ) → ( ( ( 𝑏 ∈ ( 0 ..^ 5 ) ∧ 𝑦 ∈ ( 0 ..^ 5 ) ) ∧ ( ⟨ 0 , 𝑏 ⟩ = ⟨ 0 , ( ( ( 2nd ‘ ⟨ 0 , 𝑦 ⟩ ) + 1 ) mod 5 ) ⟩ ∨ ⟨ 0 , 𝑏 ⟩ = ⟨ 1 , ( 2nd ‘ ⟨ 0 , 𝑦 ⟩ ) ⟩ ∨ ⟨ 0 , 𝑏 ⟩ = ⟨ 0 , ( ( ( 2nd ‘ ⟨ 0 , 𝑦 ⟩ ) − 1 ) mod 5 ) ⟩ ) ) → ¬ { ⟨ 0 , 𝑏 ⟩ , ⟨ 1 , ( ( 𝑦 − 2 ) mod 5 ) ⟩ } ∈ 𝐸 ) )
134 132 133 sylbi ⊢ ( ⟨ 1 , ( ( 𝑦 − 2 ) mod 5 ) ⟩ = ⟨ 0 , ( ( ( 2nd ‘ ⟨ 0 , 𝑏 ⟩ ) − 1 ) mod 5 ) ⟩ → ( ( ( 𝑏 ∈ ( 0 ..^ 5 ) ∧ 𝑦 ∈ ( 0 ..^ 5 ) ) ∧ ( ⟨ 0 , 𝑏 ⟩ = ⟨ 0 , ( ( ( 2nd ‘ ⟨ 0 , 𝑦 ⟩ ) + 1 ) mod 5 ) ⟩ ∨ ⟨ 0 , 𝑏 ⟩ = ⟨ 1 , ( 2nd ‘ ⟨ 0 , 𝑦 ⟩ ) ⟩ ∨ ⟨ 0 , 𝑏 ⟩ = ⟨ 0 , ( ( ( 2nd ‘ ⟨ 0 , 𝑦 ⟩ ) − 1 ) mod 5 ) ⟩ ) ) → ¬ { ⟨ 0 , 𝑏 ⟩ , ⟨ 1 , ( ( 𝑦 − 2 ) mod 5 ) ⟩ } ∈ 𝐸 ) )
135 27 131 134 3jaoi ⊢ ( ( ⟨ 1 , ( ( 𝑦 − 2 ) mod 5 ) ⟩ = ⟨ 0 , ( ( ( 2nd ‘ ⟨ 0 , 𝑏 ⟩ ) + 1 ) mod 5 ) ⟩ ∨ ⟨ 1 , ( ( 𝑦 − 2 ) mod 5 ) ⟩ = ⟨ 1 , ( 2nd ‘ ⟨ 0 , 𝑏 ⟩ ) ⟩ ∨ ⟨ 1 , ( ( 𝑦 − 2 ) mod 5 ) ⟩ = ⟨ 0 , ( ( ( 2nd ‘ ⟨ 0 , 𝑏 ⟩ ) − 1 ) mod 5 ) ⟩ ) → ( ( ( 𝑏 ∈ ( 0 ..^ 5 ) ∧ 𝑦 ∈ ( 0 ..^ 5 ) ) ∧ ( ⟨ 0 , 𝑏 ⟩ = ⟨ 0 , ( ( ( 2nd ‘ ⟨ 0 , 𝑦 ⟩ ) + 1 ) mod 5 ) ⟩ ∨ ⟨ 0 , 𝑏 ⟩ = ⟨ 1 , ( 2nd ‘ ⟨ 0 , 𝑦 ⟩ ) ⟩ ∨ ⟨ 0 , 𝑏 ⟩ = ⟨ 0 , ( ( ( 2nd ‘ ⟨ 0 , 𝑦 ⟩ ) − 1 ) mod 5 ) ⟩ ) ) → ¬ { ⟨ 0 , 𝑏 ⟩ , ⟨ 1 , ( ( 𝑦 − 2 ) mod 5 ) ⟩ } ∈ 𝐸 ) )
136 19 135 syl ⊢ ( { ⟨ 0 , 𝑏 ⟩ , ⟨ 1 , ( ( 𝑦 − 2 ) mod 5 ) ⟩ } ∈ 𝐸 → ( ( ( 𝑏 ∈ ( 0 ..^ 5 ) ∧ 𝑦 ∈ ( 0 ..^ 5 ) ) ∧ ( ⟨ 0 , 𝑏 ⟩ = ⟨ 0 , ( ( ( 2nd ‘ ⟨ 0 , 𝑦 ⟩ ) + 1 ) mod 5 ) ⟩ ∨ ⟨ 0 , 𝑏 ⟩ = ⟨ 1 , ( 2nd ‘ ⟨ 0 , 𝑦 ⟩ ) ⟩ ∨ ⟨ 0 , 𝑏 ⟩ = ⟨ 0 , ( ( ( 2nd ‘ ⟨ 0 , 𝑦 ⟩ ) − 1 ) mod 5 ) ⟩ ) ) → ¬ { ⟨ 0 , 𝑏 ⟩ , ⟨ 1 , ( ( 𝑦 − 2 ) mod 5 ) ⟩ } ∈ 𝐸 ) )
137 ax-1 ⊢ ( ¬ { ⟨ 0 , 𝑏 ⟩ , ⟨ 1 , ( ( 𝑦 − 2 ) mod 5 ) ⟩ } ∈ 𝐸 → ( ( ( 𝑏 ∈ ( 0 ..^ 5 ) ∧ 𝑦 ∈ ( 0 ..^ 5 ) ) ∧ ( ⟨ 0 , 𝑏 ⟩ = ⟨ 0 , ( ( ( 2nd ‘ ⟨ 0 , 𝑦 ⟩ ) + 1 ) mod 5 ) ⟩ ∨ ⟨ 0 , 𝑏 ⟩ = ⟨ 1 , ( 2nd ‘ ⟨ 0 , 𝑦 ⟩ ) ⟩ ∨ ⟨ 0 , 𝑏 ⟩ = ⟨ 0 , ( ( ( 2nd ‘ ⟨ 0 , 𝑦 ⟩ ) − 1 ) mod 5 ) ⟩ ) ) → ¬ { ⟨ 0 , 𝑏 ⟩ , ⟨ 1 , ( ( 𝑦 − 2 ) mod 5 ) ⟩ } ∈ 𝐸 ) )
138 136 137 pm2.61i ⊢ ( ( ( 𝑏 ∈ ( 0 ..^ 5 ) ∧ 𝑦 ∈ ( 0 ..^ 5 ) ) ∧ ( ⟨ 0 , 𝑏 ⟩ = ⟨ 0 , ( ( ( 2nd ‘ ⟨ 0 , 𝑦 ⟩ ) + 1 ) mod 5 ) ⟩ ∨ ⟨ 0 , 𝑏 ⟩ = ⟨ 1 , ( 2nd ‘ ⟨ 0 , 𝑦 ⟩ ) ⟩ ∨ ⟨ 0 , 𝑏 ⟩ = ⟨ 0 , ( ( ( 2nd ‘ ⟨ 0 , 𝑦 ⟩ ) − 1 ) mod 5 ) ⟩ ) ) → ¬ { ⟨ 0 , 𝑏 ⟩ , ⟨ 1 , ( ( 𝑦 − 2 ) mod 5 ) ⟩ } ∈ 𝐸 )
139 138 ex ⊢ ( ( 𝑏 ∈ ( 0 ..^ 5 ) ∧ 𝑦 ∈ ( 0 ..^ 5 ) ) → ( ( ⟨ 0 , 𝑏 ⟩ = ⟨ 0 , ( ( ( 2nd ‘ ⟨ 0 , 𝑦 ⟩ ) + 1 ) mod 5 ) ⟩ ∨ ⟨ 0 , 𝑏 ⟩ = ⟨ 1 , ( 2nd ‘ ⟨ 0 , 𝑦 ⟩ ) ⟩ ∨ ⟨ 0 , 𝑏 ⟩ = ⟨ 0 , ( ( ( 2nd ‘ ⟨ 0 , 𝑦 ⟩ ) − 1 ) mod 5 ) ⟩ ) → ¬ { ⟨ 0 , 𝑏 ⟩ , ⟨ 1 , ( ( 𝑦 − 2 ) mod 5 ) ⟩ } ∈ 𝐸 ) )
140 15 139 syld ⊢ ( ( 𝑏 ∈ ( 0 ..^ 5 ) ∧ 𝑦 ∈ ( 0 ..^ 5 ) ) → ( { ⟨ 0 , 𝑦 ⟩ , ⟨ 0 , 𝑏 ⟩ } ∈ 𝐸 → ¬ { ⟨ 0 , 𝑏 ⟩ , ⟨ 1 , ( ( 𝑦 − 2 ) mod 5 ) ⟩ } ∈ 𝐸 ) )
141 140 adantl ⊢ ( ( ( 𝐿 = ⟨ 1 , ( ( 𝑦 − 2 ) mod 5 ) ⟩ ∧ 𝐾 = ⟨ 0 , 𝑦 ⟩ ) ∧ ( 𝑏 ∈ ( 0 ..^ 5 ) ∧ 𝑦 ∈ ( 0 ..^ 5 ) ) ) → ( { ⟨ 0 , 𝑦 ⟩ , ⟨ 0 , 𝑏 ⟩ } ∈ 𝐸 → ¬ { ⟨ 0 , 𝑏 ⟩ , ⟨ 1 , ( ( 𝑦 − 2 ) mod 5 ) ⟩ } ∈ 𝐸 ) )
142 preq1 ⊢ ( 𝐾 = ⟨ 0 , 𝑦 ⟩ → { 𝐾 , ⟨ 0 , 𝑏 ⟩ } = { ⟨ 0 , 𝑦 ⟩ , ⟨ 0 , 𝑏 ⟩ } )
143 142 eleq1d ⊢ ( 𝐾 = ⟨ 0 , 𝑦 ⟩ → ( { 𝐾 , ⟨ 0 , 𝑏 ⟩ } ∈ 𝐸 ↔ { ⟨ 0 , 𝑦 ⟩ , ⟨ 0 , 𝑏 ⟩ } ∈ 𝐸 ) )
144 143 adantl ⊢ ( ( 𝐿 = ⟨ 1 , ( ( 𝑦 − 2 ) mod 5 ) ⟩ ∧ 𝐾 = ⟨ 0 , 𝑦 ⟩ ) → ( { 𝐾 , ⟨ 0 , 𝑏 ⟩ } ∈ 𝐸 ↔ { ⟨ 0 , 𝑦 ⟩ , ⟨ 0 , 𝑏 ⟩ } ∈ 𝐸 ) )
145 preq2 ⊢ ( 𝐿 = ⟨ 1 , ( ( 𝑦 − 2 ) mod 5 ) ⟩ → { ⟨ 0 , 𝑏 ⟩ , 𝐿 } = { ⟨ 0 , 𝑏 ⟩ , ⟨ 1 , ( ( 𝑦 − 2 ) mod 5 ) ⟩ } )
146 145 eleq1d ⊢ ( 𝐿 = ⟨ 1 , ( ( 𝑦 − 2 ) mod 5 ) ⟩ → ( { ⟨ 0 , 𝑏 ⟩ , 𝐿 } ∈ 𝐸 ↔ { ⟨ 0 , 𝑏 ⟩ , ⟨ 1 , ( ( 𝑦 − 2 ) mod 5 ) ⟩ } ∈ 𝐸 ) )
147 146 notbid ⊢ ( 𝐿 = ⟨ 1 , ( ( 𝑦 − 2 ) mod 5 ) ⟩ → ( ¬ { ⟨ 0 , 𝑏 ⟩ , 𝐿 } ∈ 𝐸 ↔ ¬ { ⟨ 0 , 𝑏 ⟩ , ⟨ 1 , ( ( 𝑦 − 2 ) mod 5 ) ⟩ } ∈ 𝐸 ) )
148 147 adantr ⊢ ( ( 𝐿 = ⟨ 1 , ( ( 𝑦 − 2 ) mod 5 ) ⟩ ∧ 𝐾 = ⟨ 0 , 𝑦 ⟩ ) → ( ¬ { ⟨ 0 , 𝑏 ⟩ , 𝐿 } ∈ 𝐸 ↔ ¬ { ⟨ 0 , 𝑏 ⟩ , ⟨ 1 , ( ( 𝑦 − 2 ) mod 5 ) ⟩ } ∈ 𝐸 ) )
149 144 148 imbi12d ⊢ ( ( 𝐿 = ⟨ 1 , ( ( 𝑦 − 2 ) mod 5 ) ⟩ ∧ 𝐾 = ⟨ 0 , 𝑦 ⟩ ) → ( ( { 𝐾 , ⟨ 0 , 𝑏 ⟩ } ∈ 𝐸 → ¬ { ⟨ 0 , 𝑏 ⟩ , 𝐿 } ∈ 𝐸 ) ↔ ( { ⟨ 0 , 𝑦 ⟩ , ⟨ 0 , 𝑏 ⟩ } ∈ 𝐸 → ¬ { ⟨ 0 , 𝑏 ⟩ , ⟨ 1 , ( ( 𝑦 − 2 ) mod 5 ) ⟩ } ∈ 𝐸 ) ) )
150 149 adantr ⊢ ( ( ( 𝐿 = ⟨ 1 , ( ( 𝑦 − 2 ) mod 5 ) ⟩ ∧ 𝐾 = ⟨ 0 , 𝑦 ⟩ ) ∧ ( 𝑏 ∈ ( 0 ..^ 5 ) ∧ 𝑦 ∈ ( 0 ..^ 5 ) ) ) → ( ( { 𝐾 , ⟨ 0 , 𝑏 ⟩ } ∈ 𝐸 → ¬ { ⟨ 0 , 𝑏 ⟩ , 𝐿 } ∈ 𝐸 ) ↔ ( { ⟨ 0 , 𝑦 ⟩ , ⟨ 0 , 𝑏 ⟩ } ∈ 𝐸 → ¬ { ⟨ 0 , 𝑏 ⟩ , ⟨ 1 , ( ( 𝑦 − 2 ) mod 5 ) ⟩ } ∈ 𝐸 ) ) )
151 141 150 mpbird ⊢ ( ( ( 𝐿 = ⟨ 1 , ( ( 𝑦 − 2 ) mod 5 ) ⟩ ∧ 𝐾 = ⟨ 0 , 𝑦 ⟩ ) ∧ ( 𝑏 ∈ ( 0 ..^ 5 ) ∧ 𝑦 ∈ ( 0 ..^ 5 ) ) ) → ( { 𝐾 , ⟨ 0 , 𝑏 ⟩ } ∈ 𝐸 → ¬ { ⟨ 0 , 𝑏 ⟩ , 𝐿 } ∈ 𝐸 ) )
152 151 imp ⊢ ( ( ( ( 𝐿 = ⟨ 1 , ( ( 𝑦 − 2 ) mod 5 ) ⟩ ∧ 𝐾 = ⟨ 0 , 𝑦 ⟩ ) ∧ ( 𝑏 ∈ ( 0 ..^ 5 ) ∧ 𝑦 ∈ ( 0 ..^ 5 ) ) ) ∧ { 𝐾 , ⟨ 0 , 𝑏 ⟩ } ∈ 𝐸 ) → ¬ { ⟨ 0 , 𝑏 ⟩ , 𝐿 } ∈ 𝐸 )