Metamath Proof Explorer

Theorem gpgusgra

Description: The generalized Petersen graph GPG(N,K) is a simple graph. (Contributed by AV, 27-Aug-2025)

Ref Expression
Assertion gpgusgra ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ ( 1 ..^ ( ⌈ ‘ ( 𝑁 / 2 ) ) ) ) → ( 𝑁 gPetersenGr 𝐾 ) ∈ USGraph )

Proof

Step Hyp Ref Expression
1 f1oi ⊢ ( I ↾ { 𝑒 ∈ 𝒫 ( { 0 , 1 } × ( 0 ..^ 𝑁 ) ) ∣ ∃ 𝑥 ∈ ( 0 ..^ 𝑁 ) ( 𝑒 = { ⟨ 0 , 𝑥 ⟩ , ⟨ 0 , ( ( 𝑥 + 1 ) mod 𝑁 ) ⟩ } ∨ 𝑒 = { ⟨ 0 , 𝑥 ⟩ , ⟨ 1 , 𝑥 ⟩ } ∨ 𝑒 = { ⟨ 1 , 𝑥 ⟩ , ⟨ 1 , ( ( 𝑥 + 𝐾 ) mod 𝑁 ) ⟩ } ) } ) : { 𝑒 ∈ 𝒫 ( { 0 , 1 } × ( 0 ..^ 𝑁 ) ) ∣ ∃ 𝑥 ∈ ( 0 ..^ 𝑁 ) ( 𝑒 = { ⟨ 0 , 𝑥 ⟩ , ⟨ 0 , ( ( 𝑥 + 1 ) mod 𝑁 ) ⟩ } ∨ 𝑒 = { ⟨ 0 , 𝑥 ⟩ , ⟨ 1 , 𝑥 ⟩ } ∨ 𝑒 = { ⟨ 1 , 𝑥 ⟩ , ⟨ 1 , ( ( 𝑥 + 𝐾 ) mod 𝑁 ) ⟩ } ) } –1-1-onto→ { 𝑒 ∈ 𝒫 ( { 0 , 1 } × ( 0 ..^ 𝑁 ) ) ∣ ∃ 𝑥 ∈ ( 0 ..^ 𝑁 ) ( 𝑒 = { ⟨ 0 , 𝑥 ⟩ , ⟨ 0 , ( ( 𝑥 + 1 ) mod 𝑁 ) ⟩ } ∨ 𝑒 = { ⟨ 0 , 𝑥 ⟩ , ⟨ 1 , 𝑥 ⟩ } ∨ 𝑒 = { ⟨ 1 , 𝑥 ⟩ , ⟨ 1 , ( ( 𝑥 + 𝐾 ) mod 𝑁 ) ⟩ } ) }
2 f1of1 ⊢ ( ( I ↾ { 𝑒 ∈ 𝒫 ( { 0 , 1 } × ( 0 ..^ 𝑁 ) ) ∣ ∃ 𝑥 ∈ ( 0 ..^ 𝑁 ) ( 𝑒 = { ⟨ 0 , 𝑥 ⟩ , ⟨ 0 , ( ( 𝑥 + 1 ) mod 𝑁 ) ⟩ } ∨ 𝑒 = { ⟨ 0 , 𝑥 ⟩ , ⟨ 1 , 𝑥 ⟩ } ∨ 𝑒 = { ⟨ 1 , 𝑥 ⟩ , ⟨ 1 , ( ( 𝑥 + 𝐾 ) mod 𝑁 ) ⟩ } ) } ) : { 𝑒 ∈ 𝒫 ( { 0 , 1 } × ( 0 ..^ 𝑁 ) ) ∣ ∃ 𝑥 ∈ ( 0 ..^ 𝑁 ) ( 𝑒 = { ⟨ 0 , 𝑥 ⟩ , ⟨ 0 , ( ( 𝑥 + 1 ) mod 𝑁 ) ⟩ } ∨ 𝑒 = { ⟨ 0 , 𝑥 ⟩ , ⟨ 1 , 𝑥 ⟩ } ∨ 𝑒 = { ⟨ 1 , 𝑥 ⟩ , ⟨ 1 , ( ( 𝑥 + 𝐾 ) mod 𝑁 ) ⟩ } ) } –1-1-onto→ { 𝑒 ∈ 𝒫 ( { 0 , 1 } × ( 0 ..^ 𝑁 ) ) ∣ ∃ 𝑥 ∈ ( 0 ..^ 𝑁 ) ( 𝑒 = { ⟨ 0 , 𝑥 ⟩ , ⟨ 0 , ( ( 𝑥 + 1 ) mod 𝑁 ) ⟩ } ∨ 𝑒 = { ⟨ 0 , 𝑥 ⟩ , ⟨ 1 , 𝑥 ⟩ } ∨ 𝑒 = { ⟨ 1 , 𝑥 ⟩ , ⟨ 1 , ( ( 𝑥 + 𝐾 ) mod 𝑁 ) ⟩ } ) } → ( I ↾ { 𝑒 ∈ 𝒫 ( { 0 , 1 } × ( 0 ..^ 𝑁 ) ) ∣ ∃ 𝑥 ∈ ( 0 ..^ 𝑁 ) ( 𝑒 = { ⟨ 0 , 𝑥 ⟩ , ⟨ 0 , ( ( 𝑥 + 1 ) mod 𝑁 ) ⟩ } ∨ 𝑒 = { ⟨ 0 , 𝑥 ⟩ , ⟨ 1 , 𝑥 ⟩ } ∨ 𝑒 = { ⟨ 1 , 𝑥 ⟩ , ⟨ 1 , ( ( 𝑥 + 𝐾 ) mod 𝑁 ) ⟩ } ) } ) : { 𝑒 ∈ 𝒫 ( { 0 , 1 } × ( 0 ..^ 𝑁 ) ) ∣ ∃ 𝑥 ∈ ( 0 ..^ 𝑁 ) ( 𝑒 = { ⟨ 0 , 𝑥 ⟩ , ⟨ 0 , ( ( 𝑥 + 1 ) mod 𝑁 ) ⟩ } ∨ 𝑒 = { ⟨ 0 , 𝑥 ⟩ , ⟨ 1 , 𝑥 ⟩ } ∨ 𝑒 = { ⟨ 1 , 𝑥 ⟩ , ⟨ 1 , ( ( 𝑥 + 𝐾 ) mod 𝑁 ) ⟩ } ) } –1-1→ { 𝑒 ∈ 𝒫 ( { 0 , 1 } × ( 0 ..^ 𝑁 ) ) ∣ ∃ 𝑥 ∈ ( 0 ..^ 𝑁 ) ( 𝑒 = { ⟨ 0 , 𝑥 ⟩ , ⟨ 0 , ( ( 𝑥 + 1 ) mod 𝑁 ) ⟩ } ∨ 𝑒 = { ⟨ 0 , 𝑥 ⟩ , ⟨ 1 , 𝑥 ⟩ } ∨ 𝑒 = { ⟨ 1 , 𝑥 ⟩ , ⟨ 1 , ( ( 𝑥 + 𝐾 ) mod 𝑁 ) ⟩ } ) } )
3 1 2 mp1i ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ ( 1 ..^ ( ⌈ ‘ ( 𝑁 / 2 ) ) ) ) → ( I ↾ { 𝑒 ∈ 𝒫 ( { 0 , 1 } × ( 0 ..^ 𝑁 ) ) ∣ ∃ 𝑥 ∈ ( 0 ..^ 𝑁 ) ( 𝑒 = { ⟨ 0 , 𝑥 ⟩ , ⟨ 0 , ( ( 𝑥 + 1 ) mod 𝑁 ) ⟩ } ∨ 𝑒 = { ⟨ 0 , 𝑥 ⟩ , ⟨ 1 , 𝑥 ⟩ } ∨ 𝑒 = { ⟨ 1 , 𝑥 ⟩ , ⟨ 1 , ( ( 𝑥 + 𝐾 ) mod 𝑁 ) ⟩ } ) } ) : { 𝑒 ∈ 𝒫 ( { 0 , 1 } × ( 0 ..^ 𝑁 ) ) ∣ ∃ 𝑥 ∈ ( 0 ..^ 𝑁 ) ( 𝑒 = { ⟨ 0 , 𝑥 ⟩ , ⟨ 0 , ( ( 𝑥 + 1 ) mod 𝑁 ) ⟩ } ∨ 𝑒 = { ⟨ 0 , 𝑥 ⟩ , ⟨ 1 , 𝑥 ⟩ } ∨ 𝑒 = { ⟨ 1 , 𝑥 ⟩ , ⟨ 1 , ( ( 𝑥 + 𝐾 ) mod 𝑁 ) ⟩ } ) } –1-1→ { 𝑒 ∈ 𝒫 ( { 0 , 1 } × ( 0 ..^ 𝑁 ) ) ∣ ∃ 𝑥 ∈ ( 0 ..^ 𝑁 ) ( 𝑒 = { ⟨ 0 , 𝑥 ⟩ , ⟨ 0 , ( ( 𝑥 + 1 ) mod 𝑁 ) ⟩ } ∨ 𝑒 = { ⟨ 0 , 𝑥 ⟩ , ⟨ 1 , 𝑥 ⟩ } ∨ 𝑒 = { ⟨ 1 , 𝑥 ⟩ , ⟨ 1 , ( ( 𝑥 + 𝐾 ) mod 𝑁 ) ⟩ } ) } )
4 eqid ⊢ ( 1 ..^ ( ⌈ ‘ ( 𝑁 / 2 ) ) ) = ( 1 ..^ ( ⌈ ‘ ( 𝑁 / 2 ) ) )
5 eqid ⊢ ( 0 ..^ 𝑁 ) = ( 0 ..^ 𝑁 )
6 4 5 gpgusgralem ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ ( 1 ..^ ( ⌈ ‘ ( 𝑁 / 2 ) ) ) ) → { 𝑒 ∈ 𝒫 ( { 0 , 1 } × ( 0 ..^ 𝑁 ) ) ∣ ∃ 𝑥 ∈ ( 0 ..^ 𝑁 ) ( 𝑒 = { ⟨ 0 , 𝑥 ⟩ , ⟨ 0 , ( ( 𝑥 + 1 ) mod 𝑁 ) ⟩ } ∨ 𝑒 = { ⟨ 0 , 𝑥 ⟩ , ⟨ 1 , 𝑥 ⟩ } ∨ 𝑒 = { ⟨ 1 , 𝑥 ⟩ , ⟨ 1 , ( ( 𝑥 + 𝐾 ) mod 𝑁 ) ⟩ } ) } ⊆ { 𝑝 ∈ 𝒫 ( { 0 , 1 } × ( 0 ..^ 𝑁 ) ) ∣ ( ♯ ‘ 𝑝 ) = 2 } )
7 f1ss ⊢ ( ( ( I ↾ { 𝑒 ∈ 𝒫 ( { 0 , 1 } × ( 0 ..^ 𝑁 ) ) ∣ ∃ 𝑥 ∈ ( 0 ..^ 𝑁 ) ( 𝑒 = { ⟨ 0 , 𝑥 ⟩ , ⟨ 0 , ( ( 𝑥 + 1 ) mod 𝑁 ) ⟩ } ∨ 𝑒 = { ⟨ 0 , 𝑥 ⟩ , ⟨ 1 , 𝑥 ⟩ } ∨ 𝑒 = { ⟨ 1 , 𝑥 ⟩ , ⟨ 1 , ( ( 𝑥 + 𝐾 ) mod 𝑁 ) ⟩ } ) } ) : { 𝑒 ∈ 𝒫 ( { 0 , 1 } × ( 0 ..^ 𝑁 ) ) ∣ ∃ 𝑥 ∈ ( 0 ..^ 𝑁 ) ( 𝑒 = { ⟨ 0 , 𝑥 ⟩ , ⟨ 0 , ( ( 𝑥 + 1 ) mod 𝑁 ) ⟩ } ∨ 𝑒 = { ⟨ 0 , 𝑥 ⟩ , ⟨ 1 , 𝑥 ⟩ } ∨ 𝑒 = { ⟨ 1 , 𝑥 ⟩ , ⟨ 1 , ( ( 𝑥 + 𝐾 ) mod 𝑁 ) ⟩ } ) } –1-1→ { 𝑒 ∈ 𝒫 ( { 0 , 1 } × ( 0 ..^ 𝑁 ) ) ∣ ∃ 𝑥 ∈ ( 0 ..^ 𝑁 ) ( 𝑒 = { ⟨ 0 , 𝑥 ⟩ , ⟨ 0 , ( ( 𝑥 + 1 ) mod 𝑁 ) ⟩ } ∨ 𝑒 = { ⟨ 0 , 𝑥 ⟩ , ⟨ 1 , 𝑥 ⟩ } ∨ 𝑒 = { ⟨ 1 , 𝑥 ⟩ , ⟨ 1 , ( ( 𝑥 + 𝐾 ) mod 𝑁 ) ⟩ } ) } ∧ { 𝑒 ∈ 𝒫 ( { 0 , 1 } × ( 0 ..^ 𝑁 ) ) ∣ ∃ 𝑥 ∈ ( 0 ..^ 𝑁 ) ( 𝑒 = { ⟨ 0 , 𝑥 ⟩ , ⟨ 0 , ( ( 𝑥 + 1 ) mod 𝑁 ) ⟩ } ∨ 𝑒 = { ⟨ 0 , 𝑥 ⟩ , ⟨ 1 , 𝑥 ⟩ } ∨ 𝑒 = { ⟨ 1 , 𝑥 ⟩ , ⟨ 1 , ( ( 𝑥 + 𝐾 ) mod 𝑁 ) ⟩ } ) } ⊆ { 𝑝 ∈ 𝒫 ( { 0 , 1 } × ( 0 ..^ 𝑁 ) ) ∣ ( ♯ ‘ 𝑝 ) = 2 } ) → ( I ↾ { 𝑒 ∈ 𝒫 ( { 0 , 1 } × ( 0 ..^ 𝑁 ) ) ∣ ∃ 𝑥 ∈ ( 0 ..^ 𝑁 ) ( 𝑒 = { ⟨ 0 , 𝑥 ⟩ , ⟨ 0 , ( ( 𝑥 + 1 ) mod 𝑁 ) ⟩ } ∨ 𝑒 = { ⟨ 0 , 𝑥 ⟩ , ⟨ 1 , 𝑥 ⟩ } ∨ 𝑒 = { ⟨ 1 , 𝑥 ⟩ , ⟨ 1 , ( ( 𝑥 + 𝐾 ) mod 𝑁 ) ⟩ } ) } ) : { 𝑒 ∈ 𝒫 ( { 0 , 1 } × ( 0 ..^ 𝑁 ) ) ∣ ∃ 𝑥 ∈ ( 0 ..^ 𝑁 ) ( 𝑒 = { ⟨ 0 , 𝑥 ⟩ , ⟨ 0 , ( ( 𝑥 + 1 ) mod 𝑁 ) ⟩ } ∨ 𝑒 = { ⟨ 0 , 𝑥 ⟩ , ⟨ 1 , 𝑥 ⟩ } ∨ 𝑒 = { ⟨ 1 , 𝑥 ⟩ , ⟨ 1 , ( ( 𝑥 + 𝐾 ) mod 𝑁 ) ⟩ } ) } –1-1→ { 𝑝 ∈ 𝒫 ( { 0 , 1 } × ( 0 ..^ 𝑁 ) ) ∣ ( ♯ ‘ 𝑝 ) = 2 } )
8 3 6 7 syl2anc ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ ( 1 ..^ ( ⌈ ‘ ( 𝑁 / 2 ) ) ) ) → ( I ↾ { 𝑒 ∈ 𝒫 ( { 0 , 1 } × ( 0 ..^ 𝑁 ) ) ∣ ∃ 𝑥 ∈ ( 0 ..^ 𝑁 ) ( 𝑒 = { ⟨ 0 , 𝑥 ⟩ , ⟨ 0 , ( ( 𝑥 + 1 ) mod 𝑁 ) ⟩ } ∨ 𝑒 = { ⟨ 0 , 𝑥 ⟩ , ⟨ 1 , 𝑥 ⟩ } ∨ 𝑒 = { ⟨ 1 , 𝑥 ⟩ , ⟨ 1 , ( ( 𝑥 + 𝐾 ) mod 𝑁 ) ⟩ } ) } ) : { 𝑒 ∈ 𝒫 ( { 0 , 1 } × ( 0 ..^ 𝑁 ) ) ∣ ∃ 𝑥 ∈ ( 0 ..^ 𝑁 ) ( 𝑒 = { ⟨ 0 , 𝑥 ⟩ , ⟨ 0 , ( ( 𝑥 + 1 ) mod 𝑁 ) ⟩ } ∨ 𝑒 = { ⟨ 0 , 𝑥 ⟩ , ⟨ 1 , 𝑥 ⟩ } ∨ 𝑒 = { ⟨ 1 , 𝑥 ⟩ , ⟨ 1 , ( ( 𝑥 + 𝐾 ) mod 𝑁 ) ⟩ } ) } –1-1→ { 𝑝 ∈ 𝒫 ( { 0 , 1 } × ( 0 ..^ 𝑁 ) ) ∣ ( ♯ ‘ 𝑝 ) = 2 } )
9 eluz3nn ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → 𝑁 ∈ ℕ )
10 4 5 gpgiedg ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐾 ∈ ( 1 ..^ ( ⌈ ‘ ( 𝑁 / 2 ) ) ) ) → ( iEdg ‘ ( 𝑁 gPetersenGr 𝐾 ) ) = ( I ↾ { 𝑒 ∈ 𝒫 ( { 0 , 1 } × ( 0 ..^ 𝑁 ) ) ∣ ∃ 𝑥 ∈ ( 0 ..^ 𝑁 ) ( 𝑒 = { ⟨ 0 , 𝑥 ⟩ , ⟨ 0 , ( ( 𝑥 + 1 ) mod 𝑁 ) ⟩ } ∨ 𝑒 = { ⟨ 0 , 𝑥 ⟩ , ⟨ 1 , 𝑥 ⟩ } ∨ 𝑒 = { ⟨ 1 , 𝑥 ⟩ , ⟨ 1 , ( ( 𝑥 + 𝐾 ) mod 𝑁 ) ⟩ } ) } ) )
11 9 10 sylan ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ ( 1 ..^ ( ⌈ ‘ ( 𝑁 / 2 ) ) ) ) → ( iEdg ‘ ( 𝑁 gPetersenGr 𝐾 ) ) = ( I ↾ { 𝑒 ∈ 𝒫 ( { 0 , 1 } × ( 0 ..^ 𝑁 ) ) ∣ ∃ 𝑥 ∈ ( 0 ..^ 𝑁 ) ( 𝑒 = { ⟨ 0 , 𝑥 ⟩ , ⟨ 0 , ( ( 𝑥 + 1 ) mod 𝑁 ) ⟩ } ∨ 𝑒 = { ⟨ 0 , 𝑥 ⟩ , ⟨ 1 , 𝑥 ⟩ } ∨ 𝑒 = { ⟨ 1 , 𝑥 ⟩ , ⟨ 1 , ( ( 𝑥 + 𝐾 ) mod 𝑁 ) ⟩ } ) } ) )
12 11 dmeqd ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ ( 1 ..^ ( ⌈ ‘ ( 𝑁 / 2 ) ) ) ) → dom ( iEdg ‘ ( 𝑁 gPetersenGr 𝐾 ) ) = dom ( I ↾ { 𝑒 ∈ 𝒫 ( { 0 , 1 } × ( 0 ..^ 𝑁 ) ) ∣ ∃ 𝑥 ∈ ( 0 ..^ 𝑁 ) ( 𝑒 = { ⟨ 0 , 𝑥 ⟩ , ⟨ 0 , ( ( 𝑥 + 1 ) mod 𝑁 ) ⟩ } ∨ 𝑒 = { ⟨ 0 , 𝑥 ⟩ , ⟨ 1 , 𝑥 ⟩ } ∨ 𝑒 = { ⟨ 1 , 𝑥 ⟩ , ⟨ 1 , ( ( 𝑥 + 𝐾 ) mod 𝑁 ) ⟩ } ) } ) )
13 dmresi ⊢ dom ( I ↾ { 𝑒 ∈ 𝒫 ( { 0 , 1 } × ( 0 ..^ 𝑁 ) ) ∣ ∃ 𝑥 ∈ ( 0 ..^ 𝑁 ) ( 𝑒 = { ⟨ 0 , 𝑥 ⟩ , ⟨ 0 , ( ( 𝑥 + 1 ) mod 𝑁 ) ⟩ } ∨ 𝑒 = { ⟨ 0 , 𝑥 ⟩ , ⟨ 1 , 𝑥 ⟩ } ∨ 𝑒 = { ⟨ 1 , 𝑥 ⟩ , ⟨ 1 , ( ( 𝑥 + 𝐾 ) mod 𝑁 ) ⟩ } ) } ) = { 𝑒 ∈ 𝒫 ( { 0 , 1 } × ( 0 ..^ 𝑁 ) ) ∣ ∃ 𝑥 ∈ ( 0 ..^ 𝑁 ) ( 𝑒 = { ⟨ 0 , 𝑥 ⟩ , ⟨ 0 , ( ( 𝑥 + 1 ) mod 𝑁 ) ⟩ } ∨ 𝑒 = { ⟨ 0 , 𝑥 ⟩ , ⟨ 1 , 𝑥 ⟩ } ∨ 𝑒 = { ⟨ 1 , 𝑥 ⟩ , ⟨ 1 , ( ( 𝑥 + 𝐾 ) mod 𝑁 ) ⟩ } ) }
14 12 13 eqtrdi ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ ( 1 ..^ ( ⌈ ‘ ( 𝑁 / 2 ) ) ) ) → dom ( iEdg ‘ ( 𝑁 gPetersenGr 𝐾 ) ) = { 𝑒 ∈ 𝒫 ( { 0 , 1 } × ( 0 ..^ 𝑁 ) ) ∣ ∃ 𝑥 ∈ ( 0 ..^ 𝑁 ) ( 𝑒 = { ⟨ 0 , 𝑥 ⟩ , ⟨ 0 , ( ( 𝑥 + 1 ) mod 𝑁 ) ⟩ } ∨ 𝑒 = { ⟨ 0 , 𝑥 ⟩ , ⟨ 1 , 𝑥 ⟩ } ∨ 𝑒 = { ⟨ 1 , 𝑥 ⟩ , ⟨ 1 , ( ( 𝑥 + 𝐾 ) mod 𝑁 ) ⟩ } ) } )
15 4 5 gpgvtx ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐾 ∈ ( 1 ..^ ( ⌈ ‘ ( 𝑁 / 2 ) ) ) ) → ( Vtx ‘ ( 𝑁 gPetersenGr 𝐾 ) ) = ( { 0 , 1 } × ( 0 ..^ 𝑁 ) ) )
16 9 15 sylan ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ ( 1 ..^ ( ⌈ ‘ ( 𝑁 / 2 ) ) ) ) → ( Vtx ‘ ( 𝑁 gPetersenGr 𝐾 ) ) = ( { 0 , 1 } × ( 0 ..^ 𝑁 ) ) )
17 16 pweqd ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ ( 1 ..^ ( ⌈ ‘ ( 𝑁 / 2 ) ) ) ) → 𝒫 ( Vtx ‘ ( 𝑁 gPetersenGr 𝐾 ) ) = 𝒫 ( { 0 , 1 } × ( 0 ..^ 𝑁 ) ) )
18 17 rabeqdv ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ ( 1 ..^ ( ⌈ ‘ ( 𝑁 / 2 ) ) ) ) → { 𝑝 ∈ 𝒫 ( Vtx ‘ ( 𝑁 gPetersenGr 𝐾 ) ) ∣ ( ♯ ‘ 𝑝 ) = 2 } = { 𝑝 ∈ 𝒫 ( { 0 , 1 } × ( 0 ..^ 𝑁 ) ) ∣ ( ♯ ‘ 𝑝 ) = 2 } )
19 11 14 18 f1eq123d ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ ( 1 ..^ ( ⌈ ‘ ( 𝑁 / 2 ) ) ) ) → ( ( iEdg ‘ ( 𝑁 gPetersenGr 𝐾 ) ) : dom ( iEdg ‘ ( 𝑁 gPetersenGr 𝐾 ) ) –1-1→ { 𝑝 ∈ 𝒫 ( Vtx ‘ ( 𝑁 gPetersenGr 𝐾 ) ) ∣ ( ♯ ‘ 𝑝 ) = 2 } ↔ ( I ↾ { 𝑒 ∈ 𝒫 ( { 0 , 1 } × ( 0 ..^ 𝑁 ) ) ∣ ∃ 𝑥 ∈ ( 0 ..^ 𝑁 ) ( 𝑒 = { ⟨ 0 , 𝑥 ⟩ , ⟨ 0 , ( ( 𝑥 + 1 ) mod 𝑁 ) ⟩ } ∨ 𝑒 = { ⟨ 0 , 𝑥 ⟩ , ⟨ 1 , 𝑥 ⟩ } ∨ 𝑒 = { ⟨ 1 , 𝑥 ⟩ , ⟨ 1 , ( ( 𝑥 + 𝐾 ) mod 𝑁 ) ⟩ } ) } ) : { 𝑒 ∈ 𝒫 ( { 0 , 1 } × ( 0 ..^ 𝑁 ) ) ∣ ∃ 𝑥 ∈ ( 0 ..^ 𝑁 ) ( 𝑒 = { ⟨ 0 , 𝑥 ⟩ , ⟨ 0 , ( ( 𝑥 + 1 ) mod 𝑁 ) ⟩ } ∨ 𝑒 = { ⟨ 0 , 𝑥 ⟩ , ⟨ 1 , 𝑥 ⟩ } ∨ 𝑒 = { ⟨ 1 , 𝑥 ⟩ , ⟨ 1 , ( ( 𝑥 + 𝐾 ) mod 𝑁 ) ⟩ } ) } –1-1→ { 𝑝 ∈ 𝒫 ( { 0 , 1 } × ( 0 ..^ 𝑁 ) ) ∣ ( ♯ ‘ 𝑝 ) = 2 } ) )
20 8 19 mpbird ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ ( 1 ..^ ( ⌈ ‘ ( 𝑁 / 2 ) ) ) ) → ( iEdg ‘ ( 𝑁 gPetersenGr 𝐾 ) ) : dom ( iEdg ‘ ( 𝑁 gPetersenGr 𝐾 ) ) –1-1→ { 𝑝 ∈ 𝒫 ( Vtx ‘ ( 𝑁 gPetersenGr 𝐾 ) ) ∣ ( ♯ ‘ 𝑝 ) = 2 } )
21 ovex ⊢ ( 𝑁 gPetersenGr 𝐾 ) ∈ V
22 eqid ⊢ ( Vtx ‘ ( 𝑁 gPetersenGr 𝐾 ) ) = ( Vtx ‘ ( 𝑁 gPetersenGr 𝐾 ) )
23 eqid ⊢ ( iEdg ‘ ( 𝑁 gPetersenGr 𝐾 ) ) = ( iEdg ‘ ( 𝑁 gPetersenGr 𝐾 ) )
24 22 23 isusgrs ⊢ ( ( 𝑁 gPetersenGr 𝐾 ) ∈ V → ( ( 𝑁 gPetersenGr 𝐾 ) ∈ USGraph ↔ ( iEdg ‘ ( 𝑁 gPetersenGr 𝐾 ) ) : dom ( iEdg ‘ ( 𝑁 gPetersenGr 𝐾 ) ) –1-1→ { 𝑝 ∈ 𝒫 ( Vtx ‘ ( 𝑁 gPetersenGr 𝐾 ) ) ∣ ( ♯ ‘ 𝑝 ) = 2 } ) )
25 21 24 mp1i ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ ( 1 ..^ ( ⌈ ‘ ( 𝑁 / 2 ) ) ) ) → ( ( 𝑁 gPetersenGr 𝐾 ) ∈ USGraph ↔ ( iEdg ‘ ( 𝑁 gPetersenGr 𝐾 ) ) : dom ( iEdg ‘ ( 𝑁 gPetersenGr 𝐾 ) ) –1-1→ { 𝑝 ∈ 𝒫 ( Vtx ‘ ( 𝑁 gPetersenGr 𝐾 ) ) ∣ ( ♯ ‘ 𝑝 ) = 2 } ) )
26 20 25 mpbird ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝐾 ∈ ( 1 ..^ ( ⌈ ‘ ( 𝑁 / 2 ) ) ) ) → ( 𝑁 gPetersenGr 𝐾 ) ∈ USGraph )