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	$$⊢\mathrm{ran}\left({\mathrm{I}\upharpoonright }_{\left\{e\in 𝒫\left(0\dots N\right)|\exists x\in \left(1\dots N\right)e=\left\{0,x\right\}\right\}}\right)=\left\{e\in 𝒫\left(0\dots N\right)|\exists x\in \left(1\dots N\right)e=\left\{0,x\right\}\right\}$$
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 |-