Theorem stgrvtx

Description: The vertices of the star graph S_N. (Contributed by AV, 11-Sep-2025)

	Ref	Expression
Assertion	stgrvtx	⊢ ( 𝑁 ∈ ℕ0 → ( Vtx ‘ ( StarGr ‘ 𝑁 ) ) = ( 0 ... 𝑁 ) )

Proof

Step	Hyp	Ref	Expression
1		stgrfv	⊢ ( 𝑁 ∈ ℕ0 → ( StarGr ‘ 𝑁 ) = { ⟨ ( Base ‘ ndx ) , ( 0 ... 𝑁 ) ⟩ , ⟨ ( .ef ‘ ndx ) , ( I ↾ { 𝑒 ∈ 𝒫 ( 0 ... 𝑁 ) ∣ ∃ 𝑥 ∈ ( 1 ... 𝑁 ) 𝑒 = { 0 , 𝑥 } } ) ⟩ } )
2	1	fveq2d	⊢ ( 𝑁 ∈ ℕ0 → ( Vtx ‘ ( StarGr ‘ 𝑁 ) ) = ( Vtx ‘ { ⟨ ( Base ‘ ndx ) , ( 0 ... 𝑁 ) ⟩ , ⟨ ( .ef ‘ ndx ) , ( I ↾ { 𝑒 ∈ 𝒫 ( 0 ... 𝑁 ) ∣ ∃ 𝑥 ∈ ( 1 ... 𝑁 ) 𝑒 = { 0 , 𝑥 } } ) ⟩ } ) )
3		ovex	⊢ ( 0 ... 𝑁 ) ∈ V
4		eqid	⊢ { 𝑒 ∈ 𝒫 ( 0 ... 𝑁 ) ∣ ∃ 𝑥 ∈ ( 1 ... 𝑁 ) 𝑒 = { 0 , 𝑥 } } = { 𝑒 ∈ 𝒫 ( 0 ... 𝑁 ) ∣ ∃ 𝑥 ∈ ( 1 ... 𝑁 ) 𝑒 = { 0 , 𝑥 } }
5		pwexg	⊢ ( ( 0 ... 𝑁 ) ∈ V → 𝒫 ( 0 ... 𝑁 ) ∈ V )
6	4 5	rabexd	⊢ ( ( 0 ... 𝑁 ) ∈ V → { 𝑒 ∈ 𝒫 ( 0 ... 𝑁 ) ∣ ∃ 𝑥 ∈ ( 1 ... 𝑁 ) 𝑒 = { 0 , 𝑥 } } ∈ V )
7	6	resiexd	⊢ ( ( 0 ... 𝑁 ) ∈ V → ( I ↾ { 𝑒 ∈ 𝒫 ( 0 ... 𝑁 ) ∣ ∃ 𝑥 ∈ ( 1 ... 𝑁 ) 𝑒 = { 0 , 𝑥 } } ) ∈ V )
8	3 7	ax-mp	⊢ ( I ↾ { 𝑒 ∈ 𝒫 ( 0 ... 𝑁 ) ∣ ∃ 𝑥 ∈ ( 1 ... 𝑁 ) 𝑒 = { 0 , 𝑥 } } ) ∈ V
9	3 8	pm3.2i	⊢ ( ( 0 ... 𝑁 ) ∈ V ∧ ( I ↾ { 𝑒 ∈ 𝒫 ( 0 ... 𝑁 ) ∣ ∃ 𝑥 ∈ ( 1 ... 𝑁 ) 𝑒 = { 0 , 𝑥 } } ) ∈ V )
10		eqid	⊢ { ⟨ ( Base ‘ ndx ) , ( 0 ... 𝑁 ) ⟩ , ⟨ ( .ef ‘ ndx ) , ( I ↾ { 𝑒 ∈ 𝒫 ( 0 ... 𝑁 ) ∣ ∃ 𝑥 ∈ ( 1 ... 𝑁 ) 𝑒 = { 0 , 𝑥 } } ) ⟩ } = { ⟨ ( Base ‘ ndx ) , ( 0 ... 𝑁 ) ⟩ , ⟨ ( .ef ‘ ndx ) , ( I ↾ { 𝑒 ∈ 𝒫 ( 0 ... 𝑁 ) ∣ ∃ 𝑥 ∈ ( 1 ... 𝑁 ) 𝑒 = { 0 , 𝑥 } } ) ⟩ }
11	10	struct2grvtx	⊢ ( ( ( 0 ... 𝑁 ) ∈ V ∧ ( I ↾ { 𝑒 ∈ 𝒫 ( 0 ... 𝑁 ) ∣ ∃ 𝑥 ∈ ( 1 ... 𝑁 ) 𝑒 = { 0 , 𝑥 } } ) ∈ V ) → ( Vtx ‘ { ⟨ ( Base ‘ ndx ) , ( 0 ... 𝑁 ) ⟩ , ⟨ ( .ef ‘ ndx ) , ( I ↾ { 𝑒 ∈ 𝒫 ( 0 ... 𝑁 ) ∣ ∃ 𝑥 ∈ ( 1 ... 𝑁 ) 𝑒 = { 0 , 𝑥 } } ) ⟩ } ) = ( 0 ... 𝑁 ) )
12	9 11	mp1i	⊢ ( 𝑁 ∈ ℕ0 → ( Vtx ‘ { ⟨ ( Base ‘ ndx ) , ( 0 ... 𝑁 ) ⟩ , ⟨ ( .ef ‘ ndx ) , ( I ↾ { 𝑒 ∈ 𝒫 ( 0 ... 𝑁 ) ∣ ∃ 𝑥 ∈ ( 1 ... 𝑁 ) 𝑒 = { 0 , 𝑥 } } ) ⟩ } ) = ( 0 ... 𝑁 ) )
13	2 12	eqtrd	⊢ ( 𝑁 ∈ ℕ0 → ( Vtx ‘ ( StarGr ‘ 𝑁 ) ) = ( 0 ... 𝑁 ) )