Metamath Proof Explorer

Theorem gpgedgel

Description: An edge in a generalized Petersen graph G . (Contributed by AV, 29-Aug-2025)

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

Proof

Step Hyp Ref Expression
1 gpgvtxel.i ⊢ 𝐼 = ( 0 ..^ 𝑁 )
2 gpgvtxel.j ⊢ 𝐽 = ( 1 ..^ ( ⌈ ‘ ( 𝑁 / 2 ) ) )
3 gpgvtxel.g ⊢ 𝐺 = ( 𝑁 gPetersenGr 𝐾 )
4 gpgedgel.e ⊢ 𝐸 = ( Edg ‘ 𝐺 )
5 3 fveq2i ⊢ ( Edg ‘ 𝐺 ) = ( Edg ‘ ( 𝑁 gPetersenGr 𝐾 ) )
6 4 5 eqtri ⊢ 𝐸 = ( Edg ‘ ( 𝑁 gPetersenGr 𝐾 ) )
7 6 eleq2i ⊢ ( 𝑌 ∈ 𝐸 ↔ 𝑌 ∈ ( Edg ‘ ( 𝑁 gPetersenGr 𝐾 ) ) )
8 eluzge3nn ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → 𝑁 ∈ ℕ )
9 2 1 gpgedg ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐾 ∈ 𝐽 ) → ( Edg ‘ ( 𝑁 gPetersenGr 𝐾 ) ) = { 𝑒 ∈ 𝒫 ( { 0 , 1 } × 𝐼 ) ∣ ∃ 𝑥 ∈ 𝐼 ( 𝑒 = { ⟨ 0 , 𝑥 ⟩ , ⟨ 0 , ( ( 𝑥 + 1 ) mod 𝑁 ) ⟩ } ∨ 𝑒 = { ⟨ 0 , 𝑥 ⟩ , ⟨ 1 , 𝑥 ⟩ } ∨ 𝑒 = { ⟨ 1 , 𝑥 ⟩ , ⟨ 1 , ( ( 𝑥 + 𝐾 ) mod 𝑁 ) ⟩ } ) } )
10 8 9 sylan ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) → ( Edg ‘ ( 𝑁 gPetersenGr 𝐾 ) ) = { 𝑒 ∈ 𝒫 ( { 0 , 1 } × 𝐼 ) ∣ ∃ 𝑥 ∈ 𝐼 ( 𝑒 = { ⟨ 0 , 𝑥 ⟩ , ⟨ 0 , ( ( 𝑥 + 1 ) mod 𝑁 ) ⟩ } ∨ 𝑒 = { ⟨ 0 , 𝑥 ⟩ , ⟨ 1 , 𝑥 ⟩ } ∨ 𝑒 = { ⟨ 1 , 𝑥 ⟩ , ⟨ 1 , ( ( 𝑥 + 𝐾 ) mod 𝑁 ) ⟩ } ) } )
11 10 eleq2d ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) → ( 𝑌 ∈ ( Edg ‘ ( 𝑁 gPetersenGr 𝐾 ) ) ↔ 𝑌 ∈ { 𝑒 ∈ 𝒫 ( { 0 , 1 } × 𝐼 ) ∣ ∃ 𝑥 ∈ 𝐼 ( 𝑒 = { ⟨ 0 , 𝑥 ⟩ , ⟨ 0 , ( ( 𝑥 + 1 ) mod 𝑁 ) ⟩ } ∨ 𝑒 = { ⟨ 0 , 𝑥 ⟩ , ⟨ 1 , 𝑥 ⟩ } ∨ 𝑒 = { ⟨ 1 , 𝑥 ⟩ , ⟨ 1 , ( ( 𝑥 + 𝐾 ) mod 𝑁 ) ⟩ } ) } ) )
12 7 11 bitrid ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) → ( 𝑌 ∈ 𝐸 ↔ 𝑌 ∈ { 𝑒 ∈ 𝒫 ( { 0 , 1 } × 𝐼 ) ∣ ∃ 𝑥 ∈ 𝐼 ( 𝑒 = { ⟨ 0 , 𝑥 ⟩ , ⟨ 0 , ( ( 𝑥 + 1 ) mod 𝑁 ) ⟩ } ∨ 𝑒 = { ⟨ 0 , 𝑥 ⟩ , ⟨ 1 , 𝑥 ⟩ } ∨ 𝑒 = { ⟨ 1 , 𝑥 ⟩ , ⟨ 1 , ( ( 𝑥 + 𝐾 ) mod 𝑁 ) ⟩ } ) } ) )
13 eqeq1 ⊢ ( 𝑒 = 𝑌 → ( 𝑒 = { ⟨ 0 , 𝑥 ⟩ , ⟨ 0 , ( ( 𝑥 + 1 ) mod 𝑁 ) ⟩ } ↔ 𝑌 = { ⟨ 0 , 𝑥 ⟩ , ⟨ 0 , ( ( 𝑥 + 1 ) mod 𝑁 ) ⟩ } ) )
14 eqeq1 ⊢ ( 𝑒 = 𝑌 → ( 𝑒 = { ⟨ 0 , 𝑥 ⟩ , ⟨ 1 , 𝑥 ⟩ } ↔ 𝑌 = { ⟨ 0 , 𝑥 ⟩ , ⟨ 1 , 𝑥 ⟩ } ) )
15 eqeq1 ⊢ ( 𝑒 = 𝑌 → ( 𝑒 = { ⟨ 1 , 𝑥 ⟩ , ⟨ 1 , ( ( 𝑥 + 𝐾 ) mod 𝑁 ) ⟩ } ↔ 𝑌 = { ⟨ 1 , 𝑥 ⟩ , ⟨ 1 , ( ( 𝑥 + 𝐾 ) mod 𝑁 ) ⟩ } ) )
16 13 14 15 3orbi123d ⊢ ( 𝑒 = 𝑌 → ( ( 𝑒 = { ⟨ 0 , 𝑥 ⟩ , ⟨ 0 , ( ( 𝑥 + 1 ) mod 𝑁 ) ⟩ } ∨ 𝑒 = { ⟨ 0 , 𝑥 ⟩ , ⟨ 1 , 𝑥 ⟩ } ∨ 𝑒 = { ⟨ 1 , 𝑥 ⟩ , ⟨ 1 , ( ( 𝑥 + 𝐾 ) mod 𝑁 ) ⟩ } ) ↔ ( 𝑌 = { ⟨ 0 , 𝑥 ⟩ , ⟨ 0 , ( ( 𝑥 + 1 ) mod 𝑁 ) ⟩ } ∨ 𝑌 = { ⟨ 0 , 𝑥 ⟩ , ⟨ 1 , 𝑥 ⟩ } ∨ 𝑌 = { ⟨ 1 , 𝑥 ⟩ , ⟨ 1 , ( ( 𝑥 + 𝐾 ) mod 𝑁 ) ⟩ } ) ) )
17 16 rexbidv ⊢ ( 𝑒 = 𝑌 → ( ∃ 𝑥 ∈ 𝐼 ( 𝑒 = { ⟨ 0 , 𝑥 ⟩ , ⟨ 0 , ( ( 𝑥 + 1 ) mod 𝑁 ) ⟩ } ∨ 𝑒 = { ⟨ 0 , 𝑥 ⟩ , ⟨ 1 , 𝑥 ⟩ } ∨ 𝑒 = { ⟨ 1 , 𝑥 ⟩ , ⟨ 1 , ( ( 𝑥 + 𝐾 ) mod 𝑁 ) ⟩ } ) ↔ ∃ 𝑥 ∈ 𝐼 ( 𝑌 = { ⟨ 0 , 𝑥 ⟩ , ⟨ 0 , ( ( 𝑥 + 1 ) mod 𝑁 ) ⟩ } ∨ 𝑌 = { ⟨ 0 , 𝑥 ⟩ , ⟨ 1 , 𝑥 ⟩ } ∨ 𝑌 = { ⟨ 1 , 𝑥 ⟩ , ⟨ 1 , ( ( 𝑥 + 𝐾 ) mod 𝑁 ) ⟩ } ) ) )
18 17 elrab ⊢ ( 𝑌 ∈ { 𝑒 ∈ 𝒫 ( { 0 , 1 } × 𝐼 ) ∣ ∃ 𝑥 ∈ 𝐼 ( 𝑒 = { ⟨ 0 , 𝑥 ⟩ , ⟨ 0 , ( ( 𝑥 + 1 ) mod 𝑁 ) ⟩ } ∨ 𝑒 = { ⟨ 0 , 𝑥 ⟩ , ⟨ 1 , 𝑥 ⟩ } ∨ 𝑒 = { ⟨ 1 , 𝑥 ⟩ , ⟨ 1 , ( ( 𝑥 + 𝐾 ) mod 𝑁 ) ⟩ } ) } ↔ ( 𝑌 ∈ 𝒫 ( { 0 , 1 } × 𝐼 ) ∧ ∃ 𝑥 ∈ 𝐼 ( 𝑌 = { ⟨ 0 , 𝑥 ⟩ , ⟨ 0 , ( ( 𝑥 + 1 ) mod 𝑁 ) ⟩ } ∨ 𝑌 = { ⟨ 0 , 𝑥 ⟩ , ⟨ 1 , 𝑥 ⟩ } ∨ 𝑌 = { ⟨ 1 , 𝑥 ⟩ , ⟨ 1 , ( ( 𝑥 + 𝐾 ) mod 𝑁 ) ⟩ } ) ) )
19 prex ⊢ { ⟨ 0 , 𝑥 ⟩ , ⟨ 0 , ( ( 𝑥 + 1 ) mod 𝑁 ) ⟩ } ∈ V
20 19 a1i ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ 𝑥 ∈ 𝐼 ) → { ⟨ 0 , 𝑥 ⟩ , ⟨ 0 , ( ( 𝑥 + 1 ) mod 𝑁 ) ⟩ } ∈ V )
21 c0ex ⊢ 0 ∈ V
22 21 prid1 ⊢ 0 ∈ { 0 , 1 }
23 22 a1i ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ 𝑥 ∈ 𝐼 ) → 0 ∈ { 0 , 1 } )
24 simpr ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ 𝑥 ∈ 𝐼 ) → 𝑥 ∈ 𝐼 )
25 23 24 opelxpd ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ 𝑥 ∈ 𝐼 ) → ⟨ 0 , 𝑥 ⟩ ∈ ( { 0 , 1 } × 𝐼 ) )
26 elfzoelz ⊢ ( 𝑥 ∈ ( 0 ..^ 𝑁 ) → 𝑥 ∈ ℤ )
27 26 1 eleq2s ⊢ ( 𝑥 ∈ 𝐼 → 𝑥 ∈ ℤ )
28 27 adantl ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ 𝑥 ∈ 𝐼 ) → 𝑥 ∈ ℤ )
29 28 peano2zd ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ 𝑥 ∈ 𝐼 ) → ( 𝑥 + 1 ) ∈ ℤ )
30 8 adantr ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) → 𝑁 ∈ ℕ )
31 30 adantr ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ 𝑥 ∈ 𝐼 ) → 𝑁 ∈ ℕ )
32 zmodfzo ⊢ ( ( ( 𝑥 + 1 ) ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( ( 𝑥 + 1 ) mod 𝑁 ) ∈ ( 0 ..^ 𝑁 ) )
33 29 31 32 syl2anc ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ 𝑥 ∈ 𝐼 ) → ( ( 𝑥 + 1 ) mod 𝑁 ) ∈ ( 0 ..^ 𝑁 ) )
34 33 1 eleqtrrdi ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ 𝑥 ∈ 𝐼 ) → ( ( 𝑥 + 1 ) mod 𝑁 ) ∈ 𝐼 )
35 23 34 opelxpd ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ 𝑥 ∈ 𝐼 ) → ⟨ 0 , ( ( 𝑥 + 1 ) mod 𝑁 ) ⟩ ∈ ( { 0 , 1 } × 𝐼 ) )
36 25 35 prssd ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ 𝑥 ∈ 𝐼 ) → { ⟨ 0 , 𝑥 ⟩ , ⟨ 0 , ( ( 𝑥 + 1 ) mod 𝑁 ) ⟩ } ⊆ ( { 0 , 1 } × 𝐼 ) )
37 20 36 elpwd ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ 𝑥 ∈ 𝐼 ) → { ⟨ 0 , 𝑥 ⟩ , ⟨ 0 , ( ( 𝑥 + 1 ) mod 𝑁 ) ⟩ } ∈ 𝒫 ( { 0 , 1 } × 𝐼 ) )
38 eleq1 ⊢ ( 𝑌 = { ⟨ 0 , 𝑥 ⟩ , ⟨ 0 , ( ( 𝑥 + 1 ) mod 𝑁 ) ⟩ } → ( 𝑌 ∈ 𝒫 ( { 0 , 1 } × 𝐼 ) ↔ { ⟨ 0 , 𝑥 ⟩ , ⟨ 0 , ( ( 𝑥 + 1 ) mod 𝑁 ) ⟩ } ∈ 𝒫 ( { 0 , 1 } × 𝐼 ) ) )
39 37 38 syl5ibrcom ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ 𝑥 ∈ 𝐼 ) → ( 𝑌 = { ⟨ 0 , 𝑥 ⟩ , ⟨ 0 , ( ( 𝑥 + 1 ) mod 𝑁 ) ⟩ } → 𝑌 ∈ 𝒫 ( { 0 , 1 } × 𝐼 ) ) )
40 prex ⊢ { ⟨ 0 , 𝑥 ⟩ , ⟨ 1 , 𝑥 ⟩ } ∈ V
41 40 a1i ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ 𝑥 ∈ 𝐼 ) → { ⟨ 0 , 𝑥 ⟩ , ⟨ 1 , 𝑥 ⟩ } ∈ V )
42 1ex ⊢ 1 ∈ V
43 42 prid2 ⊢ 1 ∈ { 0 , 1 }
44 43 a1i ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ 𝑥 ∈ 𝐼 ) → 1 ∈ { 0 , 1 } )
45 44 24 opelxpd ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ 𝑥 ∈ 𝐼 ) → ⟨ 1 , 𝑥 ⟩ ∈ ( { 0 , 1 } × 𝐼 ) )
46 25 45 prssd ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ 𝑥 ∈ 𝐼 ) → { ⟨ 0 , 𝑥 ⟩ , ⟨ 1 , 𝑥 ⟩ } ⊆ ( { 0 , 1 } × 𝐼 ) )
47 41 46 elpwd ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ 𝑥 ∈ 𝐼 ) → { ⟨ 0 , 𝑥 ⟩ , ⟨ 1 , 𝑥 ⟩ } ∈ 𝒫 ( { 0 , 1 } × 𝐼 ) )
48 eleq1 ⊢ ( 𝑌 = { ⟨ 0 , 𝑥 ⟩ , ⟨ 1 , 𝑥 ⟩ } → ( 𝑌 ∈ 𝒫 ( { 0 , 1 } × 𝐼 ) ↔ { ⟨ 0 , 𝑥 ⟩ , ⟨ 1 , 𝑥 ⟩ } ∈ 𝒫 ( { 0 , 1 } × 𝐼 ) ) )
49 47 48 syl5ibrcom ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ 𝑥 ∈ 𝐼 ) → ( 𝑌 = { ⟨ 0 , 𝑥 ⟩ , ⟨ 1 , 𝑥 ⟩ } → 𝑌 ∈ 𝒫 ( { 0 , 1 } × 𝐼 ) ) )
50 prex ⊢ { ⟨ 1 , 𝑥 ⟩ , ⟨ 1 , ( ( 𝑥 + 𝐾 ) mod 𝑁 ) ⟩ } ∈ V
51 50 a1i ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ 𝑥 ∈ 𝐼 ) → { ⟨ 1 , 𝑥 ⟩ , ⟨ 1 , ( ( 𝑥 + 𝐾 ) mod 𝑁 ) ⟩ } ∈ V )
52 elfzoelz ⊢ ( 𝐾 ∈ ( 1 ..^ ( ⌈ ‘ ( 𝑁 / 2 ) ) ) → 𝐾 ∈ ℤ )
53 52 2 eleq2s ⊢ ( 𝐾 ∈ 𝐽 → 𝐾 ∈ ℤ )
54 53 adantl ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) → 𝐾 ∈ ℤ )
55 54 adantr ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ 𝑥 ∈ 𝐼 ) → 𝐾 ∈ ℤ )
56 28 55 zaddcld ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ 𝑥 ∈ 𝐼 ) → ( 𝑥 + 𝐾 ) ∈ ℤ )
57 zmodfzo ⊢ ( ( ( 𝑥 + 𝐾 ) ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( ( 𝑥 + 𝐾 ) mod 𝑁 ) ∈ ( 0 ..^ 𝑁 ) )
58 56 31 57 syl2anc ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ 𝑥 ∈ 𝐼 ) → ( ( 𝑥 + 𝐾 ) mod 𝑁 ) ∈ ( 0 ..^ 𝑁 ) )
59 58 1 eleqtrrdi ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ 𝑥 ∈ 𝐼 ) → ( ( 𝑥 + 𝐾 ) mod 𝑁 ) ∈ 𝐼 )
60 44 59 opelxpd ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ 𝑥 ∈ 𝐼 ) → ⟨ 1 , ( ( 𝑥 + 𝐾 ) mod 𝑁 ) ⟩ ∈ ( { 0 , 1 } × 𝐼 ) )
61 45 60 prssd ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ 𝑥 ∈ 𝐼 ) → { ⟨ 1 , 𝑥 ⟩ , ⟨ 1 , ( ( 𝑥 + 𝐾 ) mod 𝑁 ) ⟩ } ⊆ ( { 0 , 1 } × 𝐼 ) )
62 51 61 elpwd ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ 𝑥 ∈ 𝐼 ) → { ⟨ 1 , 𝑥 ⟩ , ⟨ 1 , ( ( 𝑥 + 𝐾 ) mod 𝑁 ) ⟩ } ∈ 𝒫 ( { 0 , 1 } × 𝐼 ) )
63 eleq1 ⊢ ( 𝑌 = { ⟨ 1 , 𝑥 ⟩ , ⟨ 1 , ( ( 𝑥 + 𝐾 ) mod 𝑁 ) ⟩ } → ( 𝑌 ∈ 𝒫 ( { 0 , 1 } × 𝐼 ) ↔ { ⟨ 1 , 𝑥 ⟩ , ⟨ 1 , ( ( 𝑥 + 𝐾 ) mod 𝑁 ) ⟩ } ∈ 𝒫 ( { 0 , 1 } × 𝐼 ) ) )
64 62 63 syl5ibrcom ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ 𝑥 ∈ 𝐼 ) → ( 𝑌 = { ⟨ 1 , 𝑥 ⟩ , ⟨ 1 , ( ( 𝑥 + 𝐾 ) mod 𝑁 ) ⟩ } → 𝑌 ∈ 𝒫 ( { 0 , 1 } × 𝐼 ) ) )
65 39 49 64 3jaod ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) ∧ 𝑥 ∈ 𝐼 ) → ( ( 𝑌 = { ⟨ 0 , 𝑥 ⟩ , ⟨ 0 , ( ( 𝑥 + 1 ) mod 𝑁 ) ⟩ } ∨ 𝑌 = { ⟨ 0 , 𝑥 ⟩ , ⟨ 1 , 𝑥 ⟩ } ∨ 𝑌 = { ⟨ 1 , 𝑥 ⟩ , ⟨ 1 , ( ( 𝑥 + 𝐾 ) mod 𝑁 ) ⟩ } ) → 𝑌 ∈ 𝒫 ( { 0 , 1 } × 𝐼 ) ) )
66 65 rexlimdva ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) → ( ∃ 𝑥 ∈ 𝐼 ( 𝑌 = { ⟨ 0 , 𝑥 ⟩ , ⟨ 0 , ( ( 𝑥 + 1 ) mod 𝑁 ) ⟩ } ∨ 𝑌 = { ⟨ 0 , 𝑥 ⟩ , ⟨ 1 , 𝑥 ⟩ } ∨ 𝑌 = { ⟨ 1 , 𝑥 ⟩ , ⟨ 1 , ( ( 𝑥 + 𝐾 ) mod 𝑁 ) ⟩ } ) → 𝑌 ∈ 𝒫 ( { 0 , 1 } × 𝐼 ) ) )
67 66 pm4.71rd ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) → ( ∃ 𝑥 ∈ 𝐼 ( 𝑌 = { ⟨ 0 , 𝑥 ⟩ , ⟨ 0 , ( ( 𝑥 + 1 ) mod 𝑁 ) ⟩ } ∨ 𝑌 = { ⟨ 0 , 𝑥 ⟩ , ⟨ 1 , 𝑥 ⟩ } ∨ 𝑌 = { ⟨ 1 , 𝑥 ⟩ , ⟨ 1 , ( ( 𝑥 + 𝐾 ) mod 𝑁 ) ⟩ } ) ↔ ( 𝑌 ∈ 𝒫 ( { 0 , 1 } × 𝐼 ) ∧ ∃ 𝑥 ∈ 𝐼 ( 𝑌 = { ⟨ 0 , 𝑥 ⟩ , ⟨ 0 , ( ( 𝑥 + 1 ) mod 𝑁 ) ⟩ } ∨ 𝑌 = { ⟨ 0 , 𝑥 ⟩ , ⟨ 1 , 𝑥 ⟩ } ∨ 𝑌 = { ⟨ 1 , 𝑥 ⟩ , ⟨ 1 , ( ( 𝑥 + 𝐾 ) mod 𝑁 ) ⟩ } ) ) ) )
68 18 67 bitr4id ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) → ( 𝑌 ∈ { 𝑒 ∈ 𝒫 ( { 0 , 1 } × 𝐼 ) ∣ ∃ 𝑥 ∈ 𝐼 ( 𝑒 = { ⟨ 0 , 𝑥 ⟩ , ⟨ 0 , ( ( 𝑥 + 1 ) mod 𝑁 ) ⟩ } ∨ 𝑒 = { ⟨ 0 , 𝑥 ⟩ , ⟨ 1 , 𝑥 ⟩ } ∨ 𝑒 = { ⟨ 1 , 𝑥 ⟩ , ⟨ 1 , ( ( 𝑥 + 𝐾 ) mod 𝑁 ) ⟩ } ) } ↔ ∃ 𝑥 ∈ 𝐼 ( 𝑌 = { ⟨ 0 , 𝑥 ⟩ , ⟨ 0 , ( ( 𝑥 + 1 ) mod 𝑁 ) ⟩ } ∨ 𝑌 = { ⟨ 0 , 𝑥 ⟩ , ⟨ 1 , 𝑥 ⟩ } ∨ 𝑌 = { ⟨ 1 , 𝑥 ⟩ , ⟨ 1 , ( ( 𝑥 + 𝐾 ) mod 𝑁 ) ⟩ } ) ) )
69 12 68 bitrd ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ 𝐽 ) → ( 𝑌 ∈ 𝐸 ↔ ∃ 𝑥 ∈ 𝐼 ( 𝑌 = { ⟨ 0 , 𝑥 ⟩ , ⟨ 0 , ( ( 𝑥 + 1 ) mod 𝑁 ) ⟩ } ∨ 𝑌 = { ⟨ 0 , 𝑥 ⟩ , ⟨ 1 , 𝑥 ⟩ } ∨ 𝑌 = { ⟨ 1 , 𝑥 ⟩ , ⟨ 1 , ( ( 𝑥 + 𝐾 ) mod 𝑁 ) ⟩ } ) ) )