Metamath Proof Explorer

Theorem stgredg

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

Ref Expression
Assertion stgredg 
|- ( N e. NN0 -> ( Edg ` ( StarGr ` N ) ) = { e e. ~P ( 0 ... N ) | E. x e. ( 1 ... N ) e = { 0 , x } } )

Proof

Step Hyp Ref Expression
1 edgval 
 |-  ( Edg ` ( StarGr ` N ) ) = ran ( iEdg ` ( StarGr ` N ) )
2 stgriedg 
 |-  ( N e. NN0 -> ( iEdg ` ( StarGr ` N ) ) = ( _I |` { e e. ~P ( 0 ... N ) | E. x e. ( 1 ... N ) e = { 0 , x } } ) )
3 2 rneqd 
 |-  ( N e. NN0 -> ran ( iEdg ` ( StarGr ` N ) ) = ran ( _I |` { e e. ~P ( 0 ... N ) | E. x e. ( 1 ... N ) e = { 0 , x } } ) )
4 rnresi 
 |-  ran ( _I |` { 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 3 4 eqtrdi 
 |-  ( N e. NN0 -> ran ( iEdg ` ( StarGr ` N ) ) = { e e. ~P ( 0 ... N ) | E. x e. ( 1 ... N ) e = { 0 , x } } )
6 1 5 eqtrid 
 |-  ( N e. NN0 -> ( Edg ` ( StarGr ` N ) ) = { e e. ~P ( 0 ... N ) | E. x e. ( 1 ... N ) e = { 0 , x } } )