Metamath Proof Explorer

Theorem gpgedgiov

Description: The edges of the generalized Petersen graph GPG(N,K) between an inside and an outside vertex. (Contributed by AV, 11-Nov-2025)

Ref Expression
Hypotheses gpgedgiov.j ⊢ 𝐽 = ( 1 ..^ ( ⌈ ‘ ( 𝑁 / 2 ) ) )
gpgedgiov.i ⊢ 𝐼 = ( 0 ..^ 𝑁 )
gpgedgiov.g ⊢ 𝐺 = ( 𝑁 gPetersenGr 𝐾 )
gpgedgiov.e ⊢ 𝐸 = ( Edg ‘ 𝐺 )
Assertion gpgedgiov ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝐼 ) ) → ( { ⟨ 0 , 𝑋 ⟩ , ⟨ 1 , 𝑌 ⟩ } ∈ 𝐸 ↔ 𝑋 = 𝑌 ) )

Proof

Step Hyp Ref Expression
1 gpgedgiov.j ⊢ 𝐽 = ( 1 ..^ ( ⌈ ‘ ( 𝑁 / 2 ) ) )
2 gpgedgiov.i ⊢ 𝐼 = ( 0 ..^ 𝑁 )
3 gpgedgiov.g ⊢ 𝐺 = ( 𝑁 gPetersenGr 𝐾 )
4 gpgedgiov.e ⊢ 𝐸 = ( Edg ‘ 𝐺 )
5 simpll ⊢ ( ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝐼 ) ) ∧ { ⟨ 0 , 𝑋 ⟩ , ⟨ 1 , 𝑌 ⟩ } ∈ 𝐸 ) → ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) )
6 c0ex ⊢ 0 ∈ V
7 6 a1i ⊢ ( 𝑌 ∈ 𝐼 → 0 ∈ V )
8 7 anim1i ⊢ ( ( 𝑌 ∈ 𝐼 ∧ 𝑋 ∈ 𝐼 ) → ( 0 ∈ V ∧ 𝑋 ∈ 𝐼 ) )
9 8 ancoms ⊢ ( ( 𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝐼 ) → ( 0 ∈ V ∧ 𝑋 ∈ 𝐼 ) )
10 op1stg ⊢ ( ( 0 ∈ V ∧ 𝑋 ∈ 𝐼 ) → ( 1st ‘ ⟨ 0 , 𝑋 ⟩ ) = 0 )
11 9 10 syl ⊢ ( ( 𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝐼 ) → ( 1st ‘ ⟨ 0 , 𝑋 ⟩ ) = 0 )
12 11 ad2antlr ⊢ ( ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝐼 ) ) ∧ { ⟨ 0 , 𝑋 ⟩ , ⟨ 1 , 𝑌 ⟩ } ∈ 𝐸 ) → ( 1st ‘ ⟨ 0 , 𝑋 ⟩ ) = 0 )
13 simpr ⊢ ( ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝐼 ) ) ∧ { ⟨ 0 , 𝑋 ⟩ , ⟨ 1 , 𝑌 ⟩ } ∈ 𝐸 ) → { ⟨ 0 , 𝑋 ⟩ , ⟨ 1 , 𝑌 ⟩ } ∈ 𝐸 )
14 eqid ⊢ ( Vtx ‘ 𝐺 ) = ( Vtx ‘ 𝐺 )
15 1 3 14 4 gpgvtxedg0 ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 1st ‘ ⟨ 0 , 𝑋 ⟩ ) = 0 ∧ { ⟨ 0 , 𝑋 ⟩ , ⟨ 1 , 𝑌 ⟩ } ∈ 𝐸 ) → ( ⟨ 1 , 𝑌 ⟩ = ⟨ 0 , ( ( ( 2nd ‘ ⟨ 0 , 𝑋 ⟩ ) + 1 ) mod 𝑁 ) ⟩ ∨ ⟨ 1 , 𝑌 ⟩ = ⟨ 1 , ( 2nd ‘ ⟨ 0 , 𝑋 ⟩ ) ⟩ ∨ ⟨ 1 , 𝑌 ⟩ = ⟨ 0 , ( ( ( 2nd ‘ ⟨ 0 , 𝑋 ⟩ ) − 1 ) mod 𝑁 ) ⟩ ) )
16 5 12 13 15 syl3anc ⊢ ( ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝐼 ) ) ∧ { ⟨ 0 , 𝑋 ⟩ , ⟨ 1 , 𝑌 ⟩ } ∈ 𝐸 ) → ( ⟨ 1 , 𝑌 ⟩ = ⟨ 0 , ( ( ( 2nd ‘ ⟨ 0 , 𝑋 ⟩ ) + 1 ) mod 𝑁 ) ⟩ ∨ ⟨ 1 , 𝑌 ⟩ = ⟨ 1 , ( 2nd ‘ ⟨ 0 , 𝑋 ⟩ ) ⟩ ∨ ⟨ 1 , 𝑌 ⟩ = ⟨ 0 , ( ( ( 2nd ‘ ⟨ 0 , 𝑋 ⟩ ) − 1 ) mod 𝑁 ) ⟩ ) )
17 16 ex ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝐼 ) ) → ( { ⟨ 0 , 𝑋 ⟩ , ⟨ 1 , 𝑌 ⟩ } ∈ 𝐸 → ( ⟨ 1 , 𝑌 ⟩ = ⟨ 0 , ( ( ( 2nd ‘ ⟨ 0 , 𝑋 ⟩ ) + 1 ) mod 𝑁 ) ⟩ ∨ ⟨ 1 , 𝑌 ⟩ = ⟨ 1 , ( 2nd ‘ ⟨ 0 , 𝑋 ⟩ ) ⟩ ∨ ⟨ 1 , 𝑌 ⟩ = ⟨ 0 , ( ( ( 2nd ‘ ⟨ 0 , 𝑋 ⟩ ) − 1 ) mod 𝑁 ) ⟩ ) ) )
18 ovex ⊢ ( ( 𝑋 + 1 ) mod 𝑁 ) ∈ V
19 6 18 pm3.2i ⊢ ( 0 ∈ V ∧ ( ( 𝑋 + 1 ) mod 𝑁 ) ∈ V )
20 opthg2 ⊢ ( ( 0 ∈ V ∧ ( ( 𝑋 + 1 ) mod 𝑁 ) ∈ V ) → ( ⟨ 1 , 𝑌 ⟩ = ⟨ 0 , ( ( 𝑋 + 1 ) mod 𝑁 ) ⟩ ↔ ( 1 = 0 ∧ 𝑌 = ( ( 𝑋 + 1 ) mod 𝑁 ) ) ) )
21 19 20 mp1i ⊢ ( ( 𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝐼 ) → ( ⟨ 1 , 𝑌 ⟩ = ⟨ 0 , ( ( 𝑋 + 1 ) mod 𝑁 ) ⟩ ↔ ( 1 = 0 ∧ 𝑌 = ( ( 𝑋 + 1 ) mod 𝑁 ) ) ) )
22 ax-1ne0 ⊢ 1 ≠ 0
23 eqneqall ⊢ ( 1 = 0 → ( 1 ≠ 0 → ( 𝑌 = ( ( 𝑋 + 1 ) mod 𝑁 ) → 𝑋 = 𝑌 ) ) )
24 22 23 mpi ⊢ ( 1 = 0 → ( 𝑌 = ( ( 𝑋 + 1 ) mod 𝑁 ) → 𝑋 = 𝑌 ) )
25 24 imp ⊢ ( ( 1 = 0 ∧ 𝑌 = ( ( 𝑋 + 1 ) mod 𝑁 ) ) → 𝑋 = 𝑌 )
26 21 25 biimtrdi ⊢ ( ( 𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝐼 ) → ( ⟨ 1 , 𝑌 ⟩ = ⟨ 0 , ( ( 𝑋 + 1 ) mod 𝑁 ) ⟩ → 𝑋 = 𝑌 ) )
27 1ex ⊢ 1 ∈ V
28 27 a1i ⊢ ( 𝑌 ∈ 𝐼 → 1 ∈ V )
29 28 anim1i ⊢ ( ( 𝑌 ∈ 𝐼 ∧ 𝑋 ∈ 𝐼 ) → ( 1 ∈ V ∧ 𝑋 ∈ 𝐼 ) )
30 29 ancoms ⊢ ( ( 𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝐼 ) → ( 1 ∈ V ∧ 𝑋 ∈ 𝐼 ) )
31 opthg2 ⊢ ( ( 1 ∈ V ∧ 𝑋 ∈ 𝐼 ) → ( ⟨ 1 , 𝑌 ⟩ = ⟨ 1 , 𝑋 ⟩ ↔ ( 1 = 1 ∧ 𝑌 = 𝑋 ) ) )
32 30 31 syl ⊢ ( ( 𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝐼 ) → ( ⟨ 1 , 𝑌 ⟩ = ⟨ 1 , 𝑋 ⟩ ↔ ( 1 = 1 ∧ 𝑌 = 𝑋 ) ) )
33 simpr ⊢ ( ( 1 = 1 ∧ 𝑌 = 𝑋 ) → 𝑌 = 𝑋 )
34 33 eqcomd ⊢ ( ( 1 = 1 ∧ 𝑌 = 𝑋 ) → 𝑋 = 𝑌 )
35 32 34 biimtrdi ⊢ ( ( 𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝐼 ) → ( ⟨ 1 , 𝑌 ⟩ = ⟨ 1 , 𝑋 ⟩ → 𝑋 = 𝑌 ) )
36 ovex ⊢ ( ( 𝑋 − 1 ) mod 𝑁 ) ∈ V
37 6 36 pm3.2i ⊢ ( 0 ∈ V ∧ ( ( 𝑋 − 1 ) mod 𝑁 ) ∈ V )
38 opthg2 ⊢ ( ( 0 ∈ V ∧ ( ( 𝑋 − 1 ) mod 𝑁 ) ∈ V ) → ( ⟨ 1 , 𝑌 ⟩ = ⟨ 0 , ( ( 𝑋 − 1 ) mod 𝑁 ) ⟩ ↔ ( 1 = 0 ∧ 𝑌 = ( ( 𝑋 − 1 ) mod 𝑁 ) ) ) )
39 37 38 mp1i ⊢ ( ( 𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝐼 ) → ( ⟨ 1 , 𝑌 ⟩ = ⟨ 0 , ( ( 𝑋 − 1 ) mod 𝑁 ) ⟩ ↔ ( 1 = 0 ∧ 𝑌 = ( ( 𝑋 − 1 ) mod 𝑁 ) ) ) )
40 eqneqall ⊢ ( 1 = 0 → ( 1 ≠ 0 → ( 𝑌 = ( ( 𝑋 − 1 ) mod 𝑁 ) → 𝑋 = 𝑌 ) ) )
41 22 40 mpi ⊢ ( 1 = 0 → ( 𝑌 = ( ( 𝑋 − 1 ) mod 𝑁 ) → 𝑋 = 𝑌 ) )
42 41 imp ⊢ ( ( 1 = 0 ∧ 𝑌 = ( ( 𝑋 − 1 ) mod 𝑁 ) ) → 𝑋 = 𝑌 )
43 39 42 biimtrdi ⊢ ( ( 𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝐼 ) → ( ⟨ 1 , 𝑌 ⟩ = ⟨ 0 , ( ( 𝑋 − 1 ) mod 𝑁 ) ⟩ → 𝑋 = 𝑌 ) )
44 26 35 43 3jaod ⊢ ( ( 𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝐼 ) → ( ( ⟨ 1 , 𝑌 ⟩ = ⟨ 0 , ( ( 𝑋 + 1 ) mod 𝑁 ) ⟩ ∨ ⟨ 1 , 𝑌 ⟩ = ⟨ 1 , 𝑋 ⟩ ∨ ⟨ 1 , 𝑌 ⟩ = ⟨ 0 , ( ( 𝑋 − 1 ) mod 𝑁 ) ⟩ ) → 𝑋 = 𝑌 ) )
45 op2ndg ⊢ ( ( 0 ∈ V ∧ 𝑋 ∈ 𝐼 ) → ( 2nd ‘ ⟨ 0 , 𝑋 ⟩ ) = 𝑋 )
46 9 45 syl ⊢ ( ( 𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝐼 ) → ( 2nd ‘ ⟨ 0 , 𝑋 ⟩ ) = 𝑋 )
47 oveq1 ⊢ ( ( 2nd ‘ ⟨ 0 , 𝑋 ⟩ ) = 𝑋 → ( ( 2nd ‘ ⟨ 0 , 𝑋 ⟩ ) + 1 ) = ( 𝑋 + 1 ) )
48 47 oveq1d ⊢ ( ( 2nd ‘ ⟨ 0 , 𝑋 ⟩ ) = 𝑋 → ( ( ( 2nd ‘ ⟨ 0 , 𝑋 ⟩ ) + 1 ) mod 𝑁 ) = ( ( 𝑋 + 1 ) mod 𝑁 ) )
49 48 opeq2d ⊢ ( ( 2nd ‘ ⟨ 0 , 𝑋 ⟩ ) = 𝑋 → ⟨ 0 , ( ( ( 2nd ‘ ⟨ 0 , 𝑋 ⟩ ) + 1 ) mod 𝑁 ) ⟩ = ⟨ 0 , ( ( 𝑋 + 1 ) mod 𝑁 ) ⟩ )
50 49 eqeq2d ⊢ ( ( 2nd ‘ ⟨ 0 , 𝑋 ⟩ ) = 𝑋 → ( ⟨ 1 , 𝑌 ⟩ = ⟨ 0 , ( ( ( 2nd ‘ ⟨ 0 , 𝑋 ⟩ ) + 1 ) mod 𝑁 ) ⟩ ↔ ⟨ 1 , 𝑌 ⟩ = ⟨ 0 , ( ( 𝑋 + 1 ) mod 𝑁 ) ⟩ ) )
51 opeq2 ⊢ ( ( 2nd ‘ ⟨ 0 , 𝑋 ⟩ ) = 𝑋 → ⟨ 1 , ( 2nd ‘ ⟨ 0 , 𝑋 ⟩ ) ⟩ = ⟨ 1 , 𝑋 ⟩ )
52 51 eqeq2d ⊢ ( ( 2nd ‘ ⟨ 0 , 𝑋 ⟩ ) = 𝑋 → ( ⟨ 1 , 𝑌 ⟩ = ⟨ 1 , ( 2nd ‘ ⟨ 0 , 𝑋 ⟩ ) ⟩ ↔ ⟨ 1 , 𝑌 ⟩ = ⟨ 1 , 𝑋 ⟩ ) )
53 oveq1 ⊢ ( ( 2nd ‘ ⟨ 0 , 𝑋 ⟩ ) = 𝑋 → ( ( 2nd ‘ ⟨ 0 , 𝑋 ⟩ ) − 1 ) = ( 𝑋 − 1 ) )
54 53 oveq1d ⊢ ( ( 2nd ‘ ⟨ 0 , 𝑋 ⟩ ) = 𝑋 → ( ( ( 2nd ‘ ⟨ 0 , 𝑋 ⟩ ) − 1 ) mod 𝑁 ) = ( ( 𝑋 − 1 ) mod 𝑁 ) )
55 54 opeq2d ⊢ ( ( 2nd ‘ ⟨ 0 , 𝑋 ⟩ ) = 𝑋 → ⟨ 0 , ( ( ( 2nd ‘ ⟨ 0 , 𝑋 ⟩ ) − 1 ) mod 𝑁 ) ⟩ = ⟨ 0 , ( ( 𝑋 − 1 ) mod 𝑁 ) ⟩ )
56 55 eqeq2d ⊢ ( ( 2nd ‘ ⟨ 0 , 𝑋 ⟩ ) = 𝑋 → ( ⟨ 1 , 𝑌 ⟩ = ⟨ 0 , ( ( ( 2nd ‘ ⟨ 0 , 𝑋 ⟩ ) − 1 ) mod 𝑁 ) ⟩ ↔ ⟨ 1 , 𝑌 ⟩ = ⟨ 0 , ( ( 𝑋 − 1 ) mod 𝑁 ) ⟩ ) )
57 50 52 56 3orbi123d ⊢ ( ( 2nd ‘ ⟨ 0 , 𝑋 ⟩ ) = 𝑋 → ( ( ⟨ 1 , 𝑌 ⟩ = ⟨ 0 , ( ( ( 2nd ‘ ⟨ 0 , 𝑋 ⟩ ) + 1 ) mod 𝑁 ) ⟩ ∨ ⟨ 1 , 𝑌 ⟩ = ⟨ 1 , ( 2nd ‘ ⟨ 0 , 𝑋 ⟩ ) ⟩ ∨ ⟨ 1 , 𝑌 ⟩ = ⟨ 0 , ( ( ( 2nd ‘ ⟨ 0 , 𝑋 ⟩ ) − 1 ) mod 𝑁 ) ⟩ ) ↔ ( ⟨ 1 , 𝑌 ⟩ = ⟨ 0 , ( ( 𝑋 + 1 ) mod 𝑁 ) ⟩ ∨ ⟨ 1 , 𝑌 ⟩ = ⟨ 1 , 𝑋 ⟩ ∨ ⟨ 1 , 𝑌 ⟩ = ⟨ 0 , ( ( 𝑋 − 1 ) mod 𝑁 ) ⟩ ) ) )
58 57 imbi1d ⊢ ( ( 2nd ‘ ⟨ 0 , 𝑋 ⟩ ) = 𝑋 → ( ( ( ⟨ 1 , 𝑌 ⟩ = ⟨ 0 , ( ( ( 2nd ‘ ⟨ 0 , 𝑋 ⟩ ) + 1 ) mod 𝑁 ) ⟩ ∨ ⟨ 1 , 𝑌 ⟩ = ⟨ 1 , ( 2nd ‘ ⟨ 0 , 𝑋 ⟩ ) ⟩ ∨ ⟨ 1 , 𝑌 ⟩ = ⟨ 0 , ( ( ( 2nd ‘ ⟨ 0 , 𝑋 ⟩ ) − 1 ) mod 𝑁 ) ⟩ ) → 𝑋 = 𝑌 ) ↔ ( ( ⟨ 1 , 𝑌 ⟩ = ⟨ 0 , ( ( 𝑋 + 1 ) mod 𝑁 ) ⟩ ∨ ⟨ 1 , 𝑌 ⟩ = ⟨ 1 , 𝑋 ⟩ ∨ ⟨ 1 , 𝑌 ⟩ = ⟨ 0 , ( ( 𝑋 − 1 ) mod 𝑁 ) ⟩ ) → 𝑋 = 𝑌 ) ) )
59 46 58 syl ⊢ ( ( 𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝐼 ) → ( ( ( ⟨ 1 , 𝑌 ⟩ = ⟨ 0 , ( ( ( 2nd ‘ ⟨ 0 , 𝑋 ⟩ ) + 1 ) mod 𝑁 ) ⟩ ∨ ⟨ 1 , 𝑌 ⟩ = ⟨ 1 , ( 2nd ‘ ⟨ 0 , 𝑋 ⟩ ) ⟩ ∨ ⟨ 1 , 𝑌 ⟩ = ⟨ 0 , ( ( ( 2nd ‘ ⟨ 0 , 𝑋 ⟩ ) − 1 ) mod 𝑁 ) ⟩ ) → 𝑋 = 𝑌 ) ↔ ( ( ⟨ 1 , 𝑌 ⟩ = ⟨ 0 , ( ( 𝑋 + 1 ) mod 𝑁 ) ⟩ ∨ ⟨ 1 , 𝑌 ⟩ = ⟨ 1 , 𝑋 ⟩ ∨ ⟨ 1 , 𝑌 ⟩ = ⟨ 0 , ( ( 𝑋 − 1 ) mod 𝑁 ) ⟩ ) → 𝑋 = 𝑌 ) ) )
60 44 59 mpbird ⊢ ( ( 𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝐼 ) → ( ( ⟨ 1 , 𝑌 ⟩ = ⟨ 0 , ( ( ( 2nd ‘ ⟨ 0 , 𝑋 ⟩ ) + 1 ) mod 𝑁 ) ⟩ ∨ ⟨ 1 , 𝑌 ⟩ = ⟨ 1 , ( 2nd ‘ ⟨ 0 , 𝑋 ⟩ ) ⟩ ∨ ⟨ 1 , 𝑌 ⟩ = ⟨ 0 , ( ( ( 2nd ‘ ⟨ 0 , 𝑋 ⟩ ) − 1 ) mod 𝑁 ) ⟩ ) → 𝑋 = 𝑌 ) )
61 60 adantl ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝐼 ) ) → ( ( ⟨ 1 , 𝑌 ⟩ = ⟨ 0 , ( ( ( 2nd ‘ ⟨ 0 , 𝑋 ⟩ ) + 1 ) mod 𝑁 ) ⟩ ∨ ⟨ 1 , 𝑌 ⟩ = ⟨ 1 , ( 2nd ‘ ⟨ 0 , 𝑋 ⟩ ) ⟩ ∨ ⟨ 1 , 𝑌 ⟩ = ⟨ 0 , ( ( ( 2nd ‘ ⟨ 0 , 𝑋 ⟩ ) − 1 ) mod 𝑁 ) ⟩ ) → 𝑋 = 𝑌 ) )
62 17 61 syld ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝐼 ) ) → ( { ⟨ 0 , 𝑋 ⟩ , ⟨ 1 , 𝑌 ⟩ } ∈ 𝐸 → 𝑋 = 𝑌 ) )
63 simpr ⊢ ( ( 𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝐼 ) → 𝑌 ∈ 𝐼 )
64 63 ad2antlr ⊢ ( ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝐼 ) ) ∧ 𝑋 = 𝑌 ) → 𝑌 ∈ 𝐼 )
65 opeq2 ⊢ ( 𝑥 = 𝑌 → ⟨ 0 , 𝑥 ⟩ = ⟨ 0 , 𝑌 ⟩ )
66 oveq1 ⊢ ( 𝑥 = 𝑌 → ( 𝑥 + 1 ) = ( 𝑌 + 1 ) )
67 66 oveq1d ⊢ ( 𝑥 = 𝑌 → ( ( 𝑥 + 1 ) mod 𝑁 ) = ( ( 𝑌 + 1 ) mod 𝑁 ) )
68 67 opeq2d ⊢ ( 𝑥 = 𝑌 → ⟨ 0 , ( ( 𝑥 + 1 ) mod 𝑁 ) ⟩ = ⟨ 0 , ( ( 𝑌 + 1 ) mod 𝑁 ) ⟩ )
69 65 68 preq12d ⊢ ( 𝑥 = 𝑌 → { ⟨ 0 , 𝑥 ⟩ , ⟨ 0 , ( ( 𝑥 + 1 ) mod 𝑁 ) ⟩ } = { ⟨ 0 , 𝑌 ⟩ , ⟨ 0 , ( ( 𝑌 + 1 ) mod 𝑁 ) ⟩ } )
70 69 eqeq2d ⊢ ( 𝑥 = 𝑌 → ( { ⟨ 0 , 𝑌 ⟩ , ⟨ 1 , 𝑌 ⟩ } = { ⟨ 0 , 𝑥 ⟩ , ⟨ 0 , ( ( 𝑥 + 1 ) mod 𝑁 ) ⟩ } ↔ { ⟨ 0 , 𝑌 ⟩ , ⟨ 1 , 𝑌 ⟩ } = { ⟨ 0 , 𝑌 ⟩ , ⟨ 0 , ( ( 𝑌 + 1 ) mod 𝑁 ) ⟩ } ) )
71 opeq2 ⊢ ( 𝑥 = 𝑌 → ⟨ 1 , 𝑥 ⟩ = ⟨ 1 , 𝑌 ⟩ )
72 65 71 preq12d ⊢ ( 𝑥 = 𝑌 → { ⟨ 0 , 𝑥 ⟩ , ⟨ 1 , 𝑥 ⟩ } = { ⟨ 0 , 𝑌 ⟩ , ⟨ 1 , 𝑌 ⟩ } )
73 72 eqeq2d ⊢ ( 𝑥 = 𝑌 → ( { ⟨ 0 , 𝑌 ⟩ , ⟨ 1 , 𝑌 ⟩ } = { ⟨ 0 , 𝑥 ⟩ , ⟨ 1 , 𝑥 ⟩ } ↔ { ⟨ 0 , 𝑌 ⟩ , ⟨ 1 , 𝑌 ⟩ } = { ⟨ 0 , 𝑌 ⟩ , ⟨ 1 , 𝑌 ⟩ } ) )
74 oveq1 ⊢ ( 𝑥 = 𝑌 → ( 𝑥 + 𝐾 ) = ( 𝑌 + 𝐾 ) )
75 74 oveq1d ⊢ ( 𝑥 = 𝑌 → ( ( 𝑥 + 𝐾 ) mod 𝑁 ) = ( ( 𝑌 + 𝐾 ) mod 𝑁 ) )
76 75 opeq2d ⊢ ( 𝑥 = 𝑌 → ⟨ 1 , ( ( 𝑥 + 𝐾 ) mod 𝑁 ) ⟩ = ⟨ 1 , ( ( 𝑌 + 𝐾 ) mod 𝑁 ) ⟩ )
77 71 76 preq12d ⊢ ( 𝑥 = 𝑌 → { ⟨ 1 , 𝑥 ⟩ , ⟨ 1 , ( ( 𝑥 + 𝐾 ) mod 𝑁 ) ⟩ } = { ⟨ 1 , 𝑌 ⟩ , ⟨ 1 , ( ( 𝑌 + 𝐾 ) mod 𝑁 ) ⟩ } )
78 77 eqeq2d ⊢ ( 𝑥 = 𝑌 → ( { ⟨ 0 , 𝑌 ⟩ , ⟨ 1 , 𝑌 ⟩ } = { ⟨ 1 , 𝑥 ⟩ , ⟨ 1 , ( ( 𝑥 + 𝐾 ) mod 𝑁 ) ⟩ } ↔ { ⟨ 0 , 𝑌 ⟩ , ⟨ 1 , 𝑌 ⟩ } = { ⟨ 1 , 𝑌 ⟩ , ⟨ 1 , ( ( 𝑌 + 𝐾 ) mod 𝑁 ) ⟩ } ) )
79 70 73 78 3orbi123d ⊢ ( 𝑥 = 𝑌 → ( ( { ⟨ 0 , 𝑌 ⟩ , ⟨ 1 , 𝑌 ⟩ } = { ⟨ 0 , 𝑥 ⟩ , ⟨ 0 , ( ( 𝑥 + 1 ) mod 𝑁 ) ⟩ } ∨ { ⟨ 0 , 𝑌 ⟩ , ⟨ 1 , 𝑌 ⟩ } = { ⟨ 0 , 𝑥 ⟩ , ⟨ 1 , 𝑥 ⟩ } ∨ { ⟨ 0 , 𝑌 ⟩ , ⟨ 1 , 𝑌 ⟩ } = { ⟨ 1 , 𝑥 ⟩ , ⟨ 1 , ( ( 𝑥 + 𝐾 ) mod 𝑁 ) ⟩ } ) ↔ ( { ⟨ 0 , 𝑌 ⟩ , ⟨ 1 , 𝑌 ⟩ } = { ⟨ 0 , 𝑌 ⟩ , ⟨ 0 , ( ( 𝑌 + 1 ) mod 𝑁 ) ⟩ } ∨ { ⟨ 0 , 𝑌 ⟩ , ⟨ 1 , 𝑌 ⟩ } = { ⟨ 0 , 𝑌 ⟩ , ⟨ 1 , 𝑌 ⟩ } ∨ { ⟨ 0 , 𝑌 ⟩ , ⟨ 1 , 𝑌 ⟩ } = { ⟨ 1 , 𝑌 ⟩ , ⟨ 1 , ( ( 𝑌 + 𝐾 ) mod 𝑁 ) ⟩ } ) ) )
80 79 adantl ⊢ ( ( ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝐼 ) ) ∧ 𝑋 = 𝑌 ) ∧ 𝑥 = 𝑌 ) → ( ( { ⟨ 0 , 𝑌 ⟩ , ⟨ 1 , 𝑌 ⟩ } = { ⟨ 0 , 𝑥 ⟩ , ⟨ 0 , ( ( 𝑥 + 1 ) mod 𝑁 ) ⟩ } ∨ { ⟨ 0 , 𝑌 ⟩ , ⟨ 1 , 𝑌 ⟩ } = { ⟨ 0 , 𝑥 ⟩ , ⟨ 1 , 𝑥 ⟩ } ∨ { ⟨ 0 , 𝑌 ⟩ , ⟨ 1 , 𝑌 ⟩ } = { ⟨ 1 , 𝑥 ⟩ , ⟨ 1 , ( ( 𝑥 + 𝐾 ) mod 𝑁 ) ⟩ } ) ↔ ( { ⟨ 0 , 𝑌 ⟩ , ⟨ 1 , 𝑌 ⟩ } = { ⟨ 0 , 𝑌 ⟩ , ⟨ 0 , ( ( 𝑌 + 1 ) mod 𝑁 ) ⟩ } ∨ { ⟨ 0 , 𝑌 ⟩ , ⟨ 1 , 𝑌 ⟩ } = { ⟨ 0 , 𝑌 ⟩ , ⟨ 1 , 𝑌 ⟩ } ∨ { ⟨ 0 , 𝑌 ⟩ , ⟨ 1 , 𝑌 ⟩ } = { ⟨ 1 , 𝑌 ⟩ , ⟨ 1 , ( ( 𝑌 + 𝐾 ) mod 𝑁 ) ⟩ } ) ) )
81 eqidd ⊢ ( ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝐼 ) ) ∧ 𝑋 = 𝑌 ) → { ⟨ 0 , 𝑌 ⟩ , ⟨ 1 , 𝑌 ⟩ } = { ⟨ 0 , 𝑌 ⟩ , ⟨ 1 , 𝑌 ⟩ } )
82 81 3mix2d ⊢ ( ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝐼 ) ) ∧ 𝑋 = 𝑌 ) → ( { ⟨ 0 , 𝑌 ⟩ , ⟨ 1 , 𝑌 ⟩ } = { ⟨ 0 , 𝑌 ⟩ , ⟨ 0 , ( ( 𝑌 + 1 ) mod 𝑁 ) ⟩ } ∨ { ⟨ 0 , 𝑌 ⟩ , ⟨ 1 , 𝑌 ⟩ } = { ⟨ 0 , 𝑌 ⟩ , ⟨ 1 , 𝑌 ⟩ } ∨ { ⟨ 0 , 𝑌 ⟩ , ⟨ 1 , 𝑌 ⟩ } = { ⟨ 1 , 𝑌 ⟩ , ⟨ 1 , ( ( 𝑌 + 𝐾 ) mod 𝑁 ) ⟩ } ) )
83 64 80 82 rspcedvd ⊢ ( ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝐼 ) ) ∧ 𝑋 = 𝑌 ) → ∃ 𝑥 ∈ 𝐼 ( { ⟨ 0 , 𝑌 ⟩ , ⟨ 1 , 𝑌 ⟩ } = { ⟨ 0 , 𝑥 ⟩ , ⟨ 0 , ( ( 𝑥 + 1 ) mod 𝑁 ) ⟩ } ∨ { ⟨ 0 , 𝑌 ⟩ , ⟨ 1 , 𝑌 ⟩ } = { ⟨ 0 , 𝑥 ⟩ , ⟨ 1 , 𝑥 ⟩ } ∨ { ⟨ 0 , 𝑌 ⟩ , ⟨ 1 , 𝑌 ⟩ } = { ⟨ 1 , 𝑥 ⟩ , ⟨ 1 , ( ( 𝑥 + 𝐾 ) mod 𝑁 ) ⟩ } ) )
84 2 1 3 4 gpgedgel ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) → ( { ⟨ 0 , 𝑌 ⟩ , ⟨ 1 , 𝑌 ⟩ } ∈ 𝐸 ↔ ∃ 𝑥 ∈ 𝐼 ( { ⟨ 0 , 𝑌 ⟩ , ⟨ 1 , 𝑌 ⟩ } = { ⟨ 0 , 𝑥 ⟩ , ⟨ 0 , ( ( 𝑥 + 1 ) mod 𝑁 ) ⟩ } ∨ { ⟨ 0 , 𝑌 ⟩ , ⟨ 1 , 𝑌 ⟩ } = { ⟨ 0 , 𝑥 ⟩ , ⟨ 1 , 𝑥 ⟩ } ∨ { ⟨ 0 , 𝑌 ⟩ , ⟨ 1 , 𝑌 ⟩ } = { ⟨ 1 , 𝑥 ⟩ , ⟨ 1 , ( ( 𝑥 + 𝐾 ) mod 𝑁 ) ⟩ } ) ) )
85 84 ad2antrr ⊢ ( ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝐼 ) ) ∧ 𝑋 = 𝑌 ) → ( { ⟨ 0 , 𝑌 ⟩ , ⟨ 1 , 𝑌 ⟩ } ∈ 𝐸 ↔ ∃ 𝑥 ∈ 𝐼 ( { ⟨ 0 , 𝑌 ⟩ , ⟨ 1 , 𝑌 ⟩ } = { ⟨ 0 , 𝑥 ⟩ , ⟨ 0 , ( ( 𝑥 + 1 ) mod 𝑁 ) ⟩ } ∨ { ⟨ 0 , 𝑌 ⟩ , ⟨ 1 , 𝑌 ⟩ } = { ⟨ 0 , 𝑥 ⟩ , ⟨ 1 , 𝑥 ⟩ } ∨ { ⟨ 0 , 𝑌 ⟩ , ⟨ 1 , 𝑌 ⟩ } = { ⟨ 1 , 𝑥 ⟩ , ⟨ 1 , ( ( 𝑥 + 𝐾 ) mod 𝑁 ) ⟩ } ) ) )
86 83 85 mpbird ⊢ ( ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝐼 ) ) ∧ 𝑋 = 𝑌 ) → { ⟨ 0 , 𝑌 ⟩ , ⟨ 1 , 𝑌 ⟩ } ∈ 𝐸 )
87 opeq2 ⊢ ( 𝑋 = 𝑌 → ⟨ 0 , 𝑋 ⟩ = ⟨ 0 , 𝑌 ⟩ )
88 87 preq1d ⊢ ( 𝑋 = 𝑌 → { ⟨ 0 , 𝑋 ⟩ , ⟨ 1 , 𝑌 ⟩ } = { ⟨ 0 , 𝑌 ⟩ , ⟨ 1 , 𝑌 ⟩ } )
89 88 eleq1d ⊢ ( 𝑋 = 𝑌 → ( { ⟨ 0 , 𝑋 ⟩ , ⟨ 1 , 𝑌 ⟩ } ∈ 𝐸 ↔ { ⟨ 0 , 𝑌 ⟩ , ⟨ 1 , 𝑌 ⟩ } ∈ 𝐸 ) )
90 89 adantl ⊢ ( ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝐼 ) ) ∧ 𝑋 = 𝑌 ) → ( { ⟨ 0 , 𝑋 ⟩ , ⟨ 1 , 𝑌 ⟩ } ∈ 𝐸 ↔ { ⟨ 0 , 𝑌 ⟩ , ⟨ 1 , 𝑌 ⟩ } ∈ 𝐸 ) )
91 86 90 mpbird ⊢ ( ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝐼 ) ) ∧ 𝑋 = 𝑌 ) → { ⟨ 0 , 𝑋 ⟩ , ⟨ 1 , 𝑌 ⟩ } ∈ 𝐸 )
92 91 ex ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝐼 ) ) → ( 𝑋 = 𝑌 → { ⟨ 0 , 𝑋 ⟩ , ⟨ 1 , 𝑌 ⟩ } ∈ 𝐸 ) )
93 62 92 impbid ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝐼 ) ) → ( { ⟨ 0 , 𝑋 ⟩ , ⟨ 1 , 𝑌 ⟩ } ∈ 𝐸 ↔ 𝑋 = 𝑌 ) )