Theorem stgriedg

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

	Ref	Expression
Assertion	stgriedg	Could not format assertion : 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 |-

Proof

Step	Hyp	Ref	Expression
1		stgrfv	Could not format ( 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 } } ) >. } ) : No typesetting found for |- ( 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 } } ) >. } ) with typecode |-
2	1	fveq2d	Could not format ( N e. NN0 -> ( iEdg ` ( StarGr ` N ) ) = ( iEdg ` { <. ( Base ` ndx ) , ( 0 ... N ) >. , <. ( .ef ` ndx ) , ( _I |` { e e. ~P ( 0 ... N ) | E. x e. ( 1 ... N ) e = { 0 , x } } ) >. } ) ) : No typesetting found for |- ( N e. NN0 -> ( iEdg ` ( StarGr ` N ) ) = ( iEdg ` { <. ( Base ` ndx ) , ( 0 ... N ) >. , <. ( .ef ` ndx ) , ( _I |` { e e. ~P ( 0 ... N ) | E. x e. ( 1 ... N ) e = { 0 , x } } ) >. } ) ) with typecode |-
3		ovex	$$⊢\left(0\dots N\right)\in \mathrm{V}$$
4		eqid	$$⊢\left\{e\in 𝒫\left(0\dots N\right)|\exists x\in \left(1\dots N\right)e=\left\{0,x\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		pwexg	$$⊢\left(0\dots N\right)\in \mathrm{V}\to 𝒫\left(0\dots N\right)\in \mathrm{V}$$
6	4 5	rabexd	$$⊢\left(0\dots N\right)\in \mathrm{V}\to \left\{e\in 𝒫\left(0\dots N\right)|\exists x\in \left(1\dots N\right)e=\left\{0,x\right\}\right\}\in \mathrm{V}$$
7	6	resiexd	$$⊢\left(0\dots N\right)\in \mathrm{V}\to {\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\}}\in \mathrm{V}$$
8	3 7	ax-mp	$$⊢{\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\}}\in \mathrm{V}$$
9	3 8	pm3.2i	$$⊢\left(\left(0\dots N\right)\in \mathrm{V}\wedge {\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\}}\in \mathrm{V}\right)$$
10		eqid	$$⊢\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},\left(0\dots N\right)⟩,⟨\mathrm{ef}\left(\mathrm{ndx}\right),{\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\{⟨{\mathrm{Base}}_{\mathrm{ndx}},\left(0\dots N\right)⟩,⟨\mathrm{ef}\left(\mathrm{ndx}\right),{\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\}$$
11	10	struct2griedg	$$⊢\left(\left(0\dots N\right)\in \mathrm{V}\wedge {\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\}}\in \mathrm{V}\right)\to \mathrm{iEdg}\left(\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},\left(0\dots N\right)⟩,⟨\mathrm{ef}\left(\mathrm{ndx}\right),{\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\}\right)={\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\}}$$
12	9 11	mp1i	$$⊢N\in {\mathbb{N}}_0\to \mathrm{iEdg}\left(\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},\left(0\dots N\right)⟩,⟨\mathrm{ef}\left(\mathrm{ndx}\right),{\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\}\right)={\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\}}$$
13	2 12	eqtrd	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 |-