Metamath Proof Explorer

Theorem pgnbgreunbgrlem5lem1

Description: Lemma 1 for pgnbgreunbgrlem5 . (Contributed by AV, 21-Nov-2025)

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