Theorem stgr0

Description: The star graph S_0 consists of a single vertex without edges. (Contributed by AV, 11-Sep-2025)

	Ref	Expression
Assertion	stgr0	Could not format assertion : No typesetting found for |- ( StarGr ` 0 ) = { <. ( Base ` ndx ) , { 0 } >. , <. ( .ef ` ndx ) , (/) >. } with typecode |-

Proof

Step	Hyp	Ref	Expression
1		0nn0	$$⊢0\in {\mathbb{N}}_0$$
2		stgrfv	Could not format ( 0 e. NN0 -> ( StarGr ` 0 ) = { <. ( Base ` ndx ) , ( 0 ... 0 ) >. , <. ( .ef ` ndx ) , ( _I |` { e e. ~P ( 0 ... 0 ) | E. x e. ( 1 ... 0 ) e = { 0 , x } } ) >. } ) : No typesetting found for |- ( 0 e. NN0 -> ( StarGr ` 0 ) = { <. ( Base ` ndx ) , ( 0 ... 0 ) >. , <. ( .ef ` ndx ) , ( _I |` { e e. ~P ( 0 ... 0 ) | E. x e. ( 1 ... 0 ) e = { 0 , x } } ) >. } ) with typecode |-
3	1 2	ax-mp	Could not format ( StarGr ` 0 ) = { <. ( Base ` ndx ) , ( 0 ... 0 ) >. , <. ( .ef ` ndx ) , ( _I |` { e e. ~P ( 0 ... 0 ) | E. x e. ( 1 ... 0 ) e = { 0 , x } } ) >. } : No typesetting found for |- ( StarGr ` 0 ) = { <. ( Base ` ndx ) , ( 0 ... 0 ) >. , <. ( .ef ` ndx ) , ( _I |` { e e. ~P ( 0 ... 0 ) | E. x e. ( 1 ... 0 ) e = { 0 , x } } ) >. } with typecode |-
4		fz0sn	$$⊢\left(0\dots 0\right)=\left\{0\right\}$$
5	4	opeq2i	$$⊢⟨{\mathrm{Base}}_{\mathrm{ndx}},\left(0\dots 0\right)⟩=⟨{\mathrm{Base}}_{\mathrm{ndx}},\left\{0\right\}⟩$$
6		rabeq0	$$⊢\left\{e\in 𝒫\left(0\dots 0\right)|\exists x\in \left(1\dots 0\right)e=\left\{0,x\right\}\right\}=\varnothing \leftrightarrow \forall e\in 𝒫\left(0\dots 0\right)\neg \exists x\in \left(1\dots 0\right)e=\left\{0,x\right\}$$
7		noel	$$⊢\neg x\in \varnothing$$
8	7	pm2.21i	$$⊢x\in \varnothing \to \neg e=\left\{0,x\right\}$$
9		fz10	$$⊢\left(1\dots 0\right)=\varnothing$$
10	8 9	eleq2s	$$⊢x\in \left(1\dots 0\right)\to \neg e=\left\{0,x\right\}$$
11	10	a1i	$$⊢e\in 𝒫\left(0\dots 0\right)\to \left(x\in \left(1\dots 0\right)\to \neg e=\left\{0,x\right\}\right)$$
12	11	ralrimiv	$$⊢e\in 𝒫\left(0\dots 0\right)\to \forall x\in \left(1\dots 0\right)\neg e=\left\{0,x\right\}$$
13		ralnex	$$⊢\forall x\in \left(1\dots 0\right)\neg e=\left\{0,x\right\}\leftrightarrow \neg \exists x\in \left(1\dots 0\right)e=\left\{0,x\right\}$$
14	12 13	sylib	$$⊢e\in 𝒫\left(0\dots 0\right)\to \neg \exists x\in \left(1\dots 0\right)e=\left\{0,x\right\}$$
15	6 14	mprgbir	$$⊢\left\{e\in 𝒫\left(0\dots 0\right)|\exists x\in \left(1\dots 0\right)e=\left\{0,x\right\}\right\}=\varnothing$$
16	15	reseq2i	$$⊢{\mathrm{I}\upharpoonright }_{\left\{e\in 𝒫\left(0\dots 0\right)|\exists x\in \left(1\dots 0\right)e=\left\{0,x\right\}\right\}}={\mathrm{I}\upharpoonright }_{\varnothing }$$
17		res0	$$⊢{\mathrm{I}\upharpoonright }_{\varnothing }=\varnothing$$
18	16 17	eqtri	$$⊢{\mathrm{I}\upharpoonright }_{\left\{e\in 𝒫\left(0\dots 0\right)|\exists x\in \left(1\dots 0\right)e=\left\{0,x\right\}\right\}}=\varnothing$$
19	18	opeq2i	$$⊢⟨\mathrm{ef}\left(\mathrm{ndx}\right),{\mathrm{I}\upharpoonright }_{\left\{e\in 𝒫\left(0\dots 0\right)|\exists x\in \left(1\dots 0\right)e=\left\{0,x\right\}\right\}}⟩=⟨\mathrm{ef}\left(\mathrm{ndx}\right),\varnothing ⟩$$
20	5 19	preq12i	$$⊢\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},\left(0\dots 0\right)⟩,⟨\mathrm{ef}\left(\mathrm{ndx}\right),{\mathrm{I}\upharpoonright }_{\left\{e\in 𝒫\left(0\dots 0\right)|\exists x\in \left(1\dots 0\right)e=\left\{0,x\right\}\right\}}⟩\right\}=\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},\left\{0\right\}⟩,⟨\mathrm{ef}\left(\mathrm{ndx}\right),\varnothing ⟩\right\}$$
21	3 20	eqtri	Could not format ( StarGr ` 0 ) = { <. ( Base ` ndx ) , { 0 } >. , <. ( .ef ` ndx ) , (/) >. } : No typesetting found for |- ( StarGr ` 0 ) = { <. ( Base ` ndx ) , { 0 } >. , <. ( .ef ` ndx ) , (/) >. } with typecode |-