Theorem gpgvtx

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

	Ref	Expression
Hypotheses	gpgov.j	⊢ 𝐽 = ( 1 ..^ ( ⌈ ‘ ( 𝑁 / 2 ) ) )
	gpgov.i	⊢ 𝐼 = ( 0 ..^ 𝑁 )
Assertion	gpgvtx	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐾 ∈ 𝐽 ) → ( Vtx ‘ ( 𝑁 gPetersenGr 𝐾 ) ) = ( { 0 , 1 } × 𝐼 ) )

Proof

Step	Hyp	Ref	Expression
1		gpgov.j	⊢ 𝐽 = ( 1 ..^ ( ⌈ ‘ ( 𝑁 / 2 ) ) )
2		gpgov.i	⊢ 𝐼 = ( 0 ..^ 𝑁 )
3	1 2	gpgov	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐾 ∈ 𝐽 ) → ( 𝑁 gPetersenGr 𝐾 ) = { ⟨ ( Base ‘ ndx ) , ( { 0 , 1 } × 𝐼 ) ⟩ , ⟨ ( .ef ‘ ndx ) , ( I ↾ { 𝑒 ∈ 𝒫 ( { 0 , 1 } × 𝐼 ) ∣ ∃ 𝑥 ∈ 𝐼 ( 𝑒 = { ⟨ 0 , 𝑥 ⟩ , ⟨ 0 , ( ( 𝑥 + 1 ) mod 𝑁 ) ⟩ } ∨ 𝑒 = { ⟨ 0 , 𝑥 ⟩ , ⟨ 1 , 𝑥 ⟩ } ∨ 𝑒 = { ⟨ 1 , 𝑥 ⟩ , ⟨ 1 , ( ( 𝑥 + 𝐾 ) mod 𝑁 ) ⟩ } ) } ) ⟩ } )
4	3	fveq2d	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐾 ∈ 𝐽 ) → ( Vtx ‘ ( 𝑁 gPetersenGr 𝐾 ) ) = ( Vtx ‘ { ⟨ ( Base ‘ ndx ) , ( { 0 , 1 } × 𝐼 ) ⟩ , ⟨ ( .ef ‘ ndx ) , ( I ↾ { 𝑒 ∈ 𝒫 ( { 0 , 1 } × 𝐼 ) ∣ ∃ 𝑥 ∈ 𝐼 ( 𝑒 = { ⟨ 0 , 𝑥 ⟩ , ⟨ 0 , ( ( 𝑥 + 1 ) mod 𝑁 ) ⟩ } ∨ 𝑒 = { ⟨ 0 , 𝑥 ⟩ , ⟨ 1 , 𝑥 ⟩ } ∨ 𝑒 = { ⟨ 1 , 𝑥 ⟩ , ⟨ 1 , ( ( 𝑥 + 𝐾 ) mod 𝑁 ) ⟩ } ) } ) ⟩ } ) )
5		prex	⊢ { 0 , 1 } ∈ V
6	2	ovexi	⊢ 𝐼 ∈ V
7	5 6	xpex	⊢ ( { 0 , 1 } × 𝐼 ) ∈ V
8		eqid	⊢ { 𝑒 ∈ 𝒫 ( { 0 , 1 } × 𝐼 ) ∣ ∃ 𝑥 ∈ 𝐼 ( 𝑒 = { ⟨ 0 , 𝑥 ⟩ , ⟨ 0 , ( ( 𝑥 + 1 ) mod 𝑁 ) ⟩ } ∨ 𝑒 = { ⟨ 0 , 𝑥 ⟩ , ⟨ 1 , 𝑥 ⟩ } ∨ 𝑒 = { ⟨ 1 , 𝑥 ⟩ , ⟨ 1 , ( ( 𝑥 + 𝐾 ) mod 𝑁 ) ⟩ } ) } = { 𝑒 ∈ 𝒫 ( { 0 , 1 } × 𝐼 ) ∣ ∃ 𝑥 ∈ 𝐼 ( 𝑒 = { ⟨ 0 , 𝑥 ⟩ , ⟨ 0 , ( ( 𝑥 + 1 ) mod 𝑁 ) ⟩ } ∨ 𝑒 = { ⟨ 0 , 𝑥 ⟩ , ⟨ 1 , 𝑥 ⟩ } ∨ 𝑒 = { ⟨ 1 , 𝑥 ⟩ , ⟨ 1 , ( ( 𝑥 + 𝐾 ) mod 𝑁 ) ⟩ } ) }
9	5	a1i	⊢ ( 𝐼 = ( 0 ..^ 𝑁 ) → { 0 , 1 } ∈ V )
10		ovexd	⊢ ( 𝐼 = ( 0 ..^ 𝑁 ) → ( 0 ..^ 𝑁 ) ∈ V )
11	2 10	eqeltrid	⊢ ( 𝐼 = ( 0 ..^ 𝑁 ) → 𝐼 ∈ V )
12	9 11	xpexd	⊢ ( 𝐼 = ( 0 ..^ 𝑁 ) → ( { 0 , 1 } × 𝐼 ) ∈ V )
13	12	pwexd	⊢ ( 𝐼 = ( 0 ..^ 𝑁 ) → 𝒫 ( { 0 , 1 } × 𝐼 ) ∈ V )
14	8 13	rabexd	⊢ ( 𝐼 = ( 0 ..^ 𝑁 ) → { 𝑒 ∈ 𝒫 ( { 0 , 1 } × 𝐼 ) ∣ ∃ 𝑥 ∈ 𝐼 ( 𝑒 = { ⟨ 0 , 𝑥 ⟩ , ⟨ 0 , ( ( 𝑥 + 1 ) mod 𝑁 ) ⟩ } ∨ 𝑒 = { ⟨ 0 , 𝑥 ⟩ , ⟨ 1 , 𝑥 ⟩ } ∨ 𝑒 = { ⟨ 1 , 𝑥 ⟩ , ⟨ 1 , ( ( 𝑥 + 𝐾 ) mod 𝑁 ) ⟩ } ) } ∈ V )
15	14	resiexd	⊢ ( 𝐼 = ( 0 ..^ 𝑁 ) → ( I ↾ { 𝑒 ∈ 𝒫 ( { 0 , 1 } × 𝐼 ) ∣ ∃ 𝑥 ∈ 𝐼 ( 𝑒 = { ⟨ 0 , 𝑥 ⟩ , ⟨ 0 , ( ( 𝑥 + 1 ) mod 𝑁 ) ⟩ } ∨ 𝑒 = { ⟨ 0 , 𝑥 ⟩ , ⟨ 1 , 𝑥 ⟩ } ∨ 𝑒 = { ⟨ 1 , 𝑥 ⟩ , ⟨ 1 , ( ( 𝑥 + 𝐾 ) mod 𝑁 ) ⟩ } ) } ) ∈ V )
16	2 15	ax-mp	⊢ ( I ↾ { 𝑒 ∈ 𝒫 ( { 0 , 1 } × 𝐼 ) ∣ ∃ 𝑥 ∈ 𝐼 ( 𝑒 = { ⟨ 0 , 𝑥 ⟩ , ⟨ 0 , ( ( 𝑥 + 1 ) mod 𝑁 ) ⟩ } ∨ 𝑒 = { ⟨ 0 , 𝑥 ⟩ , ⟨ 1 , 𝑥 ⟩ } ∨ 𝑒 = { ⟨ 1 , 𝑥 ⟩ , ⟨ 1 , ( ( 𝑥 + 𝐾 ) mod 𝑁 ) ⟩ } ) } ) ∈ V
17	7 16	pm3.2i	⊢ ( ( { 0 , 1 } × 𝐼 ) ∈ V ∧ ( I ↾ { 𝑒 ∈ 𝒫 ( { 0 , 1 } × 𝐼 ) ∣ ∃ 𝑥 ∈ 𝐼 ( 𝑒 = { ⟨ 0 , 𝑥 ⟩ , ⟨ 0 , ( ( 𝑥 + 1 ) mod 𝑁 ) ⟩ } ∨ 𝑒 = { ⟨ 0 , 𝑥 ⟩ , ⟨ 1 , 𝑥 ⟩ } ∨ 𝑒 = { ⟨ 1 , 𝑥 ⟩ , ⟨ 1 , ( ( 𝑥 + 𝐾 ) mod 𝑁 ) ⟩ } ) } ) ∈ V )
18		eqid	⊢ { ⟨ ( Base ‘ ndx ) , ( { 0 , 1 } × 𝐼 ) ⟩ , ⟨ ( .ef ‘ ndx ) , ( I ↾ { 𝑒 ∈ 𝒫 ( { 0 , 1 } × 𝐼 ) ∣ ∃ 𝑥 ∈ 𝐼 ( 𝑒 = { ⟨ 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 𝑁 ) ⟩ } ) } ) ⟩ }
19	18	struct2grvtx	⊢ ( ( ( { 0 , 1 } × 𝐼 ) ∈ V ∧ ( I ↾ { 𝑒 ∈ 𝒫 ( { 0 , 1 } × 𝐼 ) ∣ ∃ 𝑥 ∈ 𝐼 ( 𝑒 = { ⟨ 0 , 𝑥 ⟩ , ⟨ 0 , ( ( 𝑥 + 1 ) mod 𝑁 ) ⟩ } ∨ 𝑒 = { ⟨ 0 , 𝑥 ⟩ , ⟨ 1 , 𝑥 ⟩ } ∨ 𝑒 = { ⟨ 1 , 𝑥 ⟩ , ⟨ 1 , ( ( 𝑥 + 𝐾 ) mod 𝑁 ) ⟩ } ) } ) ∈ V ) → ( Vtx ‘ { ⟨ ( Base ‘ ndx ) , ( { 0 , 1 } × 𝐼 ) ⟩ , ⟨ ( .ef ‘ ndx ) , ( I ↾ { 𝑒 ∈ 𝒫 ( { 0 , 1 } × 𝐼 ) ∣ ∃ 𝑥 ∈ 𝐼 ( 𝑒 = { ⟨ 0 , 𝑥 ⟩ , ⟨ 0 , ( ( 𝑥 + 1 ) mod 𝑁 ) ⟩ } ∨ 𝑒 = { ⟨ 0 , 𝑥 ⟩ , ⟨ 1 , 𝑥 ⟩ } ∨ 𝑒 = { ⟨ 1 , 𝑥 ⟩ , ⟨ 1 , ( ( 𝑥 + 𝐾 ) mod 𝑁 ) ⟩ } ) } ) ⟩ } ) = ( { 0 , 1 } × 𝐼 ) )
20	17 19	mp1i	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐾 ∈ 𝐽 ) → ( Vtx ‘ { ⟨ ( Base ‘ ndx ) , ( { 0 , 1 } × 𝐼 ) ⟩ , ⟨ ( .ef ‘ ndx ) , ( I ↾ { 𝑒 ∈ 𝒫 ( { 0 , 1 } × 𝐼 ) ∣ ∃ 𝑥 ∈ 𝐼 ( 𝑒 = { ⟨ 0 , 𝑥 ⟩ , ⟨ 0 , ( ( 𝑥 + 1 ) mod 𝑁 ) ⟩ } ∨ 𝑒 = { ⟨ 0 , 𝑥 ⟩ , ⟨ 1 , 𝑥 ⟩ } ∨ 𝑒 = { ⟨ 1 , 𝑥 ⟩ , ⟨ 1 , ( ( 𝑥 + 𝐾 ) mod 𝑁 ) ⟩ } ) } ) ⟩ } ) = ( { 0 , 1 } × 𝐼 ) )
21	4 20	eqtrd	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐾 ∈ 𝐽 ) → ( Vtx ‘ ( 𝑁 gPetersenGr 𝐾 ) ) = ( { 0 , 1 } × 𝐼 ) )