Metamath Proof Explorer

Theorem gpgov

Description: The generalized Petersen graph GPG(N,K). (Contributed by AV, 26-Aug-2025)

Ref Expression
Hypotheses gpgov.j ⊢ 𝐽 = ( 1 ..^ ( ⌈ ‘ ( 𝑁 / 2 ) ) )
gpgov.i ⊢ 𝐼 = ( 0 ..^ 𝑁 )
Assertion gpgov ( ( 𝑁 ∈ ℕ ∧ 𝐾 ∈ 𝐽 ) → ( 𝑁 gPetersenGr 𝐾 ) = { ⟨ ( Base ‘ ndx ) , ( { 0 , 1 } × 𝐼 ) ⟩ , ⟨ ( .ef ‘ ndx ) , ( I ↾ { 𝑒 ∈ 𝒫 ( { 0 , 1 } × 𝐼 ) ∣ ∃ 𝑥 ∈ 𝐼 ( 𝑒 = { ⟨ 0 , 𝑥 ⟩ , ⟨ 0 , ( ( 𝑥 + 1 ) mod 𝑁 ) ⟩ } ∨ 𝑒 = { ⟨ 0 , 𝑥 ⟩ , ⟨ 1 , 𝑥 ⟩ } ∨ 𝑒 = { ⟨ 1 , 𝑥 ⟩ , ⟨ 1 , ( ( 𝑥 + 𝐾 ) mod 𝑁 ) ⟩ } ) } ) ⟩ } )

Proof

Step Hyp Ref Expression
1 gpgov.j ⊢ 𝐽 = ( 1 ..^ ( ⌈ ‘ ( 𝑁 / 2 ) ) )
2 gpgov.i ⊢ 𝐼 = ( 0 ..^ 𝑁 )
3 prex ⊢ { ⟨ ( Base ‘ ndx ) , ( { 0 , 1 } × 𝐼 ) ⟩ , ⟨ ( .ef ‘ ndx ) , ( I ↾ { 𝑒 ∈ 𝒫 ( { 0 , 1 } × 𝐼 ) ∣ ∃ 𝑥 ∈ 𝐼 ( 𝑒 = { ⟨ 0 , 𝑥 ⟩ , ⟨ 0 , ( ( 𝑥 + 1 ) mod 𝑁 ) ⟩ } ∨ 𝑒 = { ⟨ 0 , 𝑥 ⟩ , ⟨ 1 , 𝑥 ⟩ } ∨ 𝑒 = { ⟨ 1 , 𝑥 ⟩ , ⟨ 1 , ( ( 𝑥 + 𝐾 ) mod 𝑁 ) ⟩ } ) } ) ⟩ } ∈ V
4 oveq2 ⊢ ( 𝑛 = 𝑁 → ( 0 ..^ 𝑛 ) = ( 0 ..^ 𝑁 ) )
5 4 2 eqtr4di ⊢ ( 𝑛 = 𝑁 → ( 0 ..^ 𝑛 ) = 𝐼 )
6 5 xpeq2d ⊢ ( 𝑛 = 𝑁 → ( { 0 , 1 } × ( 0 ..^ 𝑛 ) ) = ( { 0 , 1 } × 𝐼 ) )
7 6 opeq2d ⊢ ( 𝑛 = 𝑁 → ⟨ ( Base ‘ ndx ) , ( { 0 , 1 } × ( 0 ..^ 𝑛 ) ) ⟩ = ⟨ ( Base ‘ ndx ) , ( { 0 , 1 } × 𝐼 ) ⟩ )
8 7 adantr ⊢ ( ( 𝑛 = 𝑁 ∧ 𝑘 = 𝐾 ) → ⟨ ( Base ‘ ndx ) , ( { 0 , 1 } × ( 0 ..^ 𝑛 ) ) ⟩ = ⟨ ( Base ‘ ndx ) , ( { 0 , 1 } × 𝐼 ) ⟩ )
9 6 pweqd ⊢ ( 𝑛 = 𝑁 → 𝒫 ( { 0 , 1 } × ( 0 ..^ 𝑛 ) ) = 𝒫 ( { 0 , 1 } × 𝐼 ) )
10 9 adantr ⊢ ( ( 𝑛 = 𝑁 ∧ 𝑘 = 𝐾 ) → 𝒫 ( { 0 , 1 } × ( 0 ..^ 𝑛 ) ) = 𝒫 ( { 0 , 1 } × 𝐼 ) )
11 5 rexeqdv ⊢ ( 𝑛 = 𝑁 → ( ∃ 𝑥 ∈ ( 0 ..^ 𝑛 ) ( 𝑒 = { ⟨ 0 , 𝑥 ⟩ , ⟨ 0 , ( ( 𝑥 + 1 ) mod 𝑛 ) ⟩ } ∨ 𝑒 = { ⟨ 0 , 𝑥 ⟩ , ⟨ 1 , 𝑥 ⟩ } ∨ 𝑒 = { ⟨ 1 , 𝑥 ⟩ , ⟨ 1 , ( ( 𝑥 + 𝑘 ) mod 𝑛 ) ⟩ } ) ↔ ∃ 𝑥 ∈ 𝐼 ( 𝑒 = { ⟨ 0 , 𝑥 ⟩ , ⟨ 0 , ( ( 𝑥 + 1 ) mod 𝑛 ) ⟩ } ∨ 𝑒 = { ⟨ 0 , 𝑥 ⟩ , ⟨ 1 , 𝑥 ⟩ } ∨ 𝑒 = { ⟨ 1 , 𝑥 ⟩ , ⟨ 1 , ( ( 𝑥 + 𝑘 ) mod 𝑛 ) ⟩ } ) ) )
12 11 adantr ⊢ ( ( 𝑛 = 𝑁 ∧ 𝑘 = 𝐾 ) → ( ∃ 𝑥 ∈ ( 0 ..^ 𝑛 ) ( 𝑒 = { ⟨ 0 , 𝑥 ⟩ , ⟨ 0 , ( ( 𝑥 + 1 ) mod 𝑛 ) ⟩ } ∨ 𝑒 = { ⟨ 0 , 𝑥 ⟩ , ⟨ 1 , 𝑥 ⟩ } ∨ 𝑒 = { ⟨ 1 , 𝑥 ⟩ , ⟨ 1 , ( ( 𝑥 + 𝑘 ) mod 𝑛 ) ⟩ } ) ↔ ∃ 𝑥 ∈ 𝐼 ( 𝑒 = { ⟨ 0 , 𝑥 ⟩ , ⟨ 0 , ( ( 𝑥 + 1 ) mod 𝑛 ) ⟩ } ∨ 𝑒 = { ⟨ 0 , 𝑥 ⟩ , ⟨ 1 , 𝑥 ⟩ } ∨ 𝑒 = { ⟨ 1 , 𝑥 ⟩ , ⟨ 1 , ( ( 𝑥 + 𝑘 ) mod 𝑛 ) ⟩ } ) ) )
13 oveq2 ⊢ ( 𝑛 = 𝑁 → ( ( 𝑥 + 1 ) mod 𝑛 ) = ( ( 𝑥 + 1 ) mod 𝑁 ) )
14 13 opeq2d ⊢ ( 𝑛 = 𝑁 → ⟨ 0 , ( ( 𝑥 + 1 ) mod 𝑛 ) ⟩ = ⟨ 0 , ( ( 𝑥 + 1 ) mod 𝑁 ) ⟩ )
15 14 preq2d ⊢ ( 𝑛 = 𝑁 → { ⟨ 0 , 𝑥 ⟩ , ⟨ 0 , ( ( 𝑥 + 1 ) mod 𝑛 ) ⟩ } = { ⟨ 0 , 𝑥 ⟩ , ⟨ 0 , ( ( 𝑥 + 1 ) mod 𝑁 ) ⟩ } )
16 15 adantr ⊢ ( ( 𝑛 = 𝑁 ∧ 𝑘 = 𝐾 ) → { ⟨ 0 , 𝑥 ⟩ , ⟨ 0 , ( ( 𝑥 + 1 ) mod 𝑛 ) ⟩ } = { ⟨ 0 , 𝑥 ⟩ , ⟨ 0 , ( ( 𝑥 + 1 ) mod 𝑁 ) ⟩ } )
17 16 eqeq2d ⊢ ( ( 𝑛 = 𝑁 ∧ 𝑘 = 𝐾 ) → ( 𝑒 = { ⟨ 0 , 𝑥 ⟩ , ⟨ 0 , ( ( 𝑥 + 1 ) mod 𝑛 ) ⟩ } ↔ 𝑒 = { ⟨ 0 , 𝑥 ⟩ , ⟨ 0 , ( ( 𝑥 + 1 ) mod 𝑁 ) ⟩ } ) )
18 biidd ⊢ ( ( 𝑛 = 𝑁 ∧ 𝑘 = 𝐾 ) → ( 𝑒 = { ⟨ 0 , 𝑥 ⟩ , ⟨ 1 , 𝑥 ⟩ } ↔ 𝑒 = { ⟨ 0 , 𝑥 ⟩ , ⟨ 1 , 𝑥 ⟩ } ) )
19 oveq2 ⊢ ( 𝑘 = 𝐾 → ( 𝑥 + 𝑘 ) = ( 𝑥 + 𝐾 ) )
20 19 adantl ⊢ ( ( 𝑛 = 𝑁 ∧ 𝑘 = 𝐾 ) → ( 𝑥 + 𝑘 ) = ( 𝑥 + 𝐾 ) )
21 simpl ⊢ ( ( 𝑛 = 𝑁 ∧ 𝑘 = 𝐾 ) → 𝑛 = 𝑁 )
22 20 21 oveq12d ⊢ ( ( 𝑛 = 𝑁 ∧ 𝑘 = 𝐾 ) → ( ( 𝑥 + 𝑘 ) mod 𝑛 ) = ( ( 𝑥 + 𝐾 ) mod 𝑁 ) )
23 22 opeq2d ⊢ ( ( 𝑛 = 𝑁 ∧ 𝑘 = 𝐾 ) → ⟨ 1 , ( ( 𝑥 + 𝑘 ) mod 𝑛 ) ⟩ = ⟨ 1 , ( ( 𝑥 + 𝐾 ) mod 𝑁 ) ⟩ )
24 23 preq2d ⊢ ( ( 𝑛 = 𝑁 ∧ 𝑘 = 𝐾 ) → { ⟨ 1 , 𝑥 ⟩ , ⟨ 1 , ( ( 𝑥 + 𝑘 ) mod 𝑛 ) ⟩ } = { ⟨ 1 , 𝑥 ⟩ , ⟨ 1 , ( ( 𝑥 + 𝐾 ) mod 𝑁 ) ⟩ } )
25 24 eqeq2d ⊢ ( ( 𝑛 = 𝑁 ∧ 𝑘 = 𝐾 ) → ( 𝑒 = { ⟨ 1 , 𝑥 ⟩ , ⟨ 1 , ( ( 𝑥 + 𝑘 ) mod 𝑛 ) ⟩ } ↔ 𝑒 = { ⟨ 1 , 𝑥 ⟩ , ⟨ 1 , ( ( 𝑥 + 𝐾 ) mod 𝑁 ) ⟩ } ) )
26 17 18 25 3orbi123d ⊢ ( ( 𝑛 = 𝑁 ∧ 𝑘 = 𝐾 ) → ( ( 𝑒 = { ⟨ 0 , 𝑥 ⟩ , ⟨ 0 , ( ( 𝑥 + 1 ) mod 𝑛 ) ⟩ } ∨ 𝑒 = { ⟨ 0 , 𝑥 ⟩ , ⟨ 1 , 𝑥 ⟩ } ∨ 𝑒 = { ⟨ 1 , 𝑥 ⟩ , ⟨ 1 , ( ( 𝑥 + 𝑘 ) mod 𝑛 ) ⟩ } ) ↔ ( 𝑒 = { ⟨ 0 , 𝑥 ⟩ , ⟨ 0 , ( ( 𝑥 + 1 ) mod 𝑁 ) ⟩ } ∨ 𝑒 = { ⟨ 0 , 𝑥 ⟩ , ⟨ 1 , 𝑥 ⟩ } ∨ 𝑒 = { ⟨ 1 , 𝑥 ⟩ , ⟨ 1 , ( ( 𝑥 + 𝐾 ) mod 𝑁 ) ⟩ } ) ) )
27 26 rexbidv ⊢ ( ( 𝑛 = 𝑁 ∧ 𝑘 = 𝐾 ) → ( ∃ 𝑥 ∈ 𝐼 ( 𝑒 = { ⟨ 0 , 𝑥 ⟩ , ⟨ 0 , ( ( 𝑥 + 1 ) mod 𝑛 ) ⟩ } ∨ 𝑒 = { ⟨ 0 , 𝑥 ⟩ , ⟨ 1 , 𝑥 ⟩ } ∨ 𝑒 = { ⟨ 1 , 𝑥 ⟩ , ⟨ 1 , ( ( 𝑥 + 𝑘 ) mod 𝑛 ) ⟩ } ) ↔ ∃ 𝑥 ∈ 𝐼 ( 𝑒 = { ⟨ 0 , 𝑥 ⟩ , ⟨ 0 , ( ( 𝑥 + 1 ) mod 𝑁 ) ⟩ } ∨ 𝑒 = { ⟨ 0 , 𝑥 ⟩ , ⟨ 1 , 𝑥 ⟩ } ∨ 𝑒 = { ⟨ 1 , 𝑥 ⟩ , ⟨ 1 , ( ( 𝑥 + 𝐾 ) mod 𝑁 ) ⟩ } ) ) )
28 12 27 bitrd ⊢ ( ( 𝑛 = 𝑁 ∧ 𝑘 = 𝐾 ) → ( ∃ 𝑥 ∈ ( 0 ..^ 𝑛 ) ( 𝑒 = { ⟨ 0 , 𝑥 ⟩ , ⟨ 0 , ( ( 𝑥 + 1 ) mod 𝑛 ) ⟩ } ∨ 𝑒 = { ⟨ 0 , 𝑥 ⟩ , ⟨ 1 , 𝑥 ⟩ } ∨ 𝑒 = { ⟨ 1 , 𝑥 ⟩ , ⟨ 1 , ( ( 𝑥 + 𝑘 ) mod 𝑛 ) ⟩ } ) ↔ ∃ 𝑥 ∈ 𝐼 ( 𝑒 = { ⟨ 0 , 𝑥 ⟩ , ⟨ 0 , ( ( 𝑥 + 1 ) mod 𝑁 ) ⟩ } ∨ 𝑒 = { ⟨ 0 , 𝑥 ⟩ , ⟨ 1 , 𝑥 ⟩ } ∨ 𝑒 = { ⟨ 1 , 𝑥 ⟩ , ⟨ 1 , ( ( 𝑥 + 𝐾 ) mod 𝑁 ) ⟩ } ) ) )
29 10 28 rabeqbidv ⊢ ( ( 𝑛 = 𝑁 ∧ 𝑘 = 𝐾 ) → { 𝑒 ∈ 𝒫 ( { 0 , 1 } × ( 0 ..^ 𝑛 ) ) ∣ ∃ 𝑥 ∈ ( 0 ..^ 𝑛 ) ( 𝑒 = { ⟨ 0 , 𝑥 ⟩ , ⟨ 0 , ( ( 𝑥 + 1 ) mod 𝑛 ) ⟩ } ∨ 𝑒 = { ⟨ 0 , 𝑥 ⟩ , ⟨ 1 , 𝑥 ⟩ } ∨ 𝑒 = { ⟨ 1 , 𝑥 ⟩ , ⟨ 1 , ( ( 𝑥 + 𝑘 ) mod 𝑛 ) ⟩ } ) } = { 𝑒 ∈ 𝒫 ( { 0 , 1 } × 𝐼 ) ∣ ∃ 𝑥 ∈ 𝐼 ( 𝑒 = { ⟨ 0 , 𝑥 ⟩ , ⟨ 0 , ( ( 𝑥 + 1 ) mod 𝑁 ) ⟩ } ∨ 𝑒 = { ⟨ 0 , 𝑥 ⟩ , ⟨ 1 , 𝑥 ⟩ } ∨ 𝑒 = { ⟨ 1 , 𝑥 ⟩ , ⟨ 1 , ( ( 𝑥 + 𝐾 ) mod 𝑁 ) ⟩ } ) } )
30 29 reseq2d ⊢ ( ( 𝑛 = 𝑁 ∧ 𝑘 = 𝐾 ) → ( I ↾ { 𝑒 ∈ 𝒫 ( { 0 , 1 } × ( 0 ..^ 𝑛 ) ) ∣ ∃ 𝑥 ∈ ( 0 ..^ 𝑛 ) ( 𝑒 = { ⟨ 0 , 𝑥 ⟩ , ⟨ 0 , ( ( 𝑥 + 1 ) mod 𝑛 ) ⟩ } ∨ 𝑒 = { ⟨ 0 , 𝑥 ⟩ , ⟨ 1 , 𝑥 ⟩ } ∨ 𝑒 = { ⟨ 1 , 𝑥 ⟩ , ⟨ 1 , ( ( 𝑥 + 𝑘 ) mod 𝑛 ) ⟩ } ) } ) = ( I ↾ { 𝑒 ∈ 𝒫 ( { 0 , 1 } × 𝐼 ) ∣ ∃ 𝑥 ∈ 𝐼 ( 𝑒 = { ⟨ 0 , 𝑥 ⟩ , ⟨ 0 , ( ( 𝑥 + 1 ) mod 𝑁 ) ⟩ } ∨ 𝑒 = { ⟨ 0 , 𝑥 ⟩ , ⟨ 1 , 𝑥 ⟩ } ∨ 𝑒 = { ⟨ 1 , 𝑥 ⟩ , ⟨ 1 , ( ( 𝑥 + 𝐾 ) mod 𝑁 ) ⟩ } ) } ) )
31 30 opeq2d ⊢ ( ( 𝑛 = 𝑁 ∧ 𝑘 = 𝐾 ) → ⟨ ( .ef ‘ ndx ) , ( I ↾ { 𝑒 ∈ 𝒫 ( { 0 , 1 } × ( 0 ..^ 𝑛 ) ) ∣ ∃ 𝑥 ∈ ( 0 ..^ 𝑛 ) ( 𝑒 = { ⟨ 0 , 𝑥 ⟩ , ⟨ 0 , ( ( 𝑥 + 1 ) mod 𝑛 ) ⟩ } ∨ 𝑒 = { ⟨ 0 , 𝑥 ⟩ , ⟨ 1 , 𝑥 ⟩ } ∨ 𝑒 = { ⟨ 1 , 𝑥 ⟩ , ⟨ 1 , ( ( 𝑥 + 𝑘 ) mod 𝑛 ) ⟩ } ) } ) ⟩ = ⟨ ( .ef ‘ ndx ) , ( I ↾ { 𝑒 ∈ 𝒫 ( { 0 , 1 } × 𝐼 ) ∣ ∃ 𝑥 ∈ 𝐼 ( 𝑒 = { ⟨ 0 , 𝑥 ⟩ , ⟨ 0 , ( ( 𝑥 + 1 ) mod 𝑁 ) ⟩ } ∨ 𝑒 = { ⟨ 0 , 𝑥 ⟩ , ⟨ 1 , 𝑥 ⟩ } ∨ 𝑒 = { ⟨ 1 , 𝑥 ⟩ , ⟨ 1 , ( ( 𝑥 + 𝐾 ) mod 𝑁 ) ⟩ } ) } ) ⟩ )
32 8 31 preq12d ⊢ ( ( 𝑛 = 𝑁 ∧ 𝑘 = 𝐾 ) → { ⟨ ( Base ‘ ndx ) , ( { 0 , 1 } × ( 0 ..^ 𝑛 ) ) ⟩ , ⟨ ( .ef ‘ ndx ) , ( I ↾ { 𝑒 ∈ 𝒫 ( { 0 , 1 } × ( 0 ..^ 𝑛 ) ) ∣ ∃ 𝑥 ∈ ( 0 ..^ 𝑛 ) ( 𝑒 = { ⟨ 0 , 𝑥 ⟩ , ⟨ 0 , ( ( 𝑥 + 1 ) mod 𝑛 ) ⟩ } ∨ 𝑒 = { ⟨ 0 , 𝑥 ⟩ , ⟨ 1 , 𝑥 ⟩ } ∨ 𝑒 = { ⟨ 1 , 𝑥 ⟩ , ⟨ 1 , ( ( 𝑥 + 𝑘 ) mod 𝑛 ) ⟩ } ) } ) ⟩ } = { ⟨ ( Base ‘ ndx ) , ( { 0 , 1 } × 𝐼 ) ⟩ , ⟨ ( .ef ‘ ndx ) , ( I ↾ { 𝑒 ∈ 𝒫 ( { 0 , 1 } × 𝐼 ) ∣ ∃ 𝑥 ∈ 𝐼 ( 𝑒 = { ⟨ 0 , 𝑥 ⟩ , ⟨ 0 , ( ( 𝑥 + 1 ) mod 𝑁 ) ⟩ } ∨ 𝑒 = { ⟨ 0 , 𝑥 ⟩ , ⟨ 1 , 𝑥 ⟩ } ∨ 𝑒 = { ⟨ 1 , 𝑥 ⟩ , ⟨ 1 , ( ( 𝑥 + 𝐾 ) mod 𝑁 ) ⟩ } ) } ) ⟩ } )
33 fvoveq1 ⊢ ( 𝑛 = 𝑁 → ( ⌈ ‘ ( 𝑛 / 2 ) ) = ( ⌈ ‘ ( 𝑁 / 2 ) ) )
34 33 oveq2d ⊢ ( 𝑛 = 𝑁 → ( 1 ..^ ( ⌈ ‘ ( 𝑛 / 2 ) ) ) = ( 1 ..^ ( ⌈ ‘ ( 𝑁 / 2 ) ) ) )
35 34 1 eqtr4di ⊢ ( 𝑛 = 𝑁 → ( 1 ..^ ( ⌈ ‘ ( 𝑛 / 2 ) ) ) = 𝐽 )
36 df-gpg ⊢ gPetersenGr = ( 𝑛 ∈ ℕ , 𝑘 ∈ ( 1 ..^ ( ⌈ ‘ ( 𝑛 / 2 ) ) ) ↦ { ⟨ ( Base ‘ ndx ) , ( { 0 , 1 } × ( 0 ..^ 𝑛 ) ) ⟩ , ⟨ ( .ef ‘ ndx ) , ( I ↾ { 𝑒 ∈ 𝒫 ( { 0 , 1 } × ( 0 ..^ 𝑛 ) ) ∣ ∃ 𝑥 ∈ ( 0 ..^ 𝑛 ) ( 𝑒 = { ⟨ 0 , 𝑥 ⟩ , ⟨ 0 , ( ( 𝑥 + 1 ) mod 𝑛 ) ⟩ } ∨ 𝑒 = { ⟨ 0 , 𝑥 ⟩ , ⟨ 1 , 𝑥 ⟩ } ∨ 𝑒 = { ⟨ 1 , 𝑥 ⟩ , ⟨ 1 , ( ( 𝑥 + 𝑘 ) mod 𝑛 ) ⟩ } ) } ) ⟩ } )
37 32 35 36 ovmpox ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐾 ∈ 𝐽 ∧ { ⟨ ( Base ‘ ndx ) , ( { 0 , 1 } × 𝐼 ) ⟩ , ⟨ ( .ef ‘ ndx ) , ( I ↾ { 𝑒 ∈ 𝒫 ( { 0 , 1 } × 𝐼 ) ∣ ∃ 𝑥 ∈ 𝐼 ( 𝑒 = { ⟨ 0 , 𝑥 ⟩ , ⟨ 0 , ( ( 𝑥 + 1 ) mod 𝑁 ) ⟩ } ∨ 𝑒 = { ⟨ 0 , 𝑥 ⟩ , ⟨ 1 , 𝑥 ⟩ } ∨ 𝑒 = { ⟨ 1 , 𝑥 ⟩ , ⟨ 1 , ( ( 𝑥 + 𝐾 ) mod 𝑁 ) ⟩ } ) } ) ⟩ } ∈ V ) → ( 𝑁 gPetersenGr 𝐾 ) = { ⟨ ( Base ‘ ndx ) , ( { 0 , 1 } × 𝐼 ) ⟩ , ⟨ ( .ef ‘ ndx ) , ( I ↾ { 𝑒 ∈ 𝒫 ( { 0 , 1 } × 𝐼 ) ∣ ∃ 𝑥 ∈ 𝐼 ( 𝑒 = { ⟨ 0 , 𝑥 ⟩ , ⟨ 0 , ( ( 𝑥 + 1 ) mod 𝑁 ) ⟩ } ∨ 𝑒 = { ⟨ 0 , 𝑥 ⟩ , ⟨ 1 , 𝑥 ⟩ } ∨ 𝑒 = { ⟨ 1 , 𝑥 ⟩ , ⟨ 1 , ( ( 𝑥 + 𝐾 ) mod 𝑁 ) ⟩ } ) } ) ⟩ } )
38 3 37 mp3an3 ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐾 ∈ 𝐽 ) → ( 𝑁 gPetersenGr 𝐾 ) = { ⟨ ( Base ‘ ndx ) , ( { 0 , 1 } × 𝐼 ) ⟩ , ⟨ ( .ef ‘ ndx ) , ( I ↾ { 𝑒 ∈ 𝒫 ( { 0 , 1 } × 𝐼 ) ∣ ∃ 𝑥 ∈ 𝐼 ( 𝑒 = { ⟨ 0 , 𝑥 ⟩ , ⟨ 0 , ( ( 𝑥 + 1 ) mod 𝑁 ) ⟩ } ∨ 𝑒 = { ⟨ 0 , 𝑥 ⟩ , ⟨ 1 , 𝑥 ⟩ } ∨ 𝑒 = { ⟨ 1 , 𝑥 ⟩ , ⟨ 1 , ( ( 𝑥 + 𝐾 ) mod 𝑁 ) ⟩ } ) } ) ⟩ } )