Theorem stgrfv

Description: The star graph S_N. (Contributed by AV, 10-Sep-2025)

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

Proof

Step	Hyp	Ref	Expression
1		df-stgr	Could not format StarGr = ( n e. NN0 |-> { <. ( Base ` ndx ) , ( 0 ... n ) >. , <. ( .ef ` ndx ) , ( _I |` { e e. ~P ( 0 ... n ) | E. x e. ( 1 ... n ) e = { 0 , x } } ) >. } ) : No typesetting found for |- StarGr = ( n e. NN0 |-> { <. ( Base ` ndx ) , ( 0 ... n ) >. , <. ( .ef ` ndx ) , ( _I |` { e e. ~P ( 0 ... n ) | E. x e. ( 1 ... n ) e = { 0 , x } } ) >. } ) with typecode |-
2	1	a1i	Could not format ( N e. NN0 -> StarGr = ( n e. NN0 |-> { <. ( 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 e. NN0 |-> { <. ( Base ` ndx ) , ( 0 ... n ) >. , <. ( .ef ` ndx ) , ( _I |` { e e. ~P ( 0 ... n ) | E. x e. ( 1 ... n ) e = { 0 , x } } ) >. } ) ) with typecode |-
3		oveq2	$$⊢n=N\to \left(0\dots n\right)=\left(0\dots N\right)$$
4	3	opeq2d	$$⊢n=N\to ⟨{\mathrm{Base}}_{\mathrm{ndx}},\left(0\dots n\right)⟩=⟨{\mathrm{Base}}_{\mathrm{ndx}},\left(0\dots N\right)⟩$$
5	3	pweqd	$$⊢n=N\to 𝒫\left(0\dots n\right)=𝒫\left(0\dots N\right)$$
6		oveq2	$$⊢n=N\to \left(1\dots n\right)=\left(1\dots N\right)$$
7	6	rexeqdv	$$⊢n=N\to \left(\exists x\in \left(1\dots n\right)e=\left\{0,x\right\}\leftrightarrow \exists x\in \left(1\dots N\right)e=\left\{0,x\right\}\right)$$
8	5 7	rabeqbidv	$$⊢n=N\to \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\}$$
9	8	reseq2d	$$⊢n=N\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\}}={\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\}}$$
10	9	opeq2d	$$⊢n=N\to ⟨\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\}}⟩=⟨\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\}}⟩$$
11	4 10	preq12d	$$⊢n=N\to \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\}$$
12	11	adantl	$$⊢\left(N\in {\mathbb{N}}_0\wedge n=N\right)\to \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\}$$
13		id	$$⊢N\in {\mathbb{N}}_0\to N\in {\mathbb{N}}_0$$
14		prex	$$⊢\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\}\in \mathrm{V}$$
15	14	a1i	$$⊢N\in {\mathbb{N}}_0\to \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\}\in \mathrm{V}$$
16	2 12 13 15	fvmptd	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 |-