Metamath Proof Explorer


Theorem stgredg

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

Ref Expression
Assertion stgredg Could not format assertion : No typesetting found for |- ( N e. NN0 -> ( Edg ` ( StarGr ` N ) ) = { e e. ~P ( 0 ... N ) | E. x e. ( 1 ... N ) e = { 0 , x } } ) with typecode |-

Proof

Step Hyp Ref Expression
1 edgval Could not format ( Edg ` ( StarGr ` N ) ) = ran ( iEdg ` ( StarGr ` N ) ) : No typesetting found for |- ( Edg ` ( StarGr ` N ) ) = ran ( iEdg ` ( StarGr ` N ) ) with typecode |-
2 stgriedg Could not format ( N e. NN0 -> ( iEdg ` ( StarGr ` N ) ) = ( _I |` { e e. ~P ( 0 ... N ) | E. x e. ( 1 ... N ) e = { 0 , x } } ) ) : No typesetting found for |- ( N e. NN0 -> ( iEdg ` ( StarGr ` N ) ) = ( _I |` { e e. ~P ( 0 ... N ) | E. x e. ( 1 ... N ) e = { 0 , x } } ) ) with typecode |-
3 2 rneqd Could not format ( N e. NN0 -> ran ( iEdg ` ( StarGr ` N ) ) = ran ( _I |` { e e. ~P ( 0 ... N ) | E. x e. ( 1 ... N ) e = { 0 , x } } ) ) : No typesetting found for |- ( N e. NN0 -> ran ( iEdg ` ( StarGr ` N ) ) = ran ( _I |` { e e. ~P ( 0 ... N ) | E. x e. ( 1 ... N ) e = { 0 , x } } ) ) with typecode |-
4 rnresi ran I e 𝒫 0 N | x 1 N e = 0 x = e 𝒫 0 N | x 1 N e = 0 x
5 3 4 eqtrdi Could not format ( N e. NN0 -> ran ( iEdg ` ( StarGr ` N ) ) = { e e. ~P ( 0 ... N ) | E. x e. ( 1 ... N ) e = { 0 , x } } ) : No typesetting found for |- ( N e. NN0 -> ran ( iEdg ` ( StarGr ` N ) ) = { e e. ~P ( 0 ... N ) | E. x e. ( 1 ... N ) e = { 0 , x } } ) with typecode |-
6 1 5 eqtrid Could not format ( N e. NN0 -> ( Edg ` ( StarGr ` N ) ) = { e e. ~P ( 0 ... N ) | E. x e. ( 1 ... N ) e = { 0 , x } } ) : No typesetting found for |- ( N e. NN0 -> ( Edg ` ( StarGr ` N ) ) = { e e. ~P ( 0 ... N ) | E. x e. ( 1 ... N ) e = { 0 , x } } ) with typecode |-