Metamath Proof Explorer

Theorem pgnbgreunbgrlem5lem3

Description: Lemma 3 for pgnbgreunbgrlem5 . (Contributed by AV, 20-Nov-2025)

Ref Expression
Hypotheses pgnbgreunbgr.g ⊢ 𝐺 = ( 5 gPetersenGr 2 )
pgnbgreunbgr.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
pgnbgreunbgr.e ⊢ 𝐸 = ( Edg ‘ 𝐺 )
pgnbgreunbgr.n ⊢ 𝑁 = ( 𝐺 NeighbVtx 𝑋 )
Assertion pgnbgreunbgrlem5lem3 ( ( ( ( 𝐿 = ⟨ 0 , ( ( 𝑦 + 1 ) mod 5 ) ⟩ ∧ 𝐾 = ⟨ 0 , ( ( 𝑦 − 1 ) mod 5 ) ⟩ ) ∧ ( 𝑏 ∈ ( 0 ..^ 5 ) ∧ 𝑦 ∈ ( 0 ..^ 5 ) ) ) ∧ { 𝐾 , ⟨ 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 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 ovex ⊢ ( ( 𝑦 − 1 ) mod 5 ) ∈ V
10 8 9 op1st ⊢ ( 1st ‘ ⟨ 0 , ( ( 𝑦 − 1 ) mod 5 ) ⟩ ) = 0
11 simpr ⊢ ( ( ( 𝑏 ∈ ( 0 ..^ 5 ) ∧ 𝑦 ∈ ( 0 ..^ 5 ) ) ∧ { ⟨ 0 , ( ( 𝑦 − 1 ) mod 5 ) ⟩ , ⟨ 1 , 𝑏 ⟩ } ∈ 𝐸 ) → { ⟨ 0 , ( ( 𝑦 − 1 ) mod 5 ) ⟩ , ⟨ 1 , 𝑏 ⟩ } ∈ 𝐸 )
12 eqid ⊢ ( 1 ..^ ( ⌈ ‘ ( 5 / 2 ) ) ) = ( 1 ..^ ( ⌈ ‘ ( 5 / 2 ) ) )
13 12 1 2 3 gpgvtxedg0 ⊢ ( ( ( 5 ∈ ( ℤ≥ ‘ 3 ) ∧ 2 ∈ ( 1 ..^ ( ⌈ ‘ ( 5 / 2 ) ) ) ) ∧ ( 1st ‘ ⟨ 0 , ( ( 𝑦 − 1 ) mod 5 ) ⟩ ) = 0 ∧ { ⟨ 0 , ( ( 𝑦 − 1 ) mod 5 ) ⟩ , ⟨ 1 , 𝑏 ⟩ } ∈ 𝐸 ) → ( ⟨ 1 , 𝑏 ⟩ = ⟨ 0 , ( ( ( 2nd ‘ ⟨ 0 , ( ( 𝑦 − 1 ) mod 5 ) ⟩ ) + 1 ) mod 5 ) ⟩ ∨ ⟨ 1 , 𝑏 ⟩ = ⟨ 1 , ( 2nd ‘ ⟨ 0 , ( ( 𝑦 − 1 ) mod 5 ) ⟩ ) ⟩ ∨ ⟨ 1 , 𝑏 ⟩ = ⟨ 0 , ( ( ( 2nd ‘ ⟨ 0 , ( ( 𝑦 − 1 ) mod 5 ) ⟩ ) − 1 ) mod 5 ) ⟩ ) )
14 7 10 11 13 mp3an12i ⊢ ( ( ( 𝑏 ∈ ( 0 ..^ 5 ) ∧ 𝑦 ∈ ( 0 ..^ 5 ) ) ∧ { ⟨ 0 , ( ( 𝑦 − 1 ) mod 5 ) ⟩ , ⟨ 1 , 𝑏 ⟩ } ∈ 𝐸 ) → ( ⟨ 1 , 𝑏 ⟩ = ⟨ 0 , ( ( ( 2nd ‘ ⟨ 0 , ( ( 𝑦 − 1 ) mod 5 ) ⟩ ) + 1 ) mod 5 ) ⟩ ∨ ⟨ 1 , 𝑏 ⟩ = ⟨ 1 , ( 2nd ‘ ⟨ 0 , ( ( 𝑦 − 1 ) mod 5 ) ⟩ ) ⟩ ∨ ⟨ 1 , 𝑏 ⟩ = ⟨ 0 , ( ( ( 2nd ‘ ⟨ 0 , ( ( 𝑦 − 1 ) mod 5 ) ⟩ ) − 1 ) mod 5 ) ⟩ ) )
15 14 ex ⊢ ( ( 𝑏 ∈ ( 0 ..^ 5 ) ∧ 𝑦 ∈ ( 0 ..^ 5 ) ) → ( { ⟨ 0 , ( ( 𝑦 − 1 ) mod 5 ) ⟩ , ⟨ 1 , 𝑏 ⟩ } ∈ 𝐸 → ( ⟨ 1 , 𝑏 ⟩ = ⟨ 0 , ( ( ( 2nd ‘ ⟨ 0 , ( ( 𝑦 − 1 ) mod 5 ) ⟩ ) + 1 ) mod 5 ) ⟩ ∨ ⟨ 1 , 𝑏 ⟩ = ⟨ 1 , ( 2nd ‘ ⟨ 0 , ( ( 𝑦 − 1 ) mod 5 ) ⟩ ) ⟩ ∨ ⟨ 1 , 𝑏 ⟩ = ⟨ 0 , ( ( ( 2nd ‘ ⟨ 0 , ( ( 𝑦 − 1 ) mod 5 ) ⟩ ) − 1 ) mod 5 ) ⟩ ) ) )
16 1ex ⊢ 1 ∈ V
17 vex ⊢ 𝑏 ∈ V
18 16 17 opth ⊢ ( ⟨ 1 , 𝑏 ⟩ = ⟨ 0 , ( ( ( 2nd ‘ ⟨ 0 , ( ( 𝑦 − 1 ) mod 5 ) ⟩ ) + 1 ) mod 5 ) ⟩ ↔ ( 1 = 0 ∧ 𝑏 = ( ( ( 2nd ‘ ⟨ 0 , ( ( 𝑦 − 1 ) mod 5 ) ⟩ ) + 1 ) mod 5 ) ) )
19 ax-1ne0 ⊢ 1 ≠ 0
20 19 a1i ⊢ ( { ⟨ 1 , 𝑏 ⟩ , ⟨ 0 , ( ( 𝑦 + 1 ) mod 5 ) ⟩ } ∈ 𝐸 → 1 ≠ 0 )
21 20 necon2bi ⊢ ( 1 = 0 → ¬ { ⟨ 1 , 𝑏 ⟩ , ⟨ 0 , ( ( 𝑦 + 1 ) mod 5 ) ⟩ } ∈ 𝐸 )
22 21 adantr ⊢ ( ( 1 = 0 ∧ 𝑏 = ( ( ( 2nd ‘ ⟨ 0 , ( ( 𝑦 − 1 ) mod 5 ) ⟩ ) + 1 ) mod 5 ) ) → ¬ { ⟨ 1 , 𝑏 ⟩ , ⟨ 0 , ( ( 𝑦 + 1 ) mod 5 ) ⟩ } ∈ 𝐸 )
23 18 22 sylbi ⊢ ( ⟨ 1 , 𝑏 ⟩ = ⟨ 0 , ( ( ( 2nd ‘ ⟨ 0 , ( ( 𝑦 − 1 ) mod 5 ) ⟩ ) + 1 ) mod 5 ) ⟩ → ¬ { ⟨ 1 , 𝑏 ⟩ , ⟨ 0 , ( ( 𝑦 + 1 ) mod 5 ) ⟩ } ∈ 𝐸 )
24 23 a1i ⊢ ( ( 𝑏 ∈ ( 0 ..^ 5 ) ∧ 𝑦 ∈ ( 0 ..^ 5 ) ) → ( ⟨ 1 , 𝑏 ⟩ = ⟨ 0 , ( ( ( 2nd ‘ ⟨ 0 , ( ( 𝑦 − 1 ) mod 5 ) ⟩ ) + 1 ) mod 5 ) ⟩ → ¬ { ⟨ 1 , 𝑏 ⟩ , ⟨ 0 , ( ( 𝑦 + 1 ) mod 5 ) ⟩ } ∈ 𝐸 ) )
25 16 17 opth ⊢ ( ⟨ 1 , 𝑏 ⟩ = ⟨ 1 , ( 2nd ‘ ⟨ 0 , ( ( 𝑦 − 1 ) mod 5 ) ⟩ ) ⟩ ↔ ( 1 = 1 ∧ 𝑏 = ( 2nd ‘ ⟨ 0 , ( ( 𝑦 − 1 ) mod 5 ) ⟩ ) ) )
26 8 9 op2nd ⊢ ( 2nd ‘ ⟨ 0 , ( ( 𝑦 − 1 ) mod 5 ) ⟩ ) = ( ( 𝑦 − 1 ) mod 5 )
27 26 eqeq2i ⊢ ( 𝑏 = ( 2nd ‘ ⟨ 0 , ( ( 𝑦 − 1 ) mod 5 ) ⟩ ) ↔ 𝑏 = ( ( 𝑦 − 1 ) mod 5 ) )
28 1 3 pgnioedg5 ⊢ ( 𝑦 ∈ ( 0 ..^ 5 ) → ¬ { ⟨ 1 , ( ( 𝑦 − 1 ) mod 5 ) ⟩ , ⟨ 0 , ( ( 𝑦 + 1 ) mod 5 ) ⟩ } ∈ 𝐸 )
29 28 adantl ⊢ ( ( 𝑏 ∈ ( 0 ..^ 5 ) ∧ 𝑦 ∈ ( 0 ..^ 5 ) ) → ¬ { ⟨ 1 , ( ( 𝑦 − 1 ) mod 5 ) ⟩ , ⟨ 0 , ( ( 𝑦 + 1 ) mod 5 ) ⟩ } ∈ 𝐸 )
30 opeq2 ⊢ ( 𝑏 = ( ( 𝑦 − 1 ) mod 5 ) → ⟨ 1 , 𝑏 ⟩ = ⟨ 1 , ( ( 𝑦 − 1 ) mod 5 ) ⟩ )
31 30 preq1d ⊢ ( 𝑏 = ( ( 𝑦 − 1 ) mod 5 ) → { ⟨ 1 , 𝑏 ⟩ , ⟨ 0 , ( ( 𝑦 + 1 ) mod 5 ) ⟩ } = { ⟨ 1 , ( ( 𝑦 − 1 ) mod 5 ) ⟩ , ⟨ 0 , ( ( 𝑦 + 1 ) mod 5 ) ⟩ } )
32 31 eleq1d ⊢ ( 𝑏 = ( ( 𝑦 − 1 ) mod 5 ) → ( { ⟨ 1 , 𝑏 ⟩ , ⟨ 0 , ( ( 𝑦 + 1 ) mod 5 ) ⟩ } ∈ 𝐸 ↔ { ⟨ 1 , ( ( 𝑦 − 1 ) mod 5 ) ⟩ , ⟨ 0 , ( ( 𝑦 + 1 ) mod 5 ) ⟩ } ∈ 𝐸 ) )
33 32 notbid ⊢ ( 𝑏 = ( ( 𝑦 − 1 ) mod 5 ) → ( ¬ { ⟨ 1 , 𝑏 ⟩ , ⟨ 0 , ( ( 𝑦 + 1 ) mod 5 ) ⟩ } ∈ 𝐸 ↔ ¬ { ⟨ 1 , ( ( 𝑦 − 1 ) mod 5 ) ⟩ , ⟨ 0 , ( ( 𝑦 + 1 ) mod 5 ) ⟩ } ∈ 𝐸 ) )
34 29 33 imbitrrid ⊢ ( 𝑏 = ( ( 𝑦 − 1 ) mod 5 ) → ( ( 𝑏 ∈ ( 0 ..^ 5 ) ∧ 𝑦 ∈ ( 0 ..^ 5 ) ) → ¬ { ⟨ 1 , 𝑏 ⟩ , ⟨ 0 , ( ( 𝑦 + 1 ) mod 5 ) ⟩ } ∈ 𝐸 ) )
35 27 34 sylbi ⊢ ( 𝑏 = ( 2nd ‘ ⟨ 0 , ( ( 𝑦 − 1 ) mod 5 ) ⟩ ) → ( ( 𝑏 ∈ ( 0 ..^ 5 ) ∧ 𝑦 ∈ ( 0 ..^ 5 ) ) → ¬ { ⟨ 1 , 𝑏 ⟩ , ⟨ 0 , ( ( 𝑦 + 1 ) mod 5 ) ⟩ } ∈ 𝐸 ) )
36 25 35 simplbiim ⊢ ( ⟨ 1 , 𝑏 ⟩ = ⟨ 1 , ( 2nd ‘ ⟨ 0 , ( ( 𝑦 − 1 ) mod 5 ) ⟩ ) ⟩ → ( ( 𝑏 ∈ ( 0 ..^ 5 ) ∧ 𝑦 ∈ ( 0 ..^ 5 ) ) → ¬ { ⟨ 1 , 𝑏 ⟩ , ⟨ 0 , ( ( 𝑦 + 1 ) mod 5 ) ⟩ } ∈ 𝐸 ) )
37 36 com12 ⊢ ( ( 𝑏 ∈ ( 0 ..^ 5 ) ∧ 𝑦 ∈ ( 0 ..^ 5 ) ) → ( ⟨ 1 , 𝑏 ⟩ = ⟨ 1 , ( 2nd ‘ ⟨ 0 , ( ( 𝑦 − 1 ) mod 5 ) ⟩ ) ⟩ → ¬ { ⟨ 1 , 𝑏 ⟩ , ⟨ 0 , ( ( 𝑦 + 1 ) mod 5 ) ⟩ } ∈ 𝐸 ) )
38 16 17 opth ⊢ ( ⟨ 1 , 𝑏 ⟩ = ⟨ 0 , ( ( ( 2nd ‘ ⟨ 0 , ( ( 𝑦 − 1 ) mod 5 ) ⟩ ) − 1 ) mod 5 ) ⟩ ↔ ( 1 = 0 ∧ 𝑏 = ( ( ( 2nd ‘ ⟨ 0 , ( ( 𝑦 − 1 ) mod 5 ) ⟩ ) − 1 ) mod 5 ) ) )
39 21 adantr ⊢ ( ( 1 = 0 ∧ 𝑏 = ( ( ( 2nd ‘ ⟨ 0 , ( ( 𝑦 − 1 ) mod 5 ) ⟩ ) − 1 ) mod 5 ) ) → ¬ { ⟨ 1 , 𝑏 ⟩ , ⟨ 0 , ( ( 𝑦 + 1 ) mod 5 ) ⟩ } ∈ 𝐸 )
40 38 39 sylbi ⊢ ( ⟨ 1 , 𝑏 ⟩ = ⟨ 0 , ( ( ( 2nd ‘ ⟨ 0 , ( ( 𝑦 − 1 ) mod 5 ) ⟩ ) − 1 ) mod 5 ) ⟩ → ¬ { ⟨ 1 , 𝑏 ⟩ , ⟨ 0 , ( ( 𝑦 + 1 ) mod 5 ) ⟩ } ∈ 𝐸 )
41 40 a1i ⊢ ( ( 𝑏 ∈ ( 0 ..^ 5 ) ∧ 𝑦 ∈ ( 0 ..^ 5 ) ) → ( ⟨ 1 , 𝑏 ⟩ = ⟨ 0 , ( ( ( 2nd ‘ ⟨ 0 , ( ( 𝑦 − 1 ) mod 5 ) ⟩ ) − 1 ) mod 5 ) ⟩ → ¬ { ⟨ 1 , 𝑏 ⟩ , ⟨ 0 , ( ( 𝑦 + 1 ) mod 5 ) ⟩ } ∈ 𝐸 ) )
42 24 37 41 3jaod ⊢ ( ( 𝑏 ∈ ( 0 ..^ 5 ) ∧ 𝑦 ∈ ( 0 ..^ 5 ) ) → ( ( ⟨ 1 , 𝑏 ⟩ = ⟨ 0 , ( ( ( 2nd ‘ ⟨ 0 , ( ( 𝑦 − 1 ) mod 5 ) ⟩ ) + 1 ) mod 5 ) ⟩ ∨ ⟨ 1 , 𝑏 ⟩ = ⟨ 1 , ( 2nd ‘ ⟨ 0 , ( ( 𝑦 − 1 ) mod 5 ) ⟩ ) ⟩ ∨ ⟨ 1 , 𝑏 ⟩ = ⟨ 0 , ( ( ( 2nd ‘ ⟨ 0 , ( ( 𝑦 − 1 ) mod 5 ) ⟩ ) − 1 ) mod 5 ) ⟩ ) → ¬ { ⟨ 1 , 𝑏 ⟩ , ⟨ 0 , ( ( 𝑦 + 1 ) mod 5 ) ⟩ } ∈ 𝐸 ) )
43 15 42 syld ⊢ ( ( 𝑏 ∈ ( 0 ..^ 5 ) ∧ 𝑦 ∈ ( 0 ..^ 5 ) ) → ( { ⟨ 0 , ( ( 𝑦 − 1 ) mod 5 ) ⟩ , ⟨ 1 , 𝑏 ⟩ } ∈ 𝐸 → ¬ { ⟨ 1 , 𝑏 ⟩ , ⟨ 0 , ( ( 𝑦 + 1 ) mod 5 ) ⟩ } ∈ 𝐸 ) )
44 43 adantl ⊢ ( ( ( 𝐿 = ⟨ 0 , ( ( 𝑦 + 1 ) mod 5 ) ⟩ ∧ 𝐾 = ⟨ 0 , ( ( 𝑦 − 1 ) mod 5 ) ⟩ ) ∧ ( 𝑏 ∈ ( 0 ..^ 5 ) ∧ 𝑦 ∈ ( 0 ..^ 5 ) ) ) → ( { ⟨ 0 , ( ( 𝑦 − 1 ) mod 5 ) ⟩ , ⟨ 1 , 𝑏 ⟩ } ∈ 𝐸 → ¬ { ⟨ 1 , 𝑏 ⟩ , ⟨ 0 , ( ( 𝑦 + 1 ) mod 5 ) ⟩ } ∈ 𝐸 ) )
45 preq1 ⊢ ( 𝐾 = ⟨ 0 , ( ( 𝑦 − 1 ) mod 5 ) ⟩ → { 𝐾 , ⟨ 1 , 𝑏 ⟩ } = { ⟨ 0 , ( ( 𝑦 − 1 ) mod 5 ) ⟩ , ⟨ 1 , 𝑏 ⟩ } )
46 45 eleq1d ⊢ ( 𝐾 = ⟨ 0 , ( ( 𝑦 − 1 ) mod 5 ) ⟩ → ( { 𝐾 , ⟨ 1 , 𝑏 ⟩ } ∈ 𝐸 ↔ { ⟨ 0 , ( ( 𝑦 − 1 ) mod 5 ) ⟩ , ⟨ 1 , 𝑏 ⟩ } ∈ 𝐸 ) )
47 46 adantl ⊢ ( ( 𝐿 = ⟨ 0 , ( ( 𝑦 + 1 ) mod 5 ) ⟩ ∧ 𝐾 = ⟨ 0 , ( ( 𝑦 − 1 ) mod 5 ) ⟩ ) → ( { 𝐾 , ⟨ 1 , 𝑏 ⟩ } ∈ 𝐸 ↔ { ⟨ 0 , ( ( 𝑦 − 1 ) mod 5 ) ⟩ , ⟨ 1 , 𝑏 ⟩ } ∈ 𝐸 ) )
48 preq2 ⊢ ( 𝐿 = ⟨ 0 , ( ( 𝑦 + 1 ) mod 5 ) ⟩ → { ⟨ 1 , 𝑏 ⟩ , 𝐿 } = { ⟨ 1 , 𝑏 ⟩ , ⟨ 0 , ( ( 𝑦 + 1 ) mod 5 ) ⟩ } )
49 48 eleq1d ⊢ ( 𝐿 = ⟨ 0 , ( ( 𝑦 + 1 ) mod 5 ) ⟩ → ( { ⟨ 1 , 𝑏 ⟩ , 𝐿 } ∈ 𝐸 ↔ { ⟨ 1 , 𝑏 ⟩ , ⟨ 0 , ( ( 𝑦 + 1 ) mod 5 ) ⟩ } ∈ 𝐸 ) )
50 49 notbid ⊢ ( 𝐿 = ⟨ 0 , ( ( 𝑦 + 1 ) mod 5 ) ⟩ → ( ¬ { ⟨ 1 , 𝑏 ⟩ , 𝐿 } ∈ 𝐸 ↔ ¬ { ⟨ 1 , 𝑏 ⟩ , ⟨ 0 , ( ( 𝑦 + 1 ) mod 5 ) ⟩ } ∈ 𝐸 ) )
51 50 adantr ⊢ ( ( 𝐿 = ⟨ 0 , ( ( 𝑦 + 1 ) mod 5 ) ⟩ ∧ 𝐾 = ⟨ 0 , ( ( 𝑦 − 1 ) mod 5 ) ⟩ ) → ( ¬ { ⟨ 1 , 𝑏 ⟩ , 𝐿 } ∈ 𝐸 ↔ ¬ { ⟨ 1 , 𝑏 ⟩ , ⟨ 0 , ( ( 𝑦 + 1 ) mod 5 ) ⟩ } ∈ 𝐸 ) )
52 47 51 imbi12d ⊢ ( ( 𝐿 = ⟨ 0 , ( ( 𝑦 + 1 ) mod 5 ) ⟩ ∧ 𝐾 = ⟨ 0 , ( ( 𝑦 − 1 ) mod 5 ) ⟩ ) → ( ( { 𝐾 , ⟨ 1 , 𝑏 ⟩ } ∈ 𝐸 → ¬ { ⟨ 1 , 𝑏 ⟩ , 𝐿 } ∈ 𝐸 ) ↔ ( { ⟨ 0 , ( ( 𝑦 − 1 ) mod 5 ) ⟩ , ⟨ 1 , 𝑏 ⟩ } ∈ 𝐸 → ¬ { ⟨ 1 , 𝑏 ⟩ , ⟨ 0 , ( ( 𝑦 + 1 ) mod 5 ) ⟩ } ∈ 𝐸 ) ) )
53 52 adantr ⊢ ( ( ( 𝐿 = ⟨ 0 , ( ( 𝑦 + 1 ) mod 5 ) ⟩ ∧ 𝐾 = ⟨ 0 , ( ( 𝑦 − 1 ) mod 5 ) ⟩ ) ∧ ( 𝑏 ∈ ( 0 ..^ 5 ) ∧ 𝑦 ∈ ( 0 ..^ 5 ) ) ) → ( ( { 𝐾 , ⟨ 1 , 𝑏 ⟩ } ∈ 𝐸 → ¬ { ⟨ 1 , 𝑏 ⟩ , 𝐿 } ∈ 𝐸 ) ↔ ( { ⟨ 0 , ( ( 𝑦 − 1 ) mod 5 ) ⟩ , ⟨ 1 , 𝑏 ⟩ } ∈ 𝐸 → ¬ { ⟨ 1 , 𝑏 ⟩ , ⟨ 0 , ( ( 𝑦 + 1 ) mod 5 ) ⟩ } ∈ 𝐸 ) ) )
54 44 53 mpbird ⊢ ( ( ( 𝐿 = ⟨ 0 , ( ( 𝑦 + 1 ) mod 5 ) ⟩ ∧ 𝐾 = ⟨ 0 , ( ( 𝑦 − 1 ) mod 5 ) ⟩ ) ∧ ( 𝑏 ∈ ( 0 ..^ 5 ) ∧ 𝑦 ∈ ( 0 ..^ 5 ) ) ) → ( { 𝐾 , ⟨ 1 , 𝑏 ⟩ } ∈ 𝐸 → ¬ { ⟨ 1 , 𝑏 ⟩ , 𝐿 } ∈ 𝐸 ) )
55 54 imp ⊢ ( ( ( ( 𝐿 = ⟨ 0 , ( ( 𝑦 + 1 ) mod 5 ) ⟩ ∧ 𝐾 = ⟨ 0 , ( ( 𝑦 − 1 ) mod 5 ) ⟩ ) ∧ ( 𝑏 ∈ ( 0 ..^ 5 ) ∧ 𝑦 ∈ ( 0 ..^ 5 ) ) ) ∧ { 𝐾 , ⟨ 1 , 𝑏 ⟩ } ∈ 𝐸 ) → ¬ { ⟨ 1 , 𝑏 ⟩ , 𝐿 } ∈ 𝐸 )