Metamath Proof Explorer

Theorem pgnbgreunbgrlem2lem1

Description: Lemma 1 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 pgnbgreunbgrlem2lem1 ( ( ( ( 𝐿 = ⟨ 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 zaddcld ⊢ ( 𝑦 ∈ ( 0 ..^ 5 ) → ( 𝑦 + 2 ) ∈ ℤ )
48 1zzd ⊢ ( 𝑦 ∈ ( 0 ..^ 5 ) → 1 ∈ ℤ )
49 44 48 zaddcld ⊢ ( 𝑦 ∈ ( 0 ..^ 5 ) → ( 𝑦 + 1 ) ∈ ℤ )
50 5nn ⊢ 5 ∈ ℕ
51 50 a1i ⊢ ( 𝑦 ∈ ( 0 ..^ 5 ) → 5 ∈ ℕ )
52 difmod0 ⊢ ( ( ( 𝑦 + 2 ) ∈ ℤ ∧ ( 𝑦 + 1 ) ∈ ℤ ∧ 5 ∈ ℕ ) → ( ( ( ( 𝑦 + 2 ) − ( 𝑦 + 1 ) ) mod 5 ) = 0 ↔ ( ( 𝑦 + 2 ) mod 5 ) = ( ( 𝑦 + 1 ) mod 5 ) ) )
53 47 49 51 52 syl3anc ⊢ ( 𝑦 ∈ ( 0 ..^ 5 ) → ( ( ( ( 𝑦 + 2 ) − ( 𝑦 + 1 ) ) mod 5 ) = 0 ↔ ( ( 𝑦 + 2 ) mod 5 ) = ( ( 𝑦 + 1 ) mod 5 ) ) )
54 44 zcnd ⊢ ( 𝑦 ∈ ( 0 ..^ 5 ) → 𝑦 ∈ ℂ )
55 2cnd ⊢ ( 𝑦 ∈ ( 0 ..^ 5 ) → 2 ∈ ℂ )
56 1cnd ⊢ ( 𝑦 ∈ ( 0 ..^ 5 ) → 1 ∈ ℂ )
57 54 55 56 pnpcand ⊢ ( 𝑦 ∈ ( 0 ..^ 5 ) → ( ( 𝑦 + 2 ) − ( 𝑦 + 1 ) ) = ( 2 − 1 ) )
58 2m1e1 ⊢ ( 2 − 1 ) = 1
59 57 58 eqtrdi ⊢ ( 𝑦 ∈ ( 0 ..^ 5 ) → ( ( 𝑦 + 2 ) − ( 𝑦 + 1 ) ) = 1 )
60 59 oveq1d ⊢ ( 𝑦 ∈ ( 0 ..^ 5 ) → ( ( ( 𝑦 + 2 ) − ( 𝑦 + 1 ) ) mod 5 ) = ( 1 mod 5 ) )
61 60 eqeq1d ⊢ ( 𝑦 ∈ ( 0 ..^ 5 ) → ( ( ( ( 𝑦 + 2 ) − ( 𝑦 + 1 ) ) mod 5 ) = 0 ↔ ( 1 mod 5 ) = 0 ) )
62 43 53 61 3bitr2d ⊢ ( 𝑦 ∈ ( 0 ..^ 5 ) → ( ( ( 𝑦 + 1 ) mod 5 ) = ( ( 𝑦 + 2 ) mod 5 ) ↔ ( 1 mod 5 ) = 0 ) )
63 1re ⊢ 1 ∈ ℝ
64 5rp ⊢ 5 ∈ ℝ+
65 0le1 ⊢ 0 ≤ 1
66 1lt5 ⊢ 1 < 5
67 modid ⊢ ( ( ( 1 ∈ ℝ ∧ 5 ∈ ℝ+ ) ∧ ( 0 ≤ 1 ∧ 1 < 5 ) ) → ( 1 mod 5 ) = 1 )
68 63 64 65 66 67 mp4an ⊢ ( 1 mod 5 ) = 1
69 68 eqeq1i ⊢ ( ( 1 mod 5 ) = 0 ↔ 1 = 0 )
70 eqneqall ⊢ ( 1 = 0 → ( 1 ≠ 0 → ¬ { ⟨ 0 , 𝑏 ⟩ , ⟨ 1 , ( ( 𝑦 + 2 ) mod 5 ) ⟩ } ∈ 𝐸 ) )
71 23 70 mpi ⊢ ( 1 = 0 → ¬ { ⟨ 0 , 𝑏 ⟩ , ⟨ 1 , ( ( 𝑦 + 2 ) mod 5 ) ⟩ } ∈ 𝐸 )
72 69 71 sylbi ⊢ ( ( 1 mod 5 ) = 0 → ¬ { ⟨ 0 , 𝑏 ⟩ , ⟨ 1 , ( ( 𝑦 + 2 ) mod 5 ) ⟩ } ∈ 𝐸 )
73 62 72 biimtrdi ⊢ ( 𝑦 ∈ ( 0 ..^ 5 ) → ( ( ( 𝑦 + 1 ) mod 5 ) = ( ( 𝑦 + 2 ) mod 5 ) → ¬ { ⟨ 0 , 𝑏 ⟩ , ⟨ 1 , ( ( 𝑦 + 2 ) mod 5 ) ⟩ } ∈ 𝐸 ) )
74 73 ad2antll ⊢ ( ( 𝑏 = ( ( 𝑦 + 1 ) mod 5 ) ∧ ( 𝑏 ∈ ( 0 ..^ 5 ) ∧ 𝑦 ∈ ( 0 ..^ 5 ) ) ) → ( ( ( 𝑦 + 1 ) mod 5 ) = ( ( 𝑦 + 2 ) mod 5 ) → ¬ { ⟨ 0 , 𝑏 ⟩ , ⟨ 1 , ( ( 𝑦 + 2 ) mod 5 ) ⟩ } ∈ 𝐸 ) )
75 41 74 sylbid ⊢ ( ( 𝑏 = ( ( 𝑦 + 1 ) mod 5 ) ∧ ( 𝑏 ∈ ( 0 ..^ 5 ) ∧ 𝑦 ∈ ( 0 ..^ 5 ) ) ) → ( 𝑏 = ( ( 𝑦 + 2 ) mod 5 ) → ¬ { ⟨ 0 , 𝑏 ⟩ , ⟨ 1 , ( ( 𝑦 + 2 ) mod 5 ) ⟩ } ∈ 𝐸 ) )
76 75 ex ⊢ ( 𝑏 = ( ( 𝑦 + 1 ) mod 5 ) → ( ( 𝑏 ∈ ( 0 ..^ 5 ) ∧ 𝑦 ∈ ( 0 ..^ 5 ) ) → ( 𝑏 = ( ( 𝑦 + 2 ) mod 5 ) → ¬ { ⟨ 0 , 𝑏 ⟩ , ⟨ 1 , ( ( 𝑦 + 2 ) mod 5 ) ⟩ } ∈ 𝐸 ) ) )
77 39 76 simplbiim ⊢ ( ⟨ 0 , 𝑏 ⟩ = ⟨ 0 , ( ( ( 2nd ‘ ⟨ 0 , 𝑦 ⟩ ) + 1 ) mod 5 ) ⟩ → ( ( 𝑏 ∈ ( 0 ..^ 5 ) ∧ 𝑦 ∈ ( 0 ..^ 5 ) ) → ( 𝑏 = ( ( 𝑦 + 2 ) mod 5 ) → ¬ { ⟨ 0 , 𝑏 ⟩ , ⟨ 1 , ( ( 𝑦 + 2 ) mod 5 ) ⟩ } ∈ 𝐸 ) ) )
78 8 16 opth ⊢ ( ⟨ 0 , 𝑏 ⟩ = ⟨ 1 , ( 2nd ‘ ⟨ 0 , 𝑦 ⟩ ) ⟩ ↔ ( 0 = 1 ∧ 𝑏 = ( 2nd ‘ ⟨ 0 , 𝑦 ⟩ ) ) )
79 0ne1 ⊢ 0 ≠ 1
80 eqneqall ⊢ ( 0 = 1 → ( 0 ≠ 1 → ( ( 𝑏 ∈ ( 0 ..^ 5 ) ∧ 𝑦 ∈ ( 0 ..^ 5 ) ) → ( 𝑏 = ( ( 𝑦 + 2 ) mod 5 ) → ¬ { ⟨ 0 , 𝑏 ⟩ , ⟨ 1 , ( ( 𝑦 + 2 ) mod 5 ) ⟩ } ∈ 𝐸 ) ) ) )
81 79 80 mpi ⊢ ( 0 = 1 → ( ( 𝑏 ∈ ( 0 ..^ 5 ) ∧ 𝑦 ∈ ( 0 ..^ 5 ) ) → ( 𝑏 = ( ( 𝑦 + 2 ) mod 5 ) → ¬ { ⟨ 0 , 𝑏 ⟩ , ⟨ 1 , ( ( 𝑦 + 2 ) mod 5 ) ⟩ } ∈ 𝐸 ) ) )
82 81 adantr ⊢ ( ( 0 = 1 ∧ 𝑏 = ( 2nd ‘ ⟨ 0 , 𝑦 ⟩ ) ) → ( ( 𝑏 ∈ ( 0 ..^ 5 ) ∧ 𝑦 ∈ ( 0 ..^ 5 ) ) → ( 𝑏 = ( ( 𝑦 + 2 ) mod 5 ) → ¬ { ⟨ 0 , 𝑏 ⟩ , ⟨ 1 , ( ( 𝑦 + 2 ) mod 5 ) ⟩ } ∈ 𝐸 ) ) )
83 78 82 sylbi ⊢ ( ⟨ 0 , 𝑏 ⟩ = ⟨ 1 , ( 2nd ‘ ⟨ 0 , 𝑦 ⟩ ) ⟩ → ( ( 𝑏 ∈ ( 0 ..^ 5 ) ∧ 𝑦 ∈ ( 0 ..^ 5 ) ) → ( 𝑏 = ( ( 𝑦 + 2 ) mod 5 ) → ¬ { ⟨ 0 , 𝑏 ⟩ , ⟨ 1 , ( ( 𝑦 + 2 ) mod 5 ) ⟩ } ∈ 𝐸 ) ) )
84 33 oveq1i ⊢ ( ( 2nd ‘ ⟨ 0 , 𝑦 ⟩ ) − 1 ) = ( 𝑦 − 1 )
85 84 oveq1i ⊢ ( ( ( 2nd ‘ ⟨ 0 , 𝑦 ⟩ ) − 1 ) mod 5 ) = ( ( 𝑦 − 1 ) mod 5 )
86 85 opeq2i ⊢ ⟨ 0 , ( ( ( 2nd ‘ ⟨ 0 , 𝑦 ⟩ ) − 1 ) mod 5 ) ⟩ = ⟨ 0 , ( ( 𝑦 − 1 ) mod 5 ) ⟩
87 86 eqeq2i ⊢ ( ⟨ 0 , 𝑏 ⟩ = ⟨ 0 , ( ( ( 2nd ‘ ⟨ 0 , 𝑦 ⟩ ) − 1 ) mod 5 ) ⟩ ↔ ⟨ 0 , 𝑏 ⟩ = ⟨ 0 , ( ( 𝑦 − 1 ) mod 5 ) ⟩ )
88 8 16 opth ⊢ ( ⟨ 0 , 𝑏 ⟩ = ⟨ 0 , ( ( 𝑦 − 1 ) mod 5 ) ⟩ ↔ ( 0 = 0 ∧ 𝑏 = ( ( 𝑦 − 1 ) mod 5 ) ) )
89 eqeq1 ⊢ ( 𝑏 = ( ( 𝑦 − 1 ) mod 5 ) → ( 𝑏 = ( ( 𝑦 + 2 ) mod 5 ) ↔ ( ( 𝑦 − 1 ) mod 5 ) = ( ( 𝑦 + 2 ) mod 5 ) ) )
90 89 adantr ⊢ ( ( 𝑏 = ( ( 𝑦 − 1 ) mod 5 ) ∧ ( 𝑏 ∈ ( 0 ..^ 5 ) ∧ 𝑦 ∈ ( 0 ..^ 5 ) ) ) → ( 𝑏 = ( ( 𝑦 + 2 ) mod 5 ) ↔ ( ( 𝑦 − 1 ) mod 5 ) = ( ( 𝑦 + 2 ) mod 5 ) ) )
91 44 48 zsubcld ⊢ ( 𝑦 ∈ ( 0 ..^ 5 ) → ( 𝑦 − 1 ) ∈ ℤ )
92 difmod0 ⊢ ( ( ( 𝑦 − 1 ) ∈ ℤ ∧ ( 𝑦 + 2 ) ∈ ℤ ∧ 5 ∈ ℕ ) → ( ( ( ( 𝑦 − 1 ) − ( 𝑦 + 2 ) ) mod 5 ) = 0 ↔ ( ( 𝑦 − 1 ) mod 5 ) = ( ( 𝑦 + 2 ) mod 5 ) ) )
93 92 bicomd ⊢ ( ( ( 𝑦 − 1 ) ∈ ℤ ∧ ( 𝑦 + 2 ) ∈ ℤ ∧ 5 ∈ ℕ ) → ( ( ( 𝑦 − 1 ) mod 5 ) = ( ( 𝑦 + 2 ) mod 5 ) ↔ ( ( ( 𝑦 − 1 ) − ( 𝑦 + 2 ) ) mod 5 ) = 0 ) )
94 91 47 51 93 syl3anc ⊢ ( 𝑦 ∈ ( 0 ..^ 5 ) → ( ( ( 𝑦 − 1 ) mod 5 ) = ( ( 𝑦 + 2 ) mod 5 ) ↔ ( ( ( 𝑦 − 1 ) − ( 𝑦 + 2 ) ) mod 5 ) = 0 ) )
95 54 56 54 55 subsubadd23 ⊢ ( 𝑦 ∈ ( 0 ..^ 5 ) → ( ( 𝑦 − 1 ) − ( 𝑦 + 2 ) ) = ( ( 𝑦 − 𝑦 ) − ( 1 + 2 ) ) )
96 54 subidd ⊢ ( 𝑦 ∈ ( 0 ..^ 5 ) → ( 𝑦 − 𝑦 ) = 0 )
97 1p2e3 ⊢ ( 1 + 2 ) = 3
98 97 a1i ⊢ ( 𝑦 ∈ ( 0 ..^ 5 ) → ( 1 + 2 ) = 3 )
99 96 98 oveq12d ⊢ ( 𝑦 ∈ ( 0 ..^ 5 ) → ( ( 𝑦 − 𝑦 ) − ( 1 + 2 ) ) = ( 0 − 3 ) )
100 df-neg ⊢ - 3 = ( 0 − 3 )
101 99 100 eqtr4di ⊢ ( 𝑦 ∈ ( 0 ..^ 5 ) → ( ( 𝑦 − 𝑦 ) − ( 1 + 2 ) ) = - 3 )
102 95 101 eqtrd ⊢ ( 𝑦 ∈ ( 0 ..^ 5 ) → ( ( 𝑦 − 1 ) − ( 𝑦 + 2 ) ) = - 3 )
103 102 oveq1d ⊢ ( 𝑦 ∈ ( 0 ..^ 5 ) → ( ( ( 𝑦 − 1 ) − ( 𝑦 + 2 ) ) mod 5 ) = ( - 3 mod 5 ) )
104 103 eqeq1d ⊢ ( 𝑦 ∈ ( 0 ..^ 5 ) → ( ( ( ( 𝑦 − 1 ) − ( 𝑦 + 2 ) ) mod 5 ) = 0 ↔ ( - 3 mod 5 ) = 0 ) )
105 3re ⊢ 3 ∈ ℝ
106 negmod0 ⊢ ( ( 3 ∈ ℝ ∧ 5 ∈ ℝ+ ) → ( ( 3 mod 5 ) = 0 ↔ ( - 3 mod 5 ) = 0 ) )
107 105 64 106 mp2an ⊢ ( ( 3 mod 5 ) = 0 ↔ ( - 3 mod 5 ) = 0 )
108 0re ⊢ 0 ∈ ℝ
109 3pos ⊢ 0 < 3
110 108 105 109 ltleii ⊢ 0 ≤ 3
111 3lt5 ⊢ 3 < 5
112 modid ⊢ ( ( ( 3 ∈ ℝ ∧ 5 ∈ ℝ+ ) ∧ ( 0 ≤ 3 ∧ 3 < 5 ) ) → ( 3 mod 5 ) = 3 )
113 105 64 110 111 112 mp4an ⊢ ( 3 mod 5 ) = 3
114 113 eqeq1i ⊢ ( ( 3 mod 5 ) = 0 ↔ 3 = 0 )
115 3ne0 ⊢ 3 ≠ 0
116 eqneqall ⊢ ( 3 = 0 → ( 3 ≠ 0 → ¬ { ⟨ 0 , 𝑏 ⟩ , ⟨ 1 , ( ( 𝑦 + 2 ) mod 5 ) ⟩ } ∈ 𝐸 ) )
117 115 116 mpi ⊢ ( 3 = 0 → ¬ { ⟨ 0 , 𝑏 ⟩ , ⟨ 1 , ( ( 𝑦 + 2 ) mod 5 ) ⟩ } ∈ 𝐸 )
118 114 117 sylbi ⊢ ( ( 3 mod 5 ) = 0 → ¬ { ⟨ 0 , 𝑏 ⟩ , ⟨ 1 , ( ( 𝑦 + 2 ) mod 5 ) ⟩ } ∈ 𝐸 )
119 107 118 sylbir ⊢ ( ( - 3 mod 5 ) = 0 → ¬ { ⟨ 0 , 𝑏 ⟩ , ⟨ 1 , ( ( 𝑦 + 2 ) mod 5 ) ⟩ } ∈ 𝐸 )
120 104 119 biimtrdi ⊢ ( 𝑦 ∈ ( 0 ..^ 5 ) → ( ( ( ( 𝑦 − 1 ) − ( 𝑦 + 2 ) ) mod 5 ) = 0 → ¬ { ⟨ 0 , 𝑏 ⟩ , ⟨ 1 , ( ( 𝑦 + 2 ) mod 5 ) ⟩ } ∈ 𝐸 ) )
121 94 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 90 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 88 124 simplbiim ⊢ ( ⟨ 0 , 𝑏 ⟩ = ⟨ 0 , ( ( 𝑦 − 1 ) mod 5 ) ⟩ → ( ( 𝑏 ∈ ( 0 ..^ 5 ) ∧ 𝑦 ∈ ( 0 ..^ 5 ) ) → ( 𝑏 = ( ( 𝑦 + 2 ) mod 5 ) → ¬ { ⟨ 0 , 𝑏 ⟩ , ⟨ 1 , ( ( 𝑦 + 2 ) mod 5 ) ⟩ } ∈ 𝐸 ) ) )
126 87 125 sylbi ⊢ ( ⟨ 0 , 𝑏 ⟩ = ⟨ 0 , ( ( ( 2nd ‘ ⟨ 0 , 𝑦 ⟩ ) − 1 ) mod 5 ) ⟩ → ( ( 𝑏 ∈ ( 0 ..^ 5 ) ∧ 𝑦 ∈ ( 0 ..^ 5 ) ) → ( 𝑏 = ( ( 𝑦 + 2 ) mod 5 ) → ¬ { ⟨ 0 , 𝑏 ⟩ , ⟨ 1 , ( ( 𝑦 + 2 ) mod 5 ) ⟩ } ∈ 𝐸 ) ) )
127 77 83 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 , 𝑏 ⟩ , 𝐿 } ∈ 𝐸 )