Metamath Proof Explorer

Theorem gpgedg2ov

Description: The edges of the generalized Petersen graph GPG(N,K) between two outside vertices. (Contributed by AV, 15-Nov-2025)

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

Proof

Step Hyp Ref Expression
1 gpgedgiov.j ⊢ 𝐽 = ( 1 ..^ ( ⌈ ‘ ( 𝑁 / 2 ) ) )
2 gpgedgiov.i ⊢ 𝐼 = ( 0 ..^ 𝑁 )
3 gpgedgiov.g ⊢ 𝐺 = ( 𝑁 gPetersenGr 𝐾 )
4 gpgedgiov.e ⊢ 𝐸 = ( Edg ‘ 𝐺 )
5 prcom ⊢ { ⟨ 0 , ( ( 𝑌 − 1 ) mod 𝑁 ) ⟩ , ⟨ 0 , 𝑋 ⟩ } = { ⟨ 0 , 𝑋 ⟩ , ⟨ 0 , ( ( 𝑌 − 1 ) mod 𝑁 ) ⟩ }
6 5 eleq1i ⊢ ( { ⟨ 0 , ( ( 𝑌 − 1 ) mod 𝑁 ) ⟩ , ⟨ 0 , 𝑋 ⟩ } ∈ 𝐸 ↔ { ⟨ 0 , 𝑋 ⟩ , ⟨ 0 , ( ( 𝑌 − 1 ) mod 𝑁 ) ⟩ } ∈ 𝐸 )
7 uzuzle35 ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 5 ) → 𝑁 ∈ ( ℤ≥ ‘ 3 ) )
8 7 anim1i ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 5 ) ∧ 𝐾 ∈ 𝐽 ) → ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) )
9 8 adantr ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 5 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝐼 ) ) → ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) )
10 9 adantr ⊢ ( ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 5 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝐼 ) ) ∧ { ⟨ 0 , 𝑋 ⟩ , ⟨ 0 , ( ( 𝑌 − 1 ) mod 𝑁 ) ⟩ } ∈ 𝐸 ) → ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) )
11 c0ex ⊢ 0 ∈ V
12 11 a1i ⊢ ( 𝑌 ∈ 𝐼 → 0 ∈ V )
13 12 anim1i ⊢ ( ( 𝑌 ∈ 𝐼 ∧ 𝑋 ∈ 𝐼 ) → ( 0 ∈ V ∧ 𝑋 ∈ 𝐼 ) )
14 13 ancoms ⊢ ( ( 𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝐼 ) → ( 0 ∈ V ∧ 𝑋 ∈ 𝐼 ) )
15 op1stg ⊢ ( ( 0 ∈ V ∧ 𝑋 ∈ 𝐼 ) → ( 1st ‘ ⟨ 0 , 𝑋 ⟩ ) = 0 )
16 14 15 syl ⊢ ( ( 𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝐼 ) → ( 1st ‘ ⟨ 0 , 𝑋 ⟩ ) = 0 )
17 16 adantl ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 5 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝐼 ) ) → ( 1st ‘ ⟨ 0 , 𝑋 ⟩ ) = 0 )
18 17 adantr ⊢ ( ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 5 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝐼 ) ) ∧ { ⟨ 0 , 𝑋 ⟩ , ⟨ 0 , ( ( 𝑌 − 1 ) mod 𝑁 ) ⟩ } ∈ 𝐸 ) → ( 1st ‘ ⟨ 0 , 𝑋 ⟩ ) = 0 )
19 simpr ⊢ ( ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 5 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝐼 ) ) ∧ { ⟨ 0 , 𝑋 ⟩ , ⟨ 0 , ( ( 𝑌 − 1 ) mod 𝑁 ) ⟩ } ∈ 𝐸 ) → { ⟨ 0 , 𝑋 ⟩ , ⟨ 0 , ( ( 𝑌 − 1 ) mod 𝑁 ) ⟩ } ∈ 𝐸 )
20 eqid ⊢ ( Vtx ‘ 𝐺 ) = ( Vtx ‘ 𝐺 )
21 1 3 20 4 gpgvtxedg0 ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 1st ‘ ⟨ 0 , 𝑋 ⟩ ) = 0 ∧ { ⟨ 0 , 𝑋 ⟩ , ⟨ 0 , ( ( 𝑌 − 1 ) mod 𝑁 ) ⟩ } ∈ 𝐸 ) → ( ⟨ 0 , ( ( 𝑌 − 1 ) mod 𝑁 ) ⟩ = ⟨ 0 , ( ( ( 2nd ‘ ⟨ 0 , 𝑋 ⟩ ) + 1 ) mod 𝑁 ) ⟩ ∨ ⟨ 0 , ( ( 𝑌 − 1 ) mod 𝑁 ) ⟩ = ⟨ 1 , ( 2nd ‘ ⟨ 0 , 𝑋 ⟩ ) ⟩ ∨ ⟨ 0 , ( ( 𝑌 − 1 ) mod 𝑁 ) ⟩ = ⟨ 0 , ( ( ( 2nd ‘ ⟨ 0 , 𝑋 ⟩ ) − 1 ) mod 𝑁 ) ⟩ ) )
22 10 18 19 21 syl3anc ⊢ ( ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 5 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝐼 ) ) ∧ { ⟨ 0 , 𝑋 ⟩ , ⟨ 0 , ( ( 𝑌 − 1 ) mod 𝑁 ) ⟩ } ∈ 𝐸 ) → ( ⟨ 0 , ( ( 𝑌 − 1 ) mod 𝑁 ) ⟩ = ⟨ 0 , ( ( ( 2nd ‘ ⟨ 0 , 𝑋 ⟩ ) + 1 ) mod 𝑁 ) ⟩ ∨ ⟨ 0 , ( ( 𝑌 − 1 ) mod 𝑁 ) ⟩ = ⟨ 1 , ( 2nd ‘ ⟨ 0 , 𝑋 ⟩ ) ⟩ ∨ ⟨ 0 , ( ( 𝑌 − 1 ) mod 𝑁 ) ⟩ = ⟨ 0 , ( ( ( 2nd ‘ ⟨ 0 , 𝑋 ⟩ ) − 1 ) mod 𝑁 ) ⟩ ) )
23 22 ex ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 5 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝐼 ) ) → ( { ⟨ 0 , 𝑋 ⟩ , ⟨ 0 , ( ( 𝑌 − 1 ) mod 𝑁 ) ⟩ } ∈ 𝐸 → ( ⟨ 0 , ( ( 𝑌 − 1 ) mod 𝑁 ) ⟩ = ⟨ 0 , ( ( ( 2nd ‘ ⟨ 0 , 𝑋 ⟩ ) + 1 ) mod 𝑁 ) ⟩ ∨ ⟨ 0 , ( ( 𝑌 − 1 ) mod 𝑁 ) ⟩ = ⟨ 1 , ( 2nd ‘ ⟨ 0 , 𝑋 ⟩ ) ⟩ ∨ ⟨ 0 , ( ( 𝑌 − 1 ) mod 𝑁 ) ⟩ = ⟨ 0 , ( ( ( 2nd ‘ ⟨ 0 , 𝑋 ⟩ ) − 1 ) mod 𝑁 ) ⟩ ) ) )
24 6 23 biimtrid ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 5 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝐼 ) ) → ( { ⟨ 0 , ( ( 𝑌 − 1 ) mod 𝑁 ) ⟩ , ⟨ 0 , 𝑋 ⟩ } ∈ 𝐸 → ( ⟨ 0 , ( ( 𝑌 − 1 ) mod 𝑁 ) ⟩ = ⟨ 0 , ( ( ( 2nd ‘ ⟨ 0 , 𝑋 ⟩ ) + 1 ) mod 𝑁 ) ⟩ ∨ ⟨ 0 , ( ( 𝑌 − 1 ) mod 𝑁 ) ⟩ = ⟨ 1 , ( 2nd ‘ ⟨ 0 , 𝑋 ⟩ ) ⟩ ∨ ⟨ 0 , ( ( 𝑌 − 1 ) mod 𝑁 ) ⟩ = ⟨ 0 , ( ( ( 2nd ‘ ⟨ 0 , 𝑋 ⟩ ) − 1 ) mod 𝑁 ) ⟩ ) ) )
25 9 adantr ⊢ ( ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 5 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝐼 ) ) ∧ { ⟨ 0 , 𝑋 ⟩ , ⟨ 0 , ( ( 𝑌 + 1 ) mod 𝑁 ) ⟩ } ∈ 𝐸 ) → ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) )
26 17 adantr ⊢ ( ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 5 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝐼 ) ) ∧ { ⟨ 0 , 𝑋 ⟩ , ⟨ 0 , ( ( 𝑌 + 1 ) mod 𝑁 ) ⟩ } ∈ 𝐸 ) → ( 1st ‘ ⟨ 0 , 𝑋 ⟩ ) = 0 )
27 simpr ⊢ ( ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 5 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝐼 ) ) ∧ { ⟨ 0 , 𝑋 ⟩ , ⟨ 0 , ( ( 𝑌 + 1 ) mod 𝑁 ) ⟩ } ∈ 𝐸 ) → { ⟨ 0 , 𝑋 ⟩ , ⟨ 0 , ( ( 𝑌 + 1 ) mod 𝑁 ) ⟩ } ∈ 𝐸 )
28 1 3 20 4 gpgvtxedg0 ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 1st ‘ ⟨ 0 , 𝑋 ⟩ ) = 0 ∧ { ⟨ 0 , 𝑋 ⟩ , ⟨ 0 , ( ( 𝑌 + 1 ) mod 𝑁 ) ⟩ } ∈ 𝐸 ) → ( ⟨ 0 , ( ( 𝑌 + 1 ) mod 𝑁 ) ⟩ = ⟨ 0 , ( ( ( 2nd ‘ ⟨ 0 , 𝑋 ⟩ ) + 1 ) mod 𝑁 ) ⟩ ∨ ⟨ 0 , ( ( 𝑌 + 1 ) mod 𝑁 ) ⟩ = ⟨ 1 , ( 2nd ‘ ⟨ 0 , 𝑋 ⟩ ) ⟩ ∨ ⟨ 0 , ( ( 𝑌 + 1 ) mod 𝑁 ) ⟩ = ⟨ 0 , ( ( ( 2nd ‘ ⟨ 0 , 𝑋 ⟩ ) − 1 ) mod 𝑁 ) ⟩ ) )
29 25 26 27 28 syl3anc ⊢ ( ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 5 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝐼 ) ) ∧ { ⟨ 0 , 𝑋 ⟩ , ⟨ 0 , ( ( 𝑌 + 1 ) mod 𝑁 ) ⟩ } ∈ 𝐸 ) → ( ⟨ 0 , ( ( 𝑌 + 1 ) mod 𝑁 ) ⟩ = ⟨ 0 , ( ( ( 2nd ‘ ⟨ 0 , 𝑋 ⟩ ) + 1 ) mod 𝑁 ) ⟩ ∨ ⟨ 0 , ( ( 𝑌 + 1 ) mod 𝑁 ) ⟩ = ⟨ 1 , ( 2nd ‘ ⟨ 0 , 𝑋 ⟩ ) ⟩ ∨ ⟨ 0 , ( ( 𝑌 + 1 ) mod 𝑁 ) ⟩ = ⟨ 0 , ( ( ( 2nd ‘ ⟨ 0 , 𝑋 ⟩ ) − 1 ) mod 𝑁 ) ⟩ ) )
30 29 ex ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 5 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝐼 ) ) → ( { ⟨ 0 , 𝑋 ⟩ , ⟨ 0 , ( ( 𝑌 + 1 ) mod 𝑁 ) ⟩ } ∈ 𝐸 → ( ⟨ 0 , ( ( 𝑌 + 1 ) mod 𝑁 ) ⟩ = ⟨ 0 , ( ( ( 2nd ‘ ⟨ 0 , 𝑋 ⟩ ) + 1 ) mod 𝑁 ) ⟩ ∨ ⟨ 0 , ( ( 𝑌 + 1 ) mod 𝑁 ) ⟩ = ⟨ 1 , ( 2nd ‘ ⟨ 0 , 𝑋 ⟩ ) ⟩ ∨ ⟨ 0 , ( ( 𝑌 + 1 ) mod 𝑁 ) ⟩ = ⟨ 0 , ( ( ( 2nd ‘ ⟨ 0 , 𝑋 ⟩ ) − 1 ) mod 𝑁 ) ⟩ ) ) )
31 ovex ⊢ ( ( 𝑌 + 1 ) mod 𝑁 ) ∈ V
32 11 31 opth ⊢ ( ⟨ 0 , ( ( 𝑌 + 1 ) mod 𝑁 ) ⟩ = ⟨ 0 , ( ( 𝑋 + 1 ) mod 𝑁 ) ⟩ ↔ ( 0 = 0 ∧ ( ( 𝑌 + 1 ) mod 𝑁 ) = ( ( 𝑋 + 1 ) mod 𝑁 ) ) )
33 7 adantr ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 5 ) ∧ 𝐾 ∈ 𝐽 ) → 𝑁 ∈ ( ℤ≥ ‘ 3 ) )
34 33 adantr ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 5 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝐼 ) ) → 𝑁 ∈ ( ℤ≥ ‘ 3 ) )
35 simpr ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 5 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝐼 ) ) → ( 𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝐼 ) )
36 35 ancomd ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 5 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝐼 ) ) → ( 𝑌 ∈ 𝐼 ∧ 𝑋 ∈ 𝐼 ) )
37 1zzd ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 5 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝐼 ) ) → 1 ∈ ℤ )
38 2 modaddid ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ ( 𝑌 ∈ 𝐼 ∧ 𝑋 ∈ 𝐼 ) ∧ 1 ∈ ℤ ) → ( ( ( 𝑌 + 1 ) mod 𝑁 ) = ( ( 𝑋 + 1 ) mod 𝑁 ) ↔ 𝑌 = 𝑋 ) )
39 34 36 37 38 syl3anc ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 5 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝐼 ) ) → ( ( ( 𝑌 + 1 ) mod 𝑁 ) = ( ( 𝑋 + 1 ) mod 𝑁 ) ↔ 𝑌 = 𝑋 ) )
40 39 biimpa ⊢ ( ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 5 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝐼 ) ) ∧ ( ( 𝑌 + 1 ) mod 𝑁 ) = ( ( 𝑋 + 1 ) mod 𝑁 ) ) → 𝑌 = 𝑋 )
41 40 eqcomd ⊢ ( ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 5 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝐼 ) ) ∧ ( ( 𝑌 + 1 ) mod 𝑁 ) = ( ( 𝑋 + 1 ) mod 𝑁 ) ) → 𝑋 = 𝑌 )
42 41 ex ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 5 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝐼 ) ) → ( ( ( 𝑌 + 1 ) mod 𝑁 ) = ( ( 𝑋 + 1 ) mod 𝑁 ) → 𝑋 = 𝑌 ) )
43 42 adantld ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 5 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝐼 ) ) → ( ( 0 = 0 ∧ ( ( 𝑌 + 1 ) mod 𝑁 ) = ( ( 𝑋 + 1 ) mod 𝑁 ) ) → 𝑋 = 𝑌 ) )
44 32 43 biimtrid ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 5 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝐼 ) ) → ( ⟨ 0 , ( ( 𝑌 + 1 ) mod 𝑁 ) ⟩ = ⟨ 0 , ( ( 𝑋 + 1 ) mod 𝑁 ) ⟩ → 𝑋 = 𝑌 ) )
45 44 imp ⊢ ( ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 5 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝐼 ) ) ∧ ⟨ 0 , ( ( 𝑌 + 1 ) mod 𝑁 ) ⟩ = ⟨ 0 , ( ( 𝑋 + 1 ) mod 𝑁 ) ⟩ ) → 𝑋 = 𝑌 )
46 45 a1d ⊢ ( ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 5 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝐼 ) ) ∧ ⟨ 0 , ( ( 𝑌 + 1 ) mod 𝑁 ) ⟩ = ⟨ 0 , ( ( 𝑋 + 1 ) mod 𝑁 ) ⟩ ) → ( ( ⟨ 0 , ( ( 𝑌 − 1 ) mod 𝑁 ) ⟩ = ⟨ 0 , ( ( 𝑋 + 1 ) mod 𝑁 ) ⟩ ∨ ⟨ 0 , ( ( 𝑌 − 1 ) mod 𝑁 ) ⟩ = ⟨ 1 , 𝑋 ⟩ ∨ ⟨ 0 , ( ( 𝑌 − 1 ) mod 𝑁 ) ⟩ = ⟨ 0 , ( ( 𝑋 − 1 ) mod 𝑁 ) ⟩ ) → 𝑋 = 𝑌 ) )
47 46 ex ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 5 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝐼 ) ) → ( ⟨ 0 , ( ( 𝑌 + 1 ) mod 𝑁 ) ⟩ = ⟨ 0 , ( ( 𝑋 + 1 ) mod 𝑁 ) ⟩ → ( ( ⟨ 0 , ( ( 𝑌 − 1 ) mod 𝑁 ) ⟩ = ⟨ 0 , ( ( 𝑋 + 1 ) mod 𝑁 ) ⟩ ∨ ⟨ 0 , ( ( 𝑌 − 1 ) mod 𝑁 ) ⟩ = ⟨ 1 , 𝑋 ⟩ ∨ ⟨ 0 , ( ( 𝑌 − 1 ) mod 𝑁 ) ⟩ = ⟨ 0 , ( ( 𝑋 − 1 ) mod 𝑁 ) ⟩ ) → 𝑋 = 𝑌 ) ) )
48 11 31 opth ⊢ ( ⟨ 0 , ( ( 𝑌 + 1 ) mod 𝑁 ) ⟩ = ⟨ 1 , 𝑋 ⟩ ↔ ( 0 = 1 ∧ ( ( 𝑌 + 1 ) mod 𝑁 ) = 𝑋 ) )
49 0ne1 ⊢ 0 ≠ 1
50 eqneqall ⊢ ( 0 = 1 → ( 0 ≠ 1 → ( ( ( 𝑌 + 1 ) mod 𝑁 ) = 𝑋 → ( ⟨ 0 , ( ( 𝑌 − 1 ) mod 𝑁 ) ⟩ = ⟨ 0 , ( ( 𝑋 + 1 ) mod 𝑁 ) ⟩ → 𝑋 = 𝑌 ) ) ) )
51 49 50 mpi ⊢ ( 0 = 1 → ( ( ( 𝑌 + 1 ) mod 𝑁 ) = 𝑋 → ( ⟨ 0 , ( ( 𝑌 − 1 ) mod 𝑁 ) ⟩ = ⟨ 0 , ( ( 𝑋 + 1 ) mod 𝑁 ) ⟩ → 𝑋 = 𝑌 ) ) )
52 51 imp ⊢ ( ( 0 = 1 ∧ ( ( 𝑌 + 1 ) mod 𝑁 ) = 𝑋 ) → ( ⟨ 0 , ( ( 𝑌 − 1 ) mod 𝑁 ) ⟩ = ⟨ 0 , ( ( 𝑋 + 1 ) mod 𝑁 ) ⟩ → 𝑋 = 𝑌 ) )
53 52 a1i ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 5 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝐼 ) ) → ( ( 0 = 1 ∧ ( ( 𝑌 + 1 ) mod 𝑁 ) = 𝑋 ) → ( ⟨ 0 , ( ( 𝑌 − 1 ) mod 𝑁 ) ⟩ = ⟨ 0 , ( ( 𝑋 + 1 ) mod 𝑁 ) ⟩ → 𝑋 = 𝑌 ) ) )
54 48 53 biimtrid ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 5 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝐼 ) ) → ( ⟨ 0 , ( ( 𝑌 + 1 ) mod 𝑁 ) ⟩ = ⟨ 1 , 𝑋 ⟩ → ( ⟨ 0 , ( ( 𝑌 − 1 ) mod 𝑁 ) ⟩ = ⟨ 0 , ( ( 𝑋 + 1 ) mod 𝑁 ) ⟩ → 𝑋 = 𝑌 ) ) )
55 54 imp ⊢ ( ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 5 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝐼 ) ) ∧ ⟨ 0 , ( ( 𝑌 + 1 ) mod 𝑁 ) ⟩ = ⟨ 1 , 𝑋 ⟩ ) → ( ⟨ 0 , ( ( 𝑌 − 1 ) mod 𝑁 ) ⟩ = ⟨ 0 , ( ( 𝑋 + 1 ) mod 𝑁 ) ⟩ → 𝑋 = 𝑌 ) )
56 eqeq2 ⊢ ( ⟨ 1 , 𝑋 ⟩ = ⟨ 0 , ( ( 𝑌 + 1 ) mod 𝑁 ) ⟩ → ( ⟨ 0 , ( ( 𝑌 − 1 ) mod 𝑁 ) ⟩ = ⟨ 1 , 𝑋 ⟩ ↔ ⟨ 0 , ( ( 𝑌 − 1 ) mod 𝑁 ) ⟩ = ⟨ 0 , ( ( 𝑌 + 1 ) mod 𝑁 ) ⟩ ) )
57 56 eqcoms ⊢ ( ⟨ 0 , ( ( 𝑌 + 1 ) mod 𝑁 ) ⟩ = ⟨ 1 , 𝑋 ⟩ → ( ⟨ 0 , ( ( 𝑌 − 1 ) mod 𝑁 ) ⟩ = ⟨ 1 , 𝑋 ⟩ ↔ ⟨ 0 , ( ( 𝑌 − 1 ) mod 𝑁 ) ⟩ = ⟨ 0 , ( ( 𝑌 + 1 ) mod 𝑁 ) ⟩ ) )
58 57 adantl ⊢ ( ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 5 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝐼 ) ) ∧ ⟨ 0 , ( ( 𝑌 + 1 ) mod 𝑁 ) ⟩ = ⟨ 1 , 𝑋 ⟩ ) → ( ⟨ 0 , ( ( 𝑌 − 1 ) mod 𝑁 ) ⟩ = ⟨ 1 , 𝑋 ⟩ ↔ ⟨ 0 , ( ( 𝑌 − 1 ) mod 𝑁 ) ⟩ = ⟨ 0 , ( ( 𝑌 + 1 ) mod 𝑁 ) ⟩ ) )
59 ovex ⊢ ( ( 𝑌 − 1 ) mod 𝑁 ) ∈ V
60 11 59 opth ⊢ ( ⟨ 0 , ( ( 𝑌 − 1 ) mod 𝑁 ) ⟩ = ⟨ 0 , ( ( 𝑌 + 1 ) mod 𝑁 ) ⟩ ↔ ( 0 = 0 ∧ ( ( 𝑌 − 1 ) mod 𝑁 ) = ( ( 𝑌 + 1 ) mod 𝑁 ) ) )
61 simpr ⊢ ( ( 𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝐼 ) → 𝑌 ∈ 𝐼 )
62 2 modm1nep1 ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝑌 ∈ 𝐼 ) → ( ( 𝑌 − 1 ) mod 𝑁 ) ≠ ( ( 𝑌 + 1 ) mod 𝑁 ) )
63 33 61 62 syl2an ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 5 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝐼 ) ) → ( ( 𝑌 − 1 ) mod 𝑁 ) ≠ ( ( 𝑌 + 1 ) mod 𝑁 ) )
64 eqneqall ⊢ ( ( ( 𝑌 − 1 ) mod 𝑁 ) = ( ( 𝑌 + 1 ) mod 𝑁 ) → ( ( ( 𝑌 − 1 ) mod 𝑁 ) ≠ ( ( 𝑌 + 1 ) mod 𝑁 ) → 𝑋 = 𝑌 ) )
65 64 com12 ⊢ ( ( ( 𝑌 − 1 ) mod 𝑁 ) ≠ ( ( 𝑌 + 1 ) mod 𝑁 ) → ( ( ( 𝑌 − 1 ) mod 𝑁 ) = ( ( 𝑌 + 1 ) mod 𝑁 ) → 𝑋 = 𝑌 ) )
66 63 65 syl ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 5 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝐼 ) ) → ( ( ( 𝑌 − 1 ) mod 𝑁 ) = ( ( 𝑌 + 1 ) mod 𝑁 ) → 𝑋 = 𝑌 ) )
67 66 adantld ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 5 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝐼 ) ) → ( ( 0 = 0 ∧ ( ( 𝑌 − 1 ) mod 𝑁 ) = ( ( 𝑌 + 1 ) mod 𝑁 ) ) → 𝑋 = 𝑌 ) )
68 60 67 biimtrid ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 5 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝐼 ) ) → ( ⟨ 0 , ( ( 𝑌 − 1 ) mod 𝑁 ) ⟩ = ⟨ 0 , ( ( 𝑌 + 1 ) mod 𝑁 ) ⟩ → 𝑋 = 𝑌 ) )
69 68 adantr ⊢ ( ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 5 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝐼 ) ) ∧ ⟨ 0 , ( ( 𝑌 + 1 ) mod 𝑁 ) ⟩ = ⟨ 1 , 𝑋 ⟩ ) → ( ⟨ 0 , ( ( 𝑌 − 1 ) mod 𝑁 ) ⟩ = ⟨ 0 , ( ( 𝑌 + 1 ) mod 𝑁 ) ⟩ → 𝑋 = 𝑌 ) )
70 58 69 sylbid ⊢ ( ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 5 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝐼 ) ) ∧ ⟨ 0 , ( ( 𝑌 + 1 ) mod 𝑁 ) ⟩ = ⟨ 1 , 𝑋 ⟩ ) → ( ⟨ 0 , ( ( 𝑌 − 1 ) mod 𝑁 ) ⟩ = ⟨ 1 , 𝑋 ⟩ → 𝑋 = 𝑌 ) )
71 49 orci ⊢ ( 0 ≠ 1 ∨ ( ( 𝑌 + 1 ) mod 𝑁 ) ≠ 𝑋 )
72 11 31 opthne ⊢ ( ⟨ 0 , ( ( 𝑌 + 1 ) mod 𝑁 ) ⟩ ≠ ⟨ 1 , 𝑋 ⟩ ↔ ( 0 ≠ 1 ∨ ( ( 𝑌 + 1 ) mod 𝑁 ) ≠ 𝑋 ) )
73 71 72 mpbir ⊢ ⟨ 0 , ( ( 𝑌 + 1 ) mod 𝑁 ) ⟩ ≠ ⟨ 1 , 𝑋 ⟩
74 73 a1i ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 5 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝐼 ) ) → ⟨ 0 , ( ( 𝑌 + 1 ) mod 𝑁 ) ⟩ ≠ ⟨ 1 , 𝑋 ⟩ )
75 eqneqall ⊢ ( ⟨ 0 , ( ( 𝑌 + 1 ) mod 𝑁 ) ⟩ = ⟨ 1 , 𝑋 ⟩ → ( ⟨ 0 , ( ( 𝑌 + 1 ) mod 𝑁 ) ⟩ ≠ ⟨ 1 , 𝑋 ⟩ → ( ⟨ 0 , ( ( 𝑌 − 1 ) mod 𝑁 ) ⟩ = ⟨ 0 , ( ( 𝑋 − 1 ) mod 𝑁 ) ⟩ → 𝑋 = 𝑌 ) ) )
76 75 com12 ⊢ ( ⟨ 0 , ( ( 𝑌 + 1 ) mod 𝑁 ) ⟩ ≠ ⟨ 1 , 𝑋 ⟩ → ( ⟨ 0 , ( ( 𝑌 + 1 ) mod 𝑁 ) ⟩ = ⟨ 1 , 𝑋 ⟩ → ( ⟨ 0 , ( ( 𝑌 − 1 ) mod 𝑁 ) ⟩ = ⟨ 0 , ( ( 𝑋 − 1 ) mod 𝑁 ) ⟩ → 𝑋 = 𝑌 ) ) )
77 74 76 syl ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 5 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝐼 ) ) → ( ⟨ 0 , ( ( 𝑌 + 1 ) mod 𝑁 ) ⟩ = ⟨ 1 , 𝑋 ⟩ → ( ⟨ 0 , ( ( 𝑌 − 1 ) mod 𝑁 ) ⟩ = ⟨ 0 , ( ( 𝑋 − 1 ) mod 𝑁 ) ⟩ → 𝑋 = 𝑌 ) ) )
78 77 imp ⊢ ( ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 5 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝐼 ) ) ∧ ⟨ 0 , ( ( 𝑌 + 1 ) mod 𝑁 ) ⟩ = ⟨ 1 , 𝑋 ⟩ ) → ( ⟨ 0 , ( ( 𝑌 − 1 ) mod 𝑁 ) ⟩ = ⟨ 0 , ( ( 𝑋 − 1 ) mod 𝑁 ) ⟩ → 𝑋 = 𝑌 ) )
79 55 70 78 3jaod ⊢ ( ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 5 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝐼 ) ) ∧ ⟨ 0 , ( ( 𝑌 + 1 ) mod 𝑁 ) ⟩ = ⟨ 1 , 𝑋 ⟩ ) → ( ( ⟨ 0 , ( ( 𝑌 − 1 ) mod 𝑁 ) ⟩ = ⟨ 0 , ( ( 𝑋 + 1 ) mod 𝑁 ) ⟩ ∨ ⟨ 0 , ( ( 𝑌 − 1 ) mod 𝑁 ) ⟩ = ⟨ 1 , 𝑋 ⟩ ∨ ⟨ 0 , ( ( 𝑌 − 1 ) mod 𝑁 ) ⟩ = ⟨ 0 , ( ( 𝑋 − 1 ) mod 𝑁 ) ⟩ ) → 𝑋 = 𝑌 ) )
80 79 ex ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 5 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝐼 ) ) → ( ⟨ 0 , ( ( 𝑌 + 1 ) mod 𝑁 ) ⟩ = ⟨ 1 , 𝑋 ⟩ → ( ( ⟨ 0 , ( ( 𝑌 − 1 ) mod 𝑁 ) ⟩ = ⟨ 0 , ( ( 𝑋 + 1 ) mod 𝑁 ) ⟩ ∨ ⟨ 0 , ( ( 𝑌 − 1 ) mod 𝑁 ) ⟩ = ⟨ 1 , 𝑋 ⟩ ∨ ⟨ 0 , ( ( 𝑌 − 1 ) mod 𝑁 ) ⟩ = ⟨ 0 , ( ( 𝑋 − 1 ) mod 𝑁 ) ⟩ ) → 𝑋 = 𝑌 ) ) )
81 11 31 opth ⊢ ( ⟨ 0 , ( ( 𝑌 + 1 ) mod 𝑁 ) ⟩ = ⟨ 0 , ( ( 𝑋 − 1 ) mod 𝑁 ) ⟩ ↔ ( 0 = 0 ∧ ( ( 𝑌 + 1 ) mod 𝑁 ) = ( ( 𝑋 − 1 ) mod 𝑁 ) ) )
82 11 59 opth ⊢ ( ⟨ 0 , ( ( 𝑌 − 1 ) mod 𝑁 ) ⟩ = ⟨ 0 , ( ( 𝑋 + 1 ) mod 𝑁 ) ⟩ ↔ ( 0 = 0 ∧ ( ( 𝑌 − 1 ) mod 𝑁 ) = ( ( 𝑋 + 1 ) mod 𝑁 ) ) )
83 simpll ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 5 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝐼 ) ) → 𝑁 ∈ ( ℤ≥ ‘ 5 ) )
84 simprl ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 5 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝐼 ) ) → 𝑋 ∈ 𝐼 )
85 simprr ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 5 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝐼 ) ) → 𝑌 ∈ 𝐼 )
86 2 modm1p1ne ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 5 ) ∧ 𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝐼 ) → ( ( ( 𝑌 − 1 ) mod 𝑁 ) = ( ( 𝑋 + 1 ) mod 𝑁 ) → ( ( 𝑌 + 1 ) mod 𝑁 ) ≠ ( ( 𝑋 − 1 ) mod 𝑁 ) ) )
87 83 84 85 86 syl3anc ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 5 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝐼 ) ) → ( ( ( 𝑌 − 1 ) mod 𝑁 ) = ( ( 𝑋 + 1 ) mod 𝑁 ) → ( ( 𝑌 + 1 ) mod 𝑁 ) ≠ ( ( 𝑋 − 1 ) mod 𝑁 ) ) )
88 eqneqall ⊢ ( ( ( 𝑌 + 1 ) mod 𝑁 ) = ( ( 𝑋 − 1 ) mod 𝑁 ) → ( ( ( 𝑌 + 1 ) mod 𝑁 ) ≠ ( ( 𝑋 − 1 ) mod 𝑁 ) → 𝑋 = 𝑌 ) )
89 88 com12 ⊢ ( ( ( 𝑌 + 1 ) mod 𝑁 ) ≠ ( ( 𝑋 − 1 ) mod 𝑁 ) → ( ( ( 𝑌 + 1 ) mod 𝑁 ) = ( ( 𝑋 − 1 ) mod 𝑁 ) → 𝑋 = 𝑌 ) )
90 89 a1i ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 5 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝐼 ) ) → ( ( ( 𝑌 + 1 ) mod 𝑁 ) ≠ ( ( 𝑋 − 1 ) mod 𝑁 ) → ( ( ( 𝑌 + 1 ) mod 𝑁 ) = ( ( 𝑋 − 1 ) mod 𝑁 ) → 𝑋 = 𝑌 ) ) )
91 87 90 syld ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 5 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝐼 ) ) → ( ( ( 𝑌 − 1 ) mod 𝑁 ) = ( ( 𝑋 + 1 ) mod 𝑁 ) → ( ( ( 𝑌 + 1 ) mod 𝑁 ) = ( ( 𝑋 − 1 ) mod 𝑁 ) → 𝑋 = 𝑌 ) ) )
92 91 adantld ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 5 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝐼 ) ) → ( ( 0 = 0 ∧ ( ( 𝑌 − 1 ) mod 𝑁 ) = ( ( 𝑋 + 1 ) mod 𝑁 ) ) → ( ( ( 𝑌 + 1 ) mod 𝑁 ) = ( ( 𝑋 − 1 ) mod 𝑁 ) → 𝑋 = 𝑌 ) ) )
93 82 92 biimtrid ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 5 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝐼 ) ) → ( ⟨ 0 , ( ( 𝑌 − 1 ) mod 𝑁 ) ⟩ = ⟨ 0 , ( ( 𝑋 + 1 ) mod 𝑁 ) ⟩ → ( ( ( 𝑌 + 1 ) mod 𝑁 ) = ( ( 𝑋 − 1 ) mod 𝑁 ) → 𝑋 = 𝑌 ) ) )
94 93 com23 ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 5 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝐼 ) ) → ( ( ( 𝑌 + 1 ) mod 𝑁 ) = ( ( 𝑋 − 1 ) mod 𝑁 ) → ( ⟨ 0 , ( ( 𝑌 − 1 ) mod 𝑁 ) ⟩ = ⟨ 0 , ( ( 𝑋 + 1 ) mod 𝑁 ) ⟩ → 𝑋 = 𝑌 ) ) )
95 94 adantld ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 5 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝐼 ) ) → ( ( 0 = 0 ∧ ( ( 𝑌 + 1 ) mod 𝑁 ) = ( ( 𝑋 − 1 ) mod 𝑁 ) ) → ( ⟨ 0 , ( ( 𝑌 − 1 ) mod 𝑁 ) ⟩ = ⟨ 0 , ( ( 𝑋 + 1 ) mod 𝑁 ) ⟩ → 𝑋 = 𝑌 ) ) )
96 81 95 biimtrid ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 5 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝐼 ) ) → ( ⟨ 0 , ( ( 𝑌 + 1 ) mod 𝑁 ) ⟩ = ⟨ 0 , ( ( 𝑋 − 1 ) mod 𝑁 ) ⟩ → ( ⟨ 0 , ( ( 𝑌 − 1 ) mod 𝑁 ) ⟩ = ⟨ 0 , ( ( 𝑋 + 1 ) mod 𝑁 ) ⟩ → 𝑋 = 𝑌 ) ) )
97 96 imp ⊢ ( ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 5 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝐼 ) ) ∧ ⟨ 0 , ( ( 𝑌 + 1 ) mod 𝑁 ) ⟩ = ⟨ 0 , ( ( 𝑋 − 1 ) mod 𝑁 ) ⟩ ) → ( ⟨ 0 , ( ( 𝑌 − 1 ) mod 𝑁 ) ⟩ = ⟨ 0 , ( ( 𝑋 + 1 ) mod 𝑁 ) ⟩ → 𝑋 = 𝑌 ) )
98 49 orci ⊢ ( 0 ≠ 1 ∨ ( ( 𝑌 − 1 ) mod 𝑁 ) ≠ 𝑋 )
99 11 59 opthne ⊢ ( ⟨ 0 , ( ( 𝑌 − 1 ) mod 𝑁 ) ⟩ ≠ ⟨ 1 , 𝑋 ⟩ ↔ ( 0 ≠ 1 ∨ ( ( 𝑌 − 1 ) mod 𝑁 ) ≠ 𝑋 ) )
100 98 99 mpbir ⊢ ⟨ 0 , ( ( 𝑌 − 1 ) mod 𝑁 ) ⟩ ≠ ⟨ 1 , 𝑋 ⟩
101 eqneqall ⊢ ( ⟨ 0 , ( ( 𝑌 − 1 ) mod 𝑁 ) ⟩ = ⟨ 1 , 𝑋 ⟩ → ( ⟨ 0 , ( ( 𝑌 − 1 ) mod 𝑁 ) ⟩ ≠ ⟨ 1 , 𝑋 ⟩ → 𝑋 = 𝑌 ) )
102 100 101 mpi ⊢ ( ⟨ 0 , ( ( 𝑌 − 1 ) mod 𝑁 ) ⟩ = ⟨ 1 , 𝑋 ⟩ → 𝑋 = 𝑌 )
103 102 a1i ⊢ ( ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 5 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝐼 ) ) ∧ ⟨ 0 , ( ( 𝑌 + 1 ) mod 𝑁 ) ⟩ = ⟨ 0 , ( ( 𝑋 − 1 ) mod 𝑁 ) ⟩ ) → ( ⟨ 0 , ( ( 𝑌 − 1 ) mod 𝑁 ) ⟩ = ⟨ 1 , 𝑋 ⟩ → 𝑋 = 𝑌 ) )
104 eqeq2 ⊢ ( ⟨ 0 , ( ( 𝑋 − 1 ) mod 𝑁 ) ⟩ = ⟨ 0 , ( ( 𝑌 + 1 ) mod 𝑁 ) ⟩ → ( ⟨ 0 , ( ( 𝑌 − 1 ) mod 𝑁 ) ⟩ = ⟨ 0 , ( ( 𝑋 − 1 ) mod 𝑁 ) ⟩ ↔ ⟨ 0 , ( ( 𝑌 − 1 ) mod 𝑁 ) ⟩ = ⟨ 0 , ( ( 𝑌 + 1 ) mod 𝑁 ) ⟩ ) )
105 104 eqcoms ⊢ ( ⟨ 0 , ( ( 𝑌 + 1 ) mod 𝑁 ) ⟩ = ⟨ 0 , ( ( 𝑋 − 1 ) mod 𝑁 ) ⟩ → ( ⟨ 0 , ( ( 𝑌 − 1 ) mod 𝑁 ) ⟩ = ⟨ 0 , ( ( 𝑋 − 1 ) mod 𝑁 ) ⟩ ↔ ⟨ 0 , ( ( 𝑌 − 1 ) mod 𝑁 ) ⟩ = ⟨ 0 , ( ( 𝑌 + 1 ) mod 𝑁 ) ⟩ ) )
106 105 adantl ⊢ ( ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 5 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝐼 ) ) ∧ ⟨ 0 , ( ( 𝑌 + 1 ) mod 𝑁 ) ⟩ = ⟨ 0 , ( ( 𝑋 − 1 ) mod 𝑁 ) ⟩ ) → ( ⟨ 0 , ( ( 𝑌 − 1 ) mod 𝑁 ) ⟩ = ⟨ 0 , ( ( 𝑋 − 1 ) mod 𝑁 ) ⟩ ↔ ⟨ 0 , ( ( 𝑌 − 1 ) mod 𝑁 ) ⟩ = ⟨ 0 , ( ( 𝑌 + 1 ) mod 𝑁 ) ⟩ ) )
107 68 adantr ⊢ ( ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 5 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝐼 ) ) ∧ ⟨ 0 , ( ( 𝑌 + 1 ) mod 𝑁 ) ⟩ = ⟨ 0 , ( ( 𝑋 − 1 ) mod 𝑁 ) ⟩ ) → ( ⟨ 0 , ( ( 𝑌 − 1 ) mod 𝑁 ) ⟩ = ⟨ 0 , ( ( 𝑌 + 1 ) mod 𝑁 ) ⟩ → 𝑋 = 𝑌 ) )
108 106 107 sylbid ⊢ ( ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 5 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝐼 ) ) ∧ ⟨ 0 , ( ( 𝑌 + 1 ) mod 𝑁 ) ⟩ = ⟨ 0 , ( ( 𝑋 − 1 ) mod 𝑁 ) ⟩ ) → ( ⟨ 0 , ( ( 𝑌 − 1 ) mod 𝑁 ) ⟩ = ⟨ 0 , ( ( 𝑋 − 1 ) mod 𝑁 ) ⟩ → 𝑋 = 𝑌 ) )
109 97 103 108 3jaod ⊢ ( ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 5 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝐼 ) ) ∧ ⟨ 0 , ( ( 𝑌 + 1 ) mod 𝑁 ) ⟩ = ⟨ 0 , ( ( 𝑋 − 1 ) mod 𝑁 ) ⟩ ) → ( ( ⟨ 0 , ( ( 𝑌 − 1 ) mod 𝑁 ) ⟩ = ⟨ 0 , ( ( 𝑋 + 1 ) mod 𝑁 ) ⟩ ∨ ⟨ 0 , ( ( 𝑌 − 1 ) mod 𝑁 ) ⟩ = ⟨ 1 , 𝑋 ⟩ ∨ ⟨ 0 , ( ( 𝑌 − 1 ) mod 𝑁 ) ⟩ = ⟨ 0 , ( ( 𝑋 − 1 ) mod 𝑁 ) ⟩ ) → 𝑋 = 𝑌 ) )
110 109 ex ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 5 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝐼 ) ) → ( ⟨ 0 , ( ( 𝑌 + 1 ) mod 𝑁 ) ⟩ = ⟨ 0 , ( ( 𝑋 − 1 ) mod 𝑁 ) ⟩ → ( ( ⟨ 0 , ( ( 𝑌 − 1 ) mod 𝑁 ) ⟩ = ⟨ 0 , ( ( 𝑋 + 1 ) mod 𝑁 ) ⟩ ∨ ⟨ 0 , ( ( 𝑌 − 1 ) mod 𝑁 ) ⟩ = ⟨ 1 , 𝑋 ⟩ ∨ ⟨ 0 , ( ( 𝑌 − 1 ) mod 𝑁 ) ⟩ = ⟨ 0 , ( ( 𝑋 − 1 ) mod 𝑁 ) ⟩ ) → 𝑋 = 𝑌 ) ) )
111 47 80 110 3jaod ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 5 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝐼 ) ) → ( ( ⟨ 0 , ( ( 𝑌 + 1 ) mod 𝑁 ) ⟩ = ⟨ 0 , ( ( 𝑋 + 1 ) mod 𝑁 ) ⟩ ∨ ⟨ 0 , ( ( 𝑌 + 1 ) mod 𝑁 ) ⟩ = ⟨ 1 , 𝑋 ⟩ ∨ ⟨ 0 , ( ( 𝑌 + 1 ) mod 𝑁 ) ⟩ = ⟨ 0 , ( ( 𝑋 − 1 ) mod 𝑁 ) ⟩ ) → ( ( ⟨ 0 , ( ( 𝑌 − 1 ) mod 𝑁 ) ⟩ = ⟨ 0 , ( ( 𝑋 + 1 ) mod 𝑁 ) ⟩ ∨ ⟨ 0 , ( ( 𝑌 − 1 ) mod 𝑁 ) ⟩ = ⟨ 1 , 𝑋 ⟩ ∨ ⟨ 0 , ( ( 𝑌 − 1 ) mod 𝑁 ) ⟩ = ⟨ 0 , ( ( 𝑋 − 1 ) mod 𝑁 ) ⟩ ) → 𝑋 = 𝑌 ) ) )
112 op2ndg ⊢ ( ( 0 ∈ V ∧ 𝑋 ∈ 𝐼 ) → ( 2nd ‘ ⟨ 0 , 𝑋 ⟩ ) = 𝑋 )
113 11 112 mpan ⊢ ( 𝑋 ∈ 𝐼 → ( 2nd ‘ ⟨ 0 , 𝑋 ⟩ ) = 𝑋 )
114 113 adantr ⊢ ( ( 𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝐼 ) → ( 2nd ‘ ⟨ 0 , 𝑋 ⟩ ) = 𝑋 )
115 114 adantl ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 5 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝐼 ) ) → ( 2nd ‘ ⟨ 0 , 𝑋 ⟩ ) = 𝑋 )
116 oveq1 ⊢ ( ( 2nd ‘ ⟨ 0 , 𝑋 ⟩ ) = 𝑋 → ( ( 2nd ‘ ⟨ 0 , 𝑋 ⟩ ) + 1 ) = ( 𝑋 + 1 ) )
117 116 oveq1d ⊢ ( ( 2nd ‘ ⟨ 0 , 𝑋 ⟩ ) = 𝑋 → ( ( ( 2nd ‘ ⟨ 0 , 𝑋 ⟩ ) + 1 ) mod 𝑁 ) = ( ( 𝑋 + 1 ) mod 𝑁 ) )
118 117 opeq2d ⊢ ( ( 2nd ‘ ⟨ 0 , 𝑋 ⟩ ) = 𝑋 → ⟨ 0 , ( ( ( 2nd ‘ ⟨ 0 , 𝑋 ⟩ ) + 1 ) mod 𝑁 ) ⟩ = ⟨ 0 , ( ( 𝑋 + 1 ) mod 𝑁 ) ⟩ )
119 118 eqeq2d ⊢ ( ( 2nd ‘ ⟨ 0 , 𝑋 ⟩ ) = 𝑋 → ( ⟨ 0 , ( ( 𝑌 + 1 ) mod 𝑁 ) ⟩ = ⟨ 0 , ( ( ( 2nd ‘ ⟨ 0 , 𝑋 ⟩ ) + 1 ) mod 𝑁 ) ⟩ ↔ ⟨ 0 , ( ( 𝑌 + 1 ) mod 𝑁 ) ⟩ = ⟨ 0 , ( ( 𝑋 + 1 ) mod 𝑁 ) ⟩ ) )
120 opeq2 ⊢ ( ( 2nd ‘ ⟨ 0 , 𝑋 ⟩ ) = 𝑋 → ⟨ 1 , ( 2nd ‘ ⟨ 0 , 𝑋 ⟩ ) ⟩ = ⟨ 1 , 𝑋 ⟩ )
121 120 eqeq2d ⊢ ( ( 2nd ‘ ⟨ 0 , 𝑋 ⟩ ) = 𝑋 → ( ⟨ 0 , ( ( 𝑌 + 1 ) mod 𝑁 ) ⟩ = ⟨ 1 , ( 2nd ‘ ⟨ 0 , 𝑋 ⟩ ) ⟩ ↔ ⟨ 0 , ( ( 𝑌 + 1 ) mod 𝑁 ) ⟩ = ⟨ 1 , 𝑋 ⟩ ) )
122 oveq1 ⊢ ( ( 2nd ‘ ⟨ 0 , 𝑋 ⟩ ) = 𝑋 → ( ( 2nd ‘ ⟨ 0 , 𝑋 ⟩ ) − 1 ) = ( 𝑋 − 1 ) )
123 122 oveq1d ⊢ ( ( 2nd ‘ ⟨ 0 , 𝑋 ⟩ ) = 𝑋 → ( ( ( 2nd ‘ ⟨ 0 , 𝑋 ⟩ ) − 1 ) mod 𝑁 ) = ( ( 𝑋 − 1 ) mod 𝑁 ) )
124 123 opeq2d ⊢ ( ( 2nd ‘ ⟨ 0 , 𝑋 ⟩ ) = 𝑋 → ⟨ 0 , ( ( ( 2nd ‘ ⟨ 0 , 𝑋 ⟩ ) − 1 ) mod 𝑁 ) ⟩ = ⟨ 0 , ( ( 𝑋 − 1 ) mod 𝑁 ) ⟩ )
125 124 eqeq2d ⊢ ( ( 2nd ‘ ⟨ 0 , 𝑋 ⟩ ) = 𝑋 → ( ⟨ 0 , ( ( 𝑌 + 1 ) mod 𝑁 ) ⟩ = ⟨ 0 , ( ( ( 2nd ‘ ⟨ 0 , 𝑋 ⟩ ) − 1 ) mod 𝑁 ) ⟩ ↔ ⟨ 0 , ( ( 𝑌 + 1 ) mod 𝑁 ) ⟩ = ⟨ 0 , ( ( 𝑋 − 1 ) mod 𝑁 ) ⟩ ) )
126 119 121 125 3orbi123d ⊢ ( ( 2nd ‘ ⟨ 0 , 𝑋 ⟩ ) = 𝑋 → ( ( ⟨ 0 , ( ( 𝑌 + 1 ) mod 𝑁 ) ⟩ = ⟨ 0 , ( ( ( 2nd ‘ ⟨ 0 , 𝑋 ⟩ ) + 1 ) mod 𝑁 ) ⟩ ∨ ⟨ 0 , ( ( 𝑌 + 1 ) mod 𝑁 ) ⟩ = ⟨ 1 , ( 2nd ‘ ⟨ 0 , 𝑋 ⟩ ) ⟩ ∨ ⟨ 0 , ( ( 𝑌 + 1 ) mod 𝑁 ) ⟩ = ⟨ 0 , ( ( ( 2nd ‘ ⟨ 0 , 𝑋 ⟩ ) − 1 ) mod 𝑁 ) ⟩ ) ↔ ( ⟨ 0 , ( ( 𝑌 + 1 ) mod 𝑁 ) ⟩ = ⟨ 0 , ( ( 𝑋 + 1 ) mod 𝑁 ) ⟩ ∨ ⟨ 0 , ( ( 𝑌 + 1 ) mod 𝑁 ) ⟩ = ⟨ 1 , 𝑋 ⟩ ∨ ⟨ 0 , ( ( 𝑌 + 1 ) mod 𝑁 ) ⟩ = ⟨ 0 , ( ( 𝑋 − 1 ) mod 𝑁 ) ⟩ ) ) )
127 118 eqeq2d ⊢ ( ( 2nd ‘ ⟨ 0 , 𝑋 ⟩ ) = 𝑋 → ( ⟨ 0 , ( ( 𝑌 − 1 ) mod 𝑁 ) ⟩ = ⟨ 0 , ( ( ( 2nd ‘ ⟨ 0 , 𝑋 ⟩ ) + 1 ) mod 𝑁 ) ⟩ ↔ ⟨ 0 , ( ( 𝑌 − 1 ) mod 𝑁 ) ⟩ = ⟨ 0 , ( ( 𝑋 + 1 ) mod 𝑁 ) ⟩ ) )
128 120 eqeq2d ⊢ ( ( 2nd ‘ ⟨ 0 , 𝑋 ⟩ ) = 𝑋 → ( ⟨ 0 , ( ( 𝑌 − 1 ) mod 𝑁 ) ⟩ = ⟨ 1 , ( 2nd ‘ ⟨ 0 , 𝑋 ⟩ ) ⟩ ↔ ⟨ 0 , ( ( 𝑌 − 1 ) mod 𝑁 ) ⟩ = ⟨ 1 , 𝑋 ⟩ ) )
129 124 eqeq2d ⊢ ( ( 2nd ‘ ⟨ 0 , 𝑋 ⟩ ) = 𝑋 → ( ⟨ 0 , ( ( 𝑌 − 1 ) mod 𝑁 ) ⟩ = ⟨ 0 , ( ( ( 2nd ‘ ⟨ 0 , 𝑋 ⟩ ) − 1 ) mod 𝑁 ) ⟩ ↔ ⟨ 0 , ( ( 𝑌 − 1 ) mod 𝑁 ) ⟩ = ⟨ 0 , ( ( 𝑋 − 1 ) mod 𝑁 ) ⟩ ) )
130 127 128 129 3orbi123d ⊢ ( ( 2nd ‘ ⟨ 0 , 𝑋 ⟩ ) = 𝑋 → ( ( ⟨ 0 , ( ( 𝑌 − 1 ) mod 𝑁 ) ⟩ = ⟨ 0 , ( ( ( 2nd ‘ ⟨ 0 , 𝑋 ⟩ ) + 1 ) mod 𝑁 ) ⟩ ∨ ⟨ 0 , ( ( 𝑌 − 1 ) mod 𝑁 ) ⟩ = ⟨ 1 , ( 2nd ‘ ⟨ 0 , 𝑋 ⟩ ) ⟩ ∨ ⟨ 0 , ( ( 𝑌 − 1 ) mod 𝑁 ) ⟩ = ⟨ 0 , ( ( ( 2nd ‘ ⟨ 0 , 𝑋 ⟩ ) − 1 ) mod 𝑁 ) ⟩ ) ↔ ( ⟨ 0 , ( ( 𝑌 − 1 ) mod 𝑁 ) ⟩ = ⟨ 0 , ( ( 𝑋 + 1 ) mod 𝑁 ) ⟩ ∨ ⟨ 0 , ( ( 𝑌 − 1 ) mod 𝑁 ) ⟩ = ⟨ 1 , 𝑋 ⟩ ∨ ⟨ 0 , ( ( 𝑌 − 1 ) mod 𝑁 ) ⟩ = ⟨ 0 , ( ( 𝑋 − 1 ) mod 𝑁 ) ⟩ ) ) )
131 130 imbi1d ⊢ ( ( 2nd ‘ ⟨ 0 , 𝑋 ⟩ ) = 𝑋 → ( ( ( ⟨ 0 , ( ( 𝑌 − 1 ) mod 𝑁 ) ⟩ = ⟨ 0 , ( ( ( 2nd ‘ ⟨ 0 , 𝑋 ⟩ ) + 1 ) mod 𝑁 ) ⟩ ∨ ⟨ 0 , ( ( 𝑌 − 1 ) mod 𝑁 ) ⟩ = ⟨ 1 , ( 2nd ‘ ⟨ 0 , 𝑋 ⟩ ) ⟩ ∨ ⟨ 0 , ( ( 𝑌 − 1 ) mod 𝑁 ) ⟩ = ⟨ 0 , ( ( ( 2nd ‘ ⟨ 0 , 𝑋 ⟩ ) − 1 ) mod 𝑁 ) ⟩ ) → 𝑋 = 𝑌 ) ↔ ( ( ⟨ 0 , ( ( 𝑌 − 1 ) mod 𝑁 ) ⟩ = ⟨ 0 , ( ( 𝑋 + 1 ) mod 𝑁 ) ⟩ ∨ ⟨ 0 , ( ( 𝑌 − 1 ) mod 𝑁 ) ⟩ = ⟨ 1 , 𝑋 ⟩ ∨ ⟨ 0 , ( ( 𝑌 − 1 ) mod 𝑁 ) ⟩ = ⟨ 0 , ( ( 𝑋 − 1 ) mod 𝑁 ) ⟩ ) → 𝑋 = 𝑌 ) ) )
132 126 131 imbi12d ⊢ ( ( 2nd ‘ ⟨ 0 , 𝑋 ⟩ ) = 𝑋 → ( ( ( ⟨ 0 , ( ( 𝑌 + 1 ) mod 𝑁 ) ⟩ = ⟨ 0 , ( ( ( 2nd ‘ ⟨ 0 , 𝑋 ⟩ ) + 1 ) mod 𝑁 ) ⟩ ∨ ⟨ 0 , ( ( 𝑌 + 1 ) mod 𝑁 ) ⟩ = ⟨ 1 , ( 2nd ‘ ⟨ 0 , 𝑋 ⟩ ) ⟩ ∨ ⟨ 0 , ( ( 𝑌 + 1 ) mod 𝑁 ) ⟩ = ⟨ 0 , ( ( ( 2nd ‘ ⟨ 0 , 𝑋 ⟩ ) − 1 ) mod 𝑁 ) ⟩ ) → ( ( ⟨ 0 , ( ( 𝑌 − 1 ) mod 𝑁 ) ⟩ = ⟨ 0 , ( ( ( 2nd ‘ ⟨ 0 , 𝑋 ⟩ ) + 1 ) mod 𝑁 ) ⟩ ∨ ⟨ 0 , ( ( 𝑌 − 1 ) mod 𝑁 ) ⟩ = ⟨ 1 , ( 2nd ‘ ⟨ 0 , 𝑋 ⟩ ) ⟩ ∨ ⟨ 0 , ( ( 𝑌 − 1 ) mod 𝑁 ) ⟩ = ⟨ 0 , ( ( ( 2nd ‘ ⟨ 0 , 𝑋 ⟩ ) − 1 ) mod 𝑁 ) ⟩ ) → 𝑋 = 𝑌 ) ) ↔ ( ( ⟨ 0 , ( ( 𝑌 + 1 ) mod 𝑁 ) ⟩ = ⟨ 0 , ( ( 𝑋 + 1 ) mod 𝑁 ) ⟩ ∨ ⟨ 0 , ( ( 𝑌 + 1 ) mod 𝑁 ) ⟩ = ⟨ 1 , 𝑋 ⟩ ∨ ⟨ 0 , ( ( 𝑌 + 1 ) mod 𝑁 ) ⟩ = ⟨ 0 , ( ( 𝑋 − 1 ) mod 𝑁 ) ⟩ ) → ( ( ⟨ 0 , ( ( 𝑌 − 1 ) mod 𝑁 ) ⟩ = ⟨ 0 , ( ( 𝑋 + 1 ) mod 𝑁 ) ⟩ ∨ ⟨ 0 , ( ( 𝑌 − 1 ) mod 𝑁 ) ⟩ = ⟨ 1 , 𝑋 ⟩ ∨ ⟨ 0 , ( ( 𝑌 − 1 ) mod 𝑁 ) ⟩ = ⟨ 0 , ( ( 𝑋 − 1 ) mod 𝑁 ) ⟩ ) → 𝑋 = 𝑌 ) ) ) )
133 115 132 syl ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 5 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝐼 ) ) → ( ( ( ⟨ 0 , ( ( 𝑌 + 1 ) mod 𝑁 ) ⟩ = ⟨ 0 , ( ( ( 2nd ‘ ⟨ 0 , 𝑋 ⟩ ) + 1 ) mod 𝑁 ) ⟩ ∨ ⟨ 0 , ( ( 𝑌 + 1 ) mod 𝑁 ) ⟩ = ⟨ 1 , ( 2nd ‘ ⟨ 0 , 𝑋 ⟩ ) ⟩ ∨ ⟨ 0 , ( ( 𝑌 + 1 ) mod 𝑁 ) ⟩ = ⟨ 0 , ( ( ( 2nd ‘ ⟨ 0 , 𝑋 ⟩ ) − 1 ) mod 𝑁 ) ⟩ ) → ( ( ⟨ 0 , ( ( 𝑌 − 1 ) mod 𝑁 ) ⟩ = ⟨ 0 , ( ( ( 2nd ‘ ⟨ 0 , 𝑋 ⟩ ) + 1 ) mod 𝑁 ) ⟩ ∨ ⟨ 0 , ( ( 𝑌 − 1 ) mod 𝑁 ) ⟩ = ⟨ 1 , ( 2nd ‘ ⟨ 0 , 𝑋 ⟩ ) ⟩ ∨ ⟨ 0 , ( ( 𝑌 − 1 ) mod 𝑁 ) ⟩ = ⟨ 0 , ( ( ( 2nd ‘ ⟨ 0 , 𝑋 ⟩ ) − 1 ) mod 𝑁 ) ⟩ ) → 𝑋 = 𝑌 ) ) ↔ ( ( ⟨ 0 , ( ( 𝑌 + 1 ) mod 𝑁 ) ⟩ = ⟨ 0 , ( ( 𝑋 + 1 ) mod 𝑁 ) ⟩ ∨ ⟨ 0 , ( ( 𝑌 + 1 ) mod 𝑁 ) ⟩ = ⟨ 1 , 𝑋 ⟩ ∨ ⟨ 0 , ( ( 𝑌 + 1 ) mod 𝑁 ) ⟩ = ⟨ 0 , ( ( 𝑋 − 1 ) mod 𝑁 ) ⟩ ) → ( ( ⟨ 0 , ( ( 𝑌 − 1 ) mod 𝑁 ) ⟩ = ⟨ 0 , ( ( 𝑋 + 1 ) mod 𝑁 ) ⟩ ∨ ⟨ 0 , ( ( 𝑌 − 1 ) mod 𝑁 ) ⟩ = ⟨ 1 , 𝑋 ⟩ ∨ ⟨ 0 , ( ( 𝑌 − 1 ) mod 𝑁 ) ⟩ = ⟨ 0 , ( ( 𝑋 − 1 ) mod 𝑁 ) ⟩ ) → 𝑋 = 𝑌 ) ) ) )
134 111 133 mpbird ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 5 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝐼 ) ) → ( ( ⟨ 0 , ( ( 𝑌 + 1 ) mod 𝑁 ) ⟩ = ⟨ 0 , ( ( ( 2nd ‘ ⟨ 0 , 𝑋 ⟩ ) + 1 ) mod 𝑁 ) ⟩ ∨ ⟨ 0 , ( ( 𝑌 + 1 ) mod 𝑁 ) ⟩ = ⟨ 1 , ( 2nd ‘ ⟨ 0 , 𝑋 ⟩ ) ⟩ ∨ ⟨ 0 , ( ( 𝑌 + 1 ) mod 𝑁 ) ⟩ = ⟨ 0 , ( ( ( 2nd ‘ ⟨ 0 , 𝑋 ⟩ ) − 1 ) mod 𝑁 ) ⟩ ) → ( ( ⟨ 0 , ( ( 𝑌 − 1 ) mod 𝑁 ) ⟩ = ⟨ 0 , ( ( ( 2nd ‘ ⟨ 0 , 𝑋 ⟩ ) + 1 ) mod 𝑁 ) ⟩ ∨ ⟨ 0 , ( ( 𝑌 − 1 ) mod 𝑁 ) ⟩ = ⟨ 1 , ( 2nd ‘ ⟨ 0 , 𝑋 ⟩ ) ⟩ ∨ ⟨ 0 , ( ( 𝑌 − 1 ) mod 𝑁 ) ⟩ = ⟨ 0 , ( ( ( 2nd ‘ ⟨ 0 , 𝑋 ⟩ ) − 1 ) mod 𝑁 ) ⟩ ) → 𝑋 = 𝑌 ) ) )
135 30 134 syld ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 5 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝐼 ) ) → ( { ⟨ 0 , 𝑋 ⟩ , ⟨ 0 , ( ( 𝑌 + 1 ) mod 𝑁 ) ⟩ } ∈ 𝐸 → ( ( ⟨ 0 , ( ( 𝑌 − 1 ) mod 𝑁 ) ⟩ = ⟨ 0 , ( ( ( 2nd ‘ ⟨ 0 , 𝑋 ⟩ ) + 1 ) mod 𝑁 ) ⟩ ∨ ⟨ 0 , ( ( 𝑌 − 1 ) mod 𝑁 ) ⟩ = ⟨ 1 , ( 2nd ‘ ⟨ 0 , 𝑋 ⟩ ) ⟩ ∨ ⟨ 0 , ( ( 𝑌 − 1 ) mod 𝑁 ) ⟩ = ⟨ 0 , ( ( ( 2nd ‘ ⟨ 0 , 𝑋 ⟩ ) − 1 ) mod 𝑁 ) ⟩ ) → 𝑋 = 𝑌 ) ) )
136 135 com23 ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 5 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝐼 ) ) → ( ( ⟨ 0 , ( ( 𝑌 − 1 ) mod 𝑁 ) ⟩ = ⟨ 0 , ( ( ( 2nd ‘ ⟨ 0 , 𝑋 ⟩ ) + 1 ) mod 𝑁 ) ⟩ ∨ ⟨ 0 , ( ( 𝑌 − 1 ) mod 𝑁 ) ⟩ = ⟨ 1 , ( 2nd ‘ ⟨ 0 , 𝑋 ⟩ ) ⟩ ∨ ⟨ 0 , ( ( 𝑌 − 1 ) mod 𝑁 ) ⟩ = ⟨ 0 , ( ( ( 2nd ‘ ⟨ 0 , 𝑋 ⟩ ) − 1 ) mod 𝑁 ) ⟩ ) → ( { ⟨ 0 , 𝑋 ⟩ , ⟨ 0 , ( ( 𝑌 + 1 ) mod 𝑁 ) ⟩ } ∈ 𝐸 → 𝑋 = 𝑌 ) ) )
137 24 136 syld ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 5 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝐼 ) ) → ( { ⟨ 0 , ( ( 𝑌 − 1 ) mod 𝑁 ) ⟩ , ⟨ 0 , 𝑋 ⟩ } ∈ 𝐸 → ( { ⟨ 0 , 𝑋 ⟩ , ⟨ 0 , ( ( 𝑌 + 1 ) mod 𝑁 ) ⟩ } ∈ 𝐸 → 𝑋 = 𝑌 ) ) )
138 137 impd ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 5 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝐼 ) ) → ( ( { ⟨ 0 , ( ( 𝑌 − 1 ) mod 𝑁 ) ⟩ , ⟨ 0 , 𝑋 ⟩ } ∈ 𝐸 ∧ { ⟨ 0 , 𝑋 ⟩ , ⟨ 0 , ( ( 𝑌 + 1 ) mod 𝑁 ) ⟩ } ∈ 𝐸 ) → 𝑋 = 𝑌 ) )
139 eqid ⊢ 0 = 0
140 139 orci ⊢ ( 0 = 0 ∨ 0 = 1 )
141 61 140 jctil ⊢ ( ( 𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝐼 ) → ( ( 0 = 0 ∨ 0 = 1 ) ∧ 𝑌 ∈ 𝐼 ) )
142 141 adantl ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 5 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝐼 ) ) → ( ( 0 = 0 ∨ 0 = 1 ) ∧ 𝑌 ∈ 𝐼 ) )
143 2 1 3 20 opgpgvtx ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) → ( ⟨ 0 , 𝑌 ⟩ ∈ ( Vtx ‘ 𝐺 ) ↔ ( ( 0 = 0 ∨ 0 = 1 ) ∧ 𝑌 ∈ 𝐼 ) ) )
144 8 143 syl ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 5 ) ∧ 𝐾 ∈ 𝐽 ) → ( ⟨ 0 , 𝑌 ⟩ ∈ ( Vtx ‘ 𝐺 ) ↔ ( ( 0 = 0 ∨ 0 = 1 ) ∧ 𝑌 ∈ 𝐼 ) ) )
145 144 adantr ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 5 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝐼 ) ) → ( ⟨ 0 , 𝑌 ⟩ ∈ ( Vtx ‘ 𝐺 ) ↔ ( ( 0 = 0 ∨ 0 = 1 ) ∧ 𝑌 ∈ 𝐼 ) ) )
146 142 145 mpbird ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 5 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝐼 ) ) → ⟨ 0 , 𝑌 ⟩ ∈ ( Vtx ‘ 𝐺 ) )
147 11 a1i ⊢ ( 𝑋 ∈ 𝐼 → 0 ∈ V )
148 op1stg ⊢ ( ( 0 ∈ V ∧ 𝑌 ∈ 𝐼 ) → ( 1st ‘ ⟨ 0 , 𝑌 ⟩ ) = 0 )
149 147 148 sylan ⊢ ( ( 𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝐼 ) → ( 1st ‘ ⟨ 0 , 𝑌 ⟩ ) = 0 )
150 149 adantl ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 5 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝐼 ) ) → ( 1st ‘ ⟨ 0 , 𝑌 ⟩ ) = 0 )
151 1 3 20 4 gpgedgvtx0 ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( ⟨ 0 , 𝑌 ⟩ ∈ ( Vtx ‘ 𝐺 ) ∧ ( 1st ‘ ⟨ 0 , 𝑌 ⟩ ) = 0 ) ) → ( { ⟨ 0 , 𝑌 ⟩ , ⟨ 0 , ( ( ( 2nd ‘ ⟨ 0 , 𝑌 ⟩ ) + 1 ) mod 𝑁 ) ⟩ } ∈ 𝐸 ∧ { ⟨ 0 , 𝑌 ⟩ , ⟨ 1 , ( 2nd ‘ ⟨ 0 , 𝑌 ⟩ ) ⟩ } ∈ 𝐸 ∧ { ⟨ 0 , 𝑌 ⟩ , ⟨ 0 , ( ( ( 2nd ‘ ⟨ 0 , 𝑌 ⟩ ) − 1 ) mod 𝑁 ) ⟩ } ∈ 𝐸 ) )
152 9 146 150 151 syl12anc ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 5 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝐼 ) ) → ( { ⟨ 0 , 𝑌 ⟩ , ⟨ 0 , ( ( ( 2nd ‘ ⟨ 0 , 𝑌 ⟩ ) + 1 ) mod 𝑁 ) ⟩ } ∈ 𝐸 ∧ { ⟨ 0 , 𝑌 ⟩ , ⟨ 1 , ( 2nd ‘ ⟨ 0 , 𝑌 ⟩ ) ⟩ } ∈ 𝐸 ∧ { ⟨ 0 , 𝑌 ⟩ , ⟨ 0 , ( ( ( 2nd ‘ ⟨ 0 , 𝑌 ⟩ ) − 1 ) mod 𝑁 ) ⟩ } ∈ 𝐸 ) )
153 op2ndg ⊢ ( ( 0 ∈ V ∧ 𝑌 ∈ 𝐼 ) → ( 2nd ‘ ⟨ 0 , 𝑌 ⟩ ) = 𝑌 )
154 11 153 mpan ⊢ ( 𝑌 ∈ 𝐼 → ( 2nd ‘ ⟨ 0 , 𝑌 ⟩ ) = 𝑌 )
155 oveq1 ⊢ ( ( 2nd ‘ ⟨ 0 , 𝑌 ⟩ ) = 𝑌 → ( ( 2nd ‘ ⟨ 0 , 𝑌 ⟩ ) − 1 ) = ( 𝑌 − 1 ) )
156 155 oveq1d ⊢ ( ( 2nd ‘ ⟨ 0 , 𝑌 ⟩ ) = 𝑌 → ( ( ( 2nd ‘ ⟨ 0 , 𝑌 ⟩ ) − 1 ) mod 𝑁 ) = ( ( 𝑌 − 1 ) mod 𝑁 ) )
157 156 opeq2d ⊢ ( ( 2nd ‘ ⟨ 0 , 𝑌 ⟩ ) = 𝑌 → ⟨ 0 , ( ( ( 2nd ‘ ⟨ 0 , 𝑌 ⟩ ) − 1 ) mod 𝑁 ) ⟩ = ⟨ 0 , ( ( 𝑌 − 1 ) mod 𝑁 ) ⟩ )
158 157 preq2d ⊢ ( ( 2nd ‘ ⟨ 0 , 𝑌 ⟩ ) = 𝑌 → { ⟨ 0 , 𝑌 ⟩ , ⟨ 0 , ( ( ( 2nd ‘ ⟨ 0 , 𝑌 ⟩ ) − 1 ) mod 𝑁 ) ⟩ } = { ⟨ 0 , 𝑌 ⟩ , ⟨ 0 , ( ( 𝑌 − 1 ) mod 𝑁 ) ⟩ } )
159 prcom ⊢ { ⟨ 0 , 𝑌 ⟩ , ⟨ 0 , ( ( 𝑌 − 1 ) mod 𝑁 ) ⟩ } = { ⟨ 0 , ( ( 𝑌 − 1 ) mod 𝑁 ) ⟩ , ⟨ 0 , 𝑌 ⟩ }
160 158 159 eqtrdi ⊢ ( ( 2nd ‘ ⟨ 0 , 𝑌 ⟩ ) = 𝑌 → { ⟨ 0 , 𝑌 ⟩ , ⟨ 0 , ( ( ( 2nd ‘ ⟨ 0 , 𝑌 ⟩ ) − 1 ) mod 𝑁 ) ⟩ } = { ⟨ 0 , ( ( 𝑌 − 1 ) mod 𝑁 ) ⟩ , ⟨ 0 , 𝑌 ⟩ } )
161 160 eleq1d ⊢ ( ( 2nd ‘ ⟨ 0 , 𝑌 ⟩ ) = 𝑌 → ( { ⟨ 0 , 𝑌 ⟩ , ⟨ 0 , ( ( ( 2nd ‘ ⟨ 0 , 𝑌 ⟩ ) − 1 ) mod 𝑁 ) ⟩ } ∈ 𝐸 ↔ { ⟨ 0 , ( ( 𝑌 − 1 ) mod 𝑁 ) ⟩ , ⟨ 0 , 𝑌 ⟩ } ∈ 𝐸 ) )
162 oveq1 ⊢ ( ( 2nd ‘ ⟨ 0 , 𝑌 ⟩ ) = 𝑌 → ( ( 2nd ‘ ⟨ 0 , 𝑌 ⟩ ) + 1 ) = ( 𝑌 + 1 ) )
163 162 oveq1d ⊢ ( ( 2nd ‘ ⟨ 0 , 𝑌 ⟩ ) = 𝑌 → ( ( ( 2nd ‘ ⟨ 0 , 𝑌 ⟩ ) + 1 ) mod 𝑁 ) = ( ( 𝑌 + 1 ) mod 𝑁 ) )
164 163 opeq2d ⊢ ( ( 2nd ‘ ⟨ 0 , 𝑌 ⟩ ) = 𝑌 → ⟨ 0 , ( ( ( 2nd ‘ ⟨ 0 , 𝑌 ⟩ ) + 1 ) mod 𝑁 ) ⟩ = ⟨ 0 , ( ( 𝑌 + 1 ) mod 𝑁 ) ⟩ )
165 164 preq2d ⊢ ( ( 2nd ‘ ⟨ 0 , 𝑌 ⟩ ) = 𝑌 → { ⟨ 0 , 𝑌 ⟩ , ⟨ 0 , ( ( ( 2nd ‘ ⟨ 0 , 𝑌 ⟩ ) + 1 ) mod 𝑁 ) ⟩ } = { ⟨ 0 , 𝑌 ⟩ , ⟨ 0 , ( ( 𝑌 + 1 ) mod 𝑁 ) ⟩ } )
166 165 eleq1d ⊢ ( ( 2nd ‘ ⟨ 0 , 𝑌 ⟩ ) = 𝑌 → ( { ⟨ 0 , 𝑌 ⟩ , ⟨ 0 , ( ( ( 2nd ‘ ⟨ 0 , 𝑌 ⟩ ) + 1 ) mod 𝑁 ) ⟩ } ∈ 𝐸 ↔ { ⟨ 0 , 𝑌 ⟩ , ⟨ 0 , ( ( 𝑌 + 1 ) mod 𝑁 ) ⟩ } ∈ 𝐸 ) )
167 161 166 anbi12d ⊢ ( ( 2nd ‘ ⟨ 0 , 𝑌 ⟩ ) = 𝑌 → ( ( { ⟨ 0 , 𝑌 ⟩ , ⟨ 0 , ( ( ( 2nd ‘ ⟨ 0 , 𝑌 ⟩ ) − 1 ) mod 𝑁 ) ⟩ } ∈ 𝐸 ∧ { ⟨ 0 , 𝑌 ⟩ , ⟨ 0 , ( ( ( 2nd ‘ ⟨ 0 , 𝑌 ⟩ ) + 1 ) mod 𝑁 ) ⟩ } ∈ 𝐸 ) ↔ ( { ⟨ 0 , ( ( 𝑌 − 1 ) mod 𝑁 ) ⟩ , ⟨ 0 , 𝑌 ⟩ } ∈ 𝐸 ∧ { ⟨ 0 , 𝑌 ⟩ , ⟨ 0 , ( ( 𝑌 + 1 ) mod 𝑁 ) ⟩ } ∈ 𝐸 ) ) )
168 154 167 syl ⊢ ( 𝑌 ∈ 𝐼 → ( ( { ⟨ 0 , 𝑌 ⟩ , ⟨ 0 , ( ( ( 2nd ‘ ⟨ 0 , 𝑌 ⟩ ) − 1 ) mod 𝑁 ) ⟩ } ∈ 𝐸 ∧ { ⟨ 0 , 𝑌 ⟩ , ⟨ 0 , ( ( ( 2nd ‘ ⟨ 0 , 𝑌 ⟩ ) + 1 ) mod 𝑁 ) ⟩ } ∈ 𝐸 ) ↔ ( { ⟨ 0 , ( ( 𝑌 − 1 ) mod 𝑁 ) ⟩ , ⟨ 0 , 𝑌 ⟩ } ∈ 𝐸 ∧ { ⟨ 0 , 𝑌 ⟩ , ⟨ 0 , ( ( 𝑌 + 1 ) mod 𝑁 ) ⟩ } ∈ 𝐸 ) ) )
169 168 biimpcd ⊢ ( ( { ⟨ 0 , 𝑌 ⟩ , ⟨ 0 , ( ( ( 2nd ‘ ⟨ 0 , 𝑌 ⟩ ) − 1 ) mod 𝑁 ) ⟩ } ∈ 𝐸 ∧ { ⟨ 0 , 𝑌 ⟩ , ⟨ 0 , ( ( ( 2nd ‘ ⟨ 0 , 𝑌 ⟩ ) + 1 ) mod 𝑁 ) ⟩ } ∈ 𝐸 ) → ( 𝑌 ∈ 𝐼 → ( { ⟨ 0 , ( ( 𝑌 − 1 ) mod 𝑁 ) ⟩ , ⟨ 0 , 𝑌 ⟩ } ∈ 𝐸 ∧ { ⟨ 0 , 𝑌 ⟩ , ⟨ 0 , ( ( 𝑌 + 1 ) mod 𝑁 ) ⟩ } ∈ 𝐸 ) ) )
170 169 ancoms ⊢ ( ( { ⟨ 0 , 𝑌 ⟩ , ⟨ 0 , ( ( ( 2nd ‘ ⟨ 0 , 𝑌 ⟩ ) + 1 ) mod 𝑁 ) ⟩ } ∈ 𝐸 ∧ { ⟨ 0 , 𝑌 ⟩ , ⟨ 0 , ( ( ( 2nd ‘ ⟨ 0 , 𝑌 ⟩ ) − 1 ) mod 𝑁 ) ⟩ } ∈ 𝐸 ) → ( 𝑌 ∈ 𝐼 → ( { ⟨ 0 , ( ( 𝑌 − 1 ) mod 𝑁 ) ⟩ , ⟨ 0 , 𝑌 ⟩ } ∈ 𝐸 ∧ { ⟨ 0 , 𝑌 ⟩ , ⟨ 0 , ( ( 𝑌 + 1 ) mod 𝑁 ) ⟩ } ∈ 𝐸 ) ) )
171 170 3adant2 ⊢ ( ( { ⟨ 0 , 𝑌 ⟩ , ⟨ 0 , ( ( ( 2nd ‘ ⟨ 0 , 𝑌 ⟩ ) + 1 ) mod 𝑁 ) ⟩ } ∈ 𝐸 ∧ { ⟨ 0 , 𝑌 ⟩ , ⟨ 1 , ( 2nd ‘ ⟨ 0 , 𝑌 ⟩ ) ⟩ } ∈ 𝐸 ∧ { ⟨ 0 , 𝑌 ⟩ , ⟨ 0 , ( ( ( 2nd ‘ ⟨ 0 , 𝑌 ⟩ ) − 1 ) mod 𝑁 ) ⟩ } ∈ 𝐸 ) → ( 𝑌 ∈ 𝐼 → ( { ⟨ 0 , ( ( 𝑌 − 1 ) mod 𝑁 ) ⟩ , ⟨ 0 , 𝑌 ⟩ } ∈ 𝐸 ∧ { ⟨ 0 , 𝑌 ⟩ , ⟨ 0 , ( ( 𝑌 + 1 ) mod 𝑁 ) ⟩ } ∈ 𝐸 ) ) )
172 171 com12 ⊢ ( 𝑌 ∈ 𝐼 → ( ( { ⟨ 0 , 𝑌 ⟩ , ⟨ 0 , ( ( ( 2nd ‘ ⟨ 0 , 𝑌 ⟩ ) + 1 ) mod 𝑁 ) ⟩ } ∈ 𝐸 ∧ { ⟨ 0 , 𝑌 ⟩ , ⟨ 1 , ( 2nd ‘ ⟨ 0 , 𝑌 ⟩ ) ⟩ } ∈ 𝐸 ∧ { ⟨ 0 , 𝑌 ⟩ , ⟨ 0 , ( ( ( 2nd ‘ ⟨ 0 , 𝑌 ⟩ ) − 1 ) mod 𝑁 ) ⟩ } ∈ 𝐸 ) → ( { ⟨ 0 , ( ( 𝑌 − 1 ) mod 𝑁 ) ⟩ , ⟨ 0 , 𝑌 ⟩ } ∈ 𝐸 ∧ { ⟨ 0 , 𝑌 ⟩ , ⟨ 0 , ( ( 𝑌 + 1 ) mod 𝑁 ) ⟩ } ∈ 𝐸 ) ) )
173 172 adantl ⊢ ( ( 𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝐼 ) → ( ( { ⟨ 0 , 𝑌 ⟩ , ⟨ 0 , ( ( ( 2nd ‘ ⟨ 0 , 𝑌 ⟩ ) + 1 ) mod 𝑁 ) ⟩ } ∈ 𝐸 ∧ { ⟨ 0 , 𝑌 ⟩ , ⟨ 1 , ( 2nd ‘ ⟨ 0 , 𝑌 ⟩ ) ⟩ } ∈ 𝐸 ∧ { ⟨ 0 , 𝑌 ⟩ , ⟨ 0 , ( ( ( 2nd ‘ ⟨ 0 , 𝑌 ⟩ ) − 1 ) mod 𝑁 ) ⟩ } ∈ 𝐸 ) → ( { ⟨ 0 , ( ( 𝑌 − 1 ) mod 𝑁 ) ⟩ , ⟨ 0 , 𝑌 ⟩ } ∈ 𝐸 ∧ { ⟨ 0 , 𝑌 ⟩ , ⟨ 0 , ( ( 𝑌 + 1 ) mod 𝑁 ) ⟩ } ∈ 𝐸 ) ) )
174 173 adantl ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 5 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝐼 ) ) → ( ( { ⟨ 0 , 𝑌 ⟩ , ⟨ 0 , ( ( ( 2nd ‘ ⟨ 0 , 𝑌 ⟩ ) + 1 ) mod 𝑁 ) ⟩ } ∈ 𝐸 ∧ { ⟨ 0 , 𝑌 ⟩ , ⟨ 1 , ( 2nd ‘ ⟨ 0 , 𝑌 ⟩ ) ⟩ } ∈ 𝐸 ∧ { ⟨ 0 , 𝑌 ⟩ , ⟨ 0 , ( ( ( 2nd ‘ ⟨ 0 , 𝑌 ⟩ ) − 1 ) mod 𝑁 ) ⟩ } ∈ 𝐸 ) → ( { ⟨ 0 , ( ( 𝑌 − 1 ) mod 𝑁 ) ⟩ , ⟨ 0 , 𝑌 ⟩ } ∈ 𝐸 ∧ { ⟨ 0 , 𝑌 ⟩ , ⟨ 0 , ( ( 𝑌 + 1 ) mod 𝑁 ) ⟩ } ∈ 𝐸 ) ) )
175 152 174 mpd ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 5 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝐼 ) ) → ( { ⟨ 0 , ( ( 𝑌 − 1 ) mod 𝑁 ) ⟩ , ⟨ 0 , 𝑌 ⟩ } ∈ 𝐸 ∧ { ⟨ 0 , 𝑌 ⟩ , ⟨ 0 , ( ( 𝑌 + 1 ) mod 𝑁 ) ⟩ } ∈ 𝐸 ) )
176 opeq2 ⊢ ( 𝑋 = 𝑌 → ⟨ 0 , 𝑋 ⟩ = ⟨ 0 , 𝑌 ⟩ )
177 176 preq2d ⊢ ( 𝑋 = 𝑌 → { ⟨ 0 , ( ( 𝑌 − 1 ) mod 𝑁 ) ⟩ , ⟨ 0 , 𝑋 ⟩ } = { ⟨ 0 , ( ( 𝑌 − 1 ) mod 𝑁 ) ⟩ , ⟨ 0 , 𝑌 ⟩ } )
178 177 eleq1d ⊢ ( 𝑋 = 𝑌 → ( { ⟨ 0 , ( ( 𝑌 − 1 ) mod 𝑁 ) ⟩ , ⟨ 0 , 𝑋 ⟩ } ∈ 𝐸 ↔ { ⟨ 0 , ( ( 𝑌 − 1 ) mod 𝑁 ) ⟩ , ⟨ 0 , 𝑌 ⟩ } ∈ 𝐸 ) )
179 176 preq1d ⊢ ( 𝑋 = 𝑌 → { ⟨ 0 , 𝑋 ⟩ , ⟨ 0 , ( ( 𝑌 + 1 ) mod 𝑁 ) ⟩ } = { ⟨ 0 , 𝑌 ⟩ , ⟨ 0 , ( ( 𝑌 + 1 ) mod 𝑁 ) ⟩ } )
180 179 eleq1d ⊢ ( 𝑋 = 𝑌 → ( { ⟨ 0 , 𝑋 ⟩ , ⟨ 0 , ( ( 𝑌 + 1 ) mod 𝑁 ) ⟩ } ∈ 𝐸 ↔ { ⟨ 0 , 𝑌 ⟩ , ⟨ 0 , ( ( 𝑌 + 1 ) mod 𝑁 ) ⟩ } ∈ 𝐸 ) )
181 178 180 anbi12d ⊢ ( 𝑋 = 𝑌 → ( ( { ⟨ 0 , ( ( 𝑌 − 1 ) mod 𝑁 ) ⟩ , ⟨ 0 , 𝑋 ⟩ } ∈ 𝐸 ∧ { ⟨ 0 , 𝑋 ⟩ , ⟨ 0 , ( ( 𝑌 + 1 ) mod 𝑁 ) ⟩ } ∈ 𝐸 ) ↔ ( { ⟨ 0 , ( ( 𝑌 − 1 ) mod 𝑁 ) ⟩ , ⟨ 0 , 𝑌 ⟩ } ∈ 𝐸 ∧ { ⟨ 0 , 𝑌 ⟩ , ⟨ 0 , ( ( 𝑌 + 1 ) mod 𝑁 ) ⟩ } ∈ 𝐸 ) ) )
182 175 181 syl5ibrcom ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 5 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝐼 ) ) → ( 𝑋 = 𝑌 → ( { ⟨ 0 , ( ( 𝑌 − 1 ) mod 𝑁 ) ⟩ , ⟨ 0 , 𝑋 ⟩ } ∈ 𝐸 ∧ { ⟨ 0 , 𝑋 ⟩ , ⟨ 0 , ( ( 𝑌 + 1 ) mod 𝑁 ) ⟩ } ∈ 𝐸 ) ) )
183 138 182 impbid ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 5 ) ∧ 𝐾 ∈ 𝐽 ) ∧ ( 𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝐼 ) ) → ( ( { ⟨ 0 , ( ( 𝑌 − 1 ) mod 𝑁 ) ⟩ , ⟨ 0 , 𝑋 ⟩ } ∈ 𝐸 ∧ { ⟨ 0 , 𝑋 ⟩ , ⟨ 0 , ( ( 𝑌 + 1 ) mod 𝑁 ) ⟩ } ∈ 𝐸 ) ↔ 𝑋 = 𝑌 ) )