Metamath Proof Explorer

Theorem stgrvtx

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

Ref Expression
Assertion stgrvtx 
|- ( N e. NN0 -> ( Vtx ` ( StarGr ` N ) ) = ( 0 ... N ) )

Proof

Step Hyp Ref Expression
1 stgrfv 
 |-  ( N e. NN0 -> ( StarGr ` N ) = { <. ( Base ` ndx ) , ( 0 ... N ) >. , <. ( .ef ` ndx ) , ( _I |` { e e. ~P ( 0 ... N ) | E. x e. ( 1 ... N ) e = { 0 , x } } ) >. } )
2 1 fveq2d 
 |-  ( N e. NN0 -> ( Vtx ` ( StarGr ` N ) ) = ( Vtx ` { <. ( Base ` ndx ) , ( 0 ... N ) >. , <. ( .ef ` ndx ) , ( _I |` { e e. ~P ( 0 ... N ) | E. x e. ( 1 ... N ) e = { 0 , x } } ) >. } ) )
3 ovex 
 |-  ( 0 ... N ) e. _V
4 eqid 
 |-  { e e. ~P ( 0 ... N ) | E. x e. ( 1 ... N ) e = { 0 , x } } = { e e. ~P ( 0 ... N ) | E. x e. ( 1 ... N ) e = { 0 , x } }
5 pwexg 
 |-  ( ( 0 ... N ) e. _V -> ~P ( 0 ... N ) e. _V )
6 4 5 rabexd 
 |-  ( ( 0 ... N ) e. _V -> { e e. ~P ( 0 ... N ) | E. x e. ( 1 ... N ) e = { 0 , x } } e. _V )
7 6 resiexd 
 |-  ( ( 0 ... N ) e. _V -> ( _I |` { e e. ~P ( 0 ... N ) | E. x e. ( 1 ... N ) e = { 0 , x } } ) e. _V )
8 3 7 ax-mp 
 |-  ( _I |` { e e. ~P ( 0 ... N ) | E. x e. ( 1 ... N ) e = { 0 , x } } ) e. _V
9 3 8 pm3.2i 
 |-  ( ( 0 ... N ) e. _V /\ ( _I |` { e e. ~P ( 0 ... N ) | E. x e. ( 1 ... N ) e = { 0 , x } } ) e. _V )
10 eqid 
 |-  { <. ( Base ` ndx ) , ( 0 ... N ) >. , <. ( .ef ` ndx ) , ( _I |` { e e. ~P ( 0 ... N ) | E. x e. ( 1 ... N ) e = { 0 , x } } ) >. } = { <. ( Base ` ndx ) , ( 0 ... N ) >. , <. ( .ef ` ndx ) , ( _I |` { e e. ~P ( 0 ... N ) | E. x e. ( 1 ... N ) e = { 0 , x } } ) >. }
11 10 struct2grvtx 
 |-  ( ( ( 0 ... N ) e. _V /\ ( _I |` { e e. ~P ( 0 ... N ) | E. x e. ( 1 ... N ) e = { 0 , x } } ) e. _V ) -> ( Vtx ` { <. ( Base ` ndx ) , ( 0 ... N ) >. , <. ( .ef ` ndx ) , ( _I |` { e e. ~P ( 0 ... N ) | E. x e. ( 1 ... N ) e = { 0 , x } } ) >. } ) = ( 0 ... N ) )
12 9 11 mp1i 
 |-  ( N e. NN0 -> ( Vtx ` { <. ( Base ` ndx ) , ( 0 ... N ) >. , <. ( .ef ` ndx ) , ( _I |` { e e. ~P ( 0 ... N ) | E. x e. ( 1 ... N ) e = { 0 , x } } ) >. } ) = ( 0 ... N ) )
13 2 12 eqtrd 
 |-  ( N e. NN0 -> ( Vtx ` ( StarGr ` N ) ) = ( 0 ... N ) )