Metamath Proof Explorer

Theorem pgnioedg3

Description: An inside and an outside vertex not adjacent in a Petersen graph. (Contributed by AV, 21-Nov-2025)

Ref Expression
Hypotheses pgnioedg1.g ⊢ 𝐺 = ( 5 gPetersenGr 2 )
pgnioedg1.e ⊢ 𝐸 = ( Edg ‘ 𝐺 )
Assertion pgnioedg3 ( 𝑦 ∈ ( 0 ..^ 5 ) → ¬ { ⟨ 1 , ( ( 𝑦 + 2 ) mod 5 ) ⟩ , ⟨ 0 , ( ( 𝑦 − 1 ) mod 5 ) ⟩ } ∈ 𝐸 )

Proof

Step Hyp Ref Expression
1 pgnioedg1.g ⊢ 𝐺 = ( 5 gPetersenGr 2 )
2 pgnioedg1.e ⊢ 𝐸 = ( Edg ‘ 𝐺 )
3 5eluz3 ⊢ 5 ∈ ( ℤ≥ ‘ 3 )
4 pglem ⊢ 2 ∈ ( 1 ..^ ( ⌈ ‘ ( 5 / 2 ) ) )
5 3 4 pm3.2i ⊢ ( 5 ∈ ( ℤ≥ ‘ 3 ) ∧ 2 ∈ ( 1 ..^ ( ⌈ ‘ ( 5 / 2 ) ) ) )
6 1ex ⊢ 1 ∈ V
7 ovex ⊢ ( ( 𝑦 + 2 ) mod 5 ) ∈ V
8 6 7 op1st ⊢ ( 1st ‘ ⟨ 1 , ( ( 𝑦 + 2 ) mod 5 ) ⟩ ) = 1
9 simpr ⊢ ( ( 𝑦 ∈ ( 0 ..^ 5 ) ∧ { ⟨ 1 , ( ( 𝑦 + 2 ) mod 5 ) ⟩ , ⟨ 0 , ( ( 𝑦 − 1 ) mod 5 ) ⟩ } ∈ 𝐸 ) → { ⟨ 1 , ( ( 𝑦 + 2 ) mod 5 ) ⟩ , ⟨ 0 , ( ( 𝑦 − 1 ) mod 5 ) ⟩ } ∈ 𝐸 )
10 eqid ⊢ ( 1 ..^ ( ⌈ ‘ ( 5 / 2 ) ) ) = ( 1 ..^ ( ⌈ ‘ ( 5 / 2 ) ) )
11 eqid ⊢ ( Vtx ‘ 𝐺 ) = ( Vtx ‘ 𝐺 )
12 10 1 11 2 gpgvtxedg1 ⊢ ( ( ( 5 ∈ ( ℤ≥ ‘ 3 ) ∧ 2 ∈ ( 1 ..^ ( ⌈ ‘ ( 5 / 2 ) ) ) ) ∧ ( 1st ‘ ⟨ 1 , ( ( 𝑦 + 2 ) mod 5 ) ⟩ ) = 1 ∧ { ⟨ 1 , ( ( 𝑦 + 2 ) mod 5 ) ⟩ , ⟨ 0 , ( ( 𝑦 − 1 ) mod 5 ) ⟩ } ∈ 𝐸 ) → ( ⟨ 0 , ( ( 𝑦 − 1 ) mod 5 ) ⟩ = ⟨ 1 , ( ( ( 2nd ‘ ⟨ 1 , ( ( 𝑦 + 2 ) mod 5 ) ⟩ ) + 2 ) mod 5 ) ⟩ ∨ ⟨ 0 , ( ( 𝑦 − 1 ) mod 5 ) ⟩ = ⟨ 0 , ( 2nd ‘ ⟨ 1 , ( ( 𝑦 + 2 ) mod 5 ) ⟩ ) ⟩ ∨ ⟨ 0 , ( ( 𝑦 − 1 ) mod 5 ) ⟩ = ⟨ 1 , ( ( ( 2nd ‘ ⟨ 1 , ( ( 𝑦 + 2 ) mod 5 ) ⟩ ) − 2 ) mod 5 ) ⟩ ) )
13 5 8 9 12 mp3an12i ⊢ ( ( 𝑦 ∈ ( 0 ..^ 5 ) ∧ { ⟨ 1 , ( ( 𝑦 + 2 ) mod 5 ) ⟩ , ⟨ 0 , ( ( 𝑦 − 1 ) mod 5 ) ⟩ } ∈ 𝐸 ) → ( ⟨ 0 , ( ( 𝑦 − 1 ) mod 5 ) ⟩ = ⟨ 1 , ( ( ( 2nd ‘ ⟨ 1 , ( ( 𝑦 + 2 ) mod 5 ) ⟩ ) + 2 ) mod 5 ) ⟩ ∨ ⟨ 0 , ( ( 𝑦 − 1 ) mod 5 ) ⟩ = ⟨ 0 , ( 2nd ‘ ⟨ 1 , ( ( 𝑦 + 2 ) mod 5 ) ⟩ ) ⟩ ∨ ⟨ 0 , ( ( 𝑦 − 1 ) mod 5 ) ⟩ = ⟨ 1 , ( ( ( 2nd ‘ ⟨ 1 , ( ( 𝑦 + 2 ) mod 5 ) ⟩ ) − 2 ) mod 5 ) ⟩ ) )
14 13 ex ⊢ ( 𝑦 ∈ ( 0 ..^ 5 ) → ( { ⟨ 1 , ( ( 𝑦 + 2 ) mod 5 ) ⟩ , ⟨ 0 , ( ( 𝑦 − 1 ) mod 5 ) ⟩ } ∈ 𝐸 → ( ⟨ 0 , ( ( 𝑦 − 1 ) mod 5 ) ⟩ = ⟨ 1 , ( ( ( 2nd ‘ ⟨ 1 , ( ( 𝑦 + 2 ) mod 5 ) ⟩ ) + 2 ) mod 5 ) ⟩ ∨ ⟨ 0 , ( ( 𝑦 − 1 ) mod 5 ) ⟩ = ⟨ 0 , ( 2nd ‘ ⟨ 1 , ( ( 𝑦 + 2 ) mod 5 ) ⟩ ) ⟩ ∨ ⟨ 0 , ( ( 𝑦 − 1 ) mod 5 ) ⟩ = ⟨ 1 , ( ( ( 2nd ‘ ⟨ 1 , ( ( 𝑦 + 2 ) mod 5 ) ⟩ ) − 2 ) mod 5 ) ⟩ ) ) )
15 c0ex ⊢ 0 ∈ V
16 ovex ⊢ ( ( 𝑦 − 1 ) mod 5 ) ∈ V
17 15 16 opth ⊢ ( ⟨ 0 , ( ( 𝑦 − 1 ) mod 5 ) ⟩ = ⟨ 1 , ( ( ( 2nd ‘ ⟨ 1 , ( ( 𝑦 + 2 ) mod 5 ) ⟩ ) + 2 ) mod 5 ) ⟩ ↔ ( 0 = 1 ∧ ( ( 𝑦 − 1 ) mod 5 ) = ( ( ( 2nd ‘ ⟨ 1 , ( ( 𝑦 + 2 ) mod 5 ) ⟩ ) + 2 ) mod 5 ) ) )
18 0ne1 ⊢ 0 ≠ 1
19 eqneqall ⊢ ( 0 = 1 → ( 0 ≠ 1 → ¬ { ⟨ 1 , ( ( 𝑦 + 2 ) mod 5 ) ⟩ , ⟨ 0 , ( ( 𝑦 − 1 ) mod 5 ) ⟩ } ∈ 𝐸 ) )
20 18 19 mpi ⊢ ( 0 = 1 → ¬ { ⟨ 1 , ( ( 𝑦 + 2 ) mod 5 ) ⟩ , ⟨ 0 , ( ( 𝑦 − 1 ) mod 5 ) ⟩ } ∈ 𝐸 )
21 20 adantr ⊢ ( ( 0 = 1 ∧ ( ( 𝑦 − 1 ) mod 5 ) = ( ( ( 2nd ‘ ⟨ 1 , ( ( 𝑦 + 2 ) mod 5 ) ⟩ ) + 2 ) mod 5 ) ) → ¬ { ⟨ 1 , ( ( 𝑦 + 2 ) mod 5 ) ⟩ , ⟨ 0 , ( ( 𝑦 − 1 ) mod 5 ) ⟩ } ∈ 𝐸 )
22 17 21 sylbi ⊢ ( ⟨ 0 , ( ( 𝑦 − 1 ) mod 5 ) ⟩ = ⟨ 1 , ( ( ( 2nd ‘ ⟨ 1 , ( ( 𝑦 + 2 ) mod 5 ) ⟩ ) + 2 ) mod 5 ) ⟩ → ¬ { ⟨ 1 , ( ( 𝑦 + 2 ) mod 5 ) ⟩ , ⟨ 0 , ( ( 𝑦 − 1 ) mod 5 ) ⟩ } ∈ 𝐸 )
23 22 a1i ⊢ ( 𝑦 ∈ ( 0 ..^ 5 ) → ( ⟨ 0 , ( ( 𝑦 − 1 ) mod 5 ) ⟩ = ⟨ 1 , ( ( ( 2nd ‘ ⟨ 1 , ( ( 𝑦 + 2 ) mod 5 ) ⟩ ) + 2 ) mod 5 ) ⟩ → ¬ { ⟨ 1 , ( ( 𝑦 + 2 ) mod 5 ) ⟩ , ⟨ 0 , ( ( 𝑦 − 1 ) mod 5 ) ⟩ } ∈ 𝐸 ) )
24 15 16 opth ⊢ ( ⟨ 0 , ( ( 𝑦 − 1 ) mod 5 ) ⟩ = ⟨ 0 , ( 2nd ‘ ⟨ 1 , ( ( 𝑦 + 2 ) mod 5 ) ⟩ ) ⟩ ↔ ( 0 = 0 ∧ ( ( 𝑦 − 1 ) mod 5 ) = ( 2nd ‘ ⟨ 1 , ( ( 𝑦 + 2 ) mod 5 ) ⟩ ) ) )
25 6 7 op2nd ⊢ ( 2nd ‘ ⟨ 1 , ( ( 𝑦 + 2 ) mod 5 ) ⟩ ) = ( ( 𝑦 + 2 ) mod 5 )
26 25 eqeq2i ⊢ ( ( ( 𝑦 − 1 ) mod 5 ) = ( 2nd ‘ ⟨ 1 , ( ( 𝑦 + 2 ) mod 5 ) ⟩ ) ↔ ( ( 𝑦 − 1 ) mod 5 ) = ( ( 𝑦 + 2 ) mod 5 ) )
27 5nn ⊢ 5 ∈ ℕ
28 27 nnzi ⊢ 5 ∈ ℤ
29 uzid ⊢ ( 5 ∈ ℤ → 5 ∈ ( ℤ≥ ‘ 5 ) )
30 28 29 ax-mp ⊢ 5 ∈ ( ℤ≥ ‘ 5 )
31 eqid ⊢ ( 0 ..^ 5 ) = ( 0 ..^ 5 )
32 31 modm1nep2 ⊢ ( ( 5 ∈ ( ℤ≥ ‘ 5 ) ∧ 𝑦 ∈ ( 0 ..^ 5 ) ) → ( ( 𝑦 − 1 ) mod 5 ) ≠ ( ( 𝑦 + 2 ) mod 5 ) )
33 30 32 mpan ⊢ ( 𝑦 ∈ ( 0 ..^ 5 ) → ( ( 𝑦 − 1 ) mod 5 ) ≠ ( ( 𝑦 + 2 ) mod 5 ) )
34 eqneqall ⊢ ( ( ( 𝑦 − 1 ) mod 5 ) = ( ( 𝑦 + 2 ) mod 5 ) → ( ( ( 𝑦 − 1 ) mod 5 ) ≠ ( ( 𝑦 + 2 ) mod 5 ) → ¬ { ⟨ 1 , ( ( 𝑦 + 2 ) mod 5 ) ⟩ , ⟨ 0 , ( ( 𝑦 − 1 ) mod 5 ) ⟩ } ∈ 𝐸 ) )
35 33 34 syl5 ⊢ ( ( ( 𝑦 − 1 ) mod 5 ) = ( ( 𝑦 + 2 ) mod 5 ) → ( 𝑦 ∈ ( 0 ..^ 5 ) → ¬ { ⟨ 1 , ( ( 𝑦 + 2 ) mod 5 ) ⟩ , ⟨ 0 , ( ( 𝑦 − 1 ) mod 5 ) ⟩ } ∈ 𝐸 ) )
36 26 35 sylbi ⊢ ( ( ( 𝑦 − 1 ) mod 5 ) = ( 2nd ‘ ⟨ 1 , ( ( 𝑦 + 2 ) mod 5 ) ⟩ ) → ( 𝑦 ∈ ( 0 ..^ 5 ) → ¬ { ⟨ 1 , ( ( 𝑦 + 2 ) mod 5 ) ⟩ , ⟨ 0 , ( ( 𝑦 − 1 ) mod 5 ) ⟩ } ∈ 𝐸 ) )
37 24 36 simplbiim ⊢ ( ⟨ 0 , ( ( 𝑦 − 1 ) mod 5 ) ⟩ = ⟨ 0 , ( 2nd ‘ ⟨ 1 , ( ( 𝑦 + 2 ) mod 5 ) ⟩ ) ⟩ → ( 𝑦 ∈ ( 0 ..^ 5 ) → ¬ { ⟨ 1 , ( ( 𝑦 + 2 ) mod 5 ) ⟩ , ⟨ 0 , ( ( 𝑦 − 1 ) mod 5 ) ⟩ } ∈ 𝐸 ) )
38 37 com12 ⊢ ( 𝑦 ∈ ( 0 ..^ 5 ) → ( ⟨ 0 , ( ( 𝑦 − 1 ) mod 5 ) ⟩ = ⟨ 0 , ( 2nd ‘ ⟨ 1 , ( ( 𝑦 + 2 ) mod 5 ) ⟩ ) ⟩ → ¬ { ⟨ 1 , ( ( 𝑦 + 2 ) mod 5 ) ⟩ , ⟨ 0 , ( ( 𝑦 − 1 ) mod 5 ) ⟩ } ∈ 𝐸 ) )
39 15 16 opth ⊢ ( ⟨ 0 , ( ( 𝑦 − 1 ) mod 5 ) ⟩ = ⟨ 1 , ( ( ( 2nd ‘ ⟨ 1 , ( ( 𝑦 + 2 ) mod 5 ) ⟩ ) − 2 ) mod 5 ) ⟩ ↔ ( 0 = 1 ∧ ( ( 𝑦 − 1 ) mod 5 ) = ( ( ( 2nd ‘ ⟨ 1 , ( ( 𝑦 + 2 ) mod 5 ) ⟩ ) − 2 ) mod 5 ) ) )
40 20 adantr ⊢ ( ( 0 = 1 ∧ ( ( 𝑦 − 1 ) mod 5 ) = ( ( ( 2nd ‘ ⟨ 1 , ( ( 𝑦 + 2 ) mod 5 ) ⟩ ) − 2 ) mod 5 ) ) → ¬ { ⟨ 1 , ( ( 𝑦 + 2 ) mod 5 ) ⟩ , ⟨ 0 , ( ( 𝑦 − 1 ) mod 5 ) ⟩ } ∈ 𝐸 )
41 39 40 sylbi ⊢ ( ⟨ 0 , ( ( 𝑦 − 1 ) mod 5 ) ⟩ = ⟨ 1 , ( ( ( 2nd ‘ ⟨ 1 , ( ( 𝑦 + 2 ) mod 5 ) ⟩ ) − 2 ) mod 5 ) ⟩ → ¬ { ⟨ 1 , ( ( 𝑦 + 2 ) mod 5 ) ⟩ , ⟨ 0 , ( ( 𝑦 − 1 ) mod 5 ) ⟩ } ∈ 𝐸 )
42 41 a1i ⊢ ( 𝑦 ∈ ( 0 ..^ 5 ) → ( ⟨ 0 , ( ( 𝑦 − 1 ) mod 5 ) ⟩ = ⟨ 1 , ( ( ( 2nd ‘ ⟨ 1 , ( ( 𝑦 + 2 ) mod 5 ) ⟩ ) − 2 ) mod 5 ) ⟩ → ¬ { ⟨ 1 , ( ( 𝑦 + 2 ) mod 5 ) ⟩ , ⟨ 0 , ( ( 𝑦 − 1 ) mod 5 ) ⟩ } ∈ 𝐸 ) )
43 23 38 42 3jaod ⊢ ( 𝑦 ∈ ( 0 ..^ 5 ) → ( ( ⟨ 0 , ( ( 𝑦 − 1 ) mod 5 ) ⟩ = ⟨ 1 , ( ( ( 2nd ‘ ⟨ 1 , ( ( 𝑦 + 2 ) mod 5 ) ⟩ ) + 2 ) mod 5 ) ⟩ ∨ ⟨ 0 , ( ( 𝑦 − 1 ) mod 5 ) ⟩ = ⟨ 0 , ( 2nd ‘ ⟨ 1 , ( ( 𝑦 + 2 ) mod 5 ) ⟩ ) ⟩ ∨ ⟨ 0 , ( ( 𝑦 − 1 ) mod 5 ) ⟩ = ⟨ 1 , ( ( ( 2nd ‘ ⟨ 1 , ( ( 𝑦 + 2 ) mod 5 ) ⟩ ) − 2 ) mod 5 ) ⟩ ) → ¬ { ⟨ 1 , ( ( 𝑦 + 2 ) mod 5 ) ⟩ , ⟨ 0 , ( ( 𝑦 − 1 ) mod 5 ) ⟩ } ∈ 𝐸 ) )
44 14 43 syld ⊢ ( 𝑦 ∈ ( 0 ..^ 5 ) → ( { ⟨ 1 , ( ( 𝑦 + 2 ) mod 5 ) ⟩ , ⟨ 0 , ( ( 𝑦 − 1 ) mod 5 ) ⟩ } ∈ 𝐸 → ¬ { ⟨ 1 , ( ( 𝑦 + 2 ) mod 5 ) ⟩ , ⟨ 0 , ( ( 𝑦 − 1 ) mod 5 ) ⟩ } ∈ 𝐸 ) )
45 44 pm2.01d ⊢ ( 𝑦 ∈ ( 0 ..^ 5 ) → ¬ { ⟨ 1 , ( ( 𝑦 + 2 ) mod 5 ) ⟩ , ⟨ 0 , ( ( 𝑦 − 1 ) mod 5 ) ⟩ } ∈ 𝐸 )