Definition df-stgr

Description: Definition of star graphs according to the first definition in Wikipedia, so that ( StarGrN ) has size N , and order N + 1 : ( StarGr0 ) will be a single vertex (graph without edges), see stgr0 , ( StarGr1 ) will be a single edge (graph with two vertices connected by an edge), see stgr1 , and ( StarGr3 ) will be a 3-star or "claw" (a star with 3 edges). (Contributed by AV, 10-Sep-2025)

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

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cstgr	Could not format StarGr : No typesetting found for class StarGr with typecode class
1		vn	$$setvarn$$
2		cn0	$$class{\mathbb{N}}_0$$
3		cbs	$$class\mathrm{Base}$$
4		cnx	$$class\mathrm{ndx}$$
5	4 3	cfv	$$class{\mathrm{Base}}_{\mathrm{ndx}}$$
6		cc0	$$class0$$
7		cfz	$$class\dots$$
8	1	cv	$$setvarn$$
9	6 8 7	co	$$class\left(0\dots n\right)$$
10	5 9	cop	$$class⟨{\mathrm{Base}}_{\mathrm{ndx}},\left(0\dots n\right)⟩$$
11		cedgf	$$class\mathrm{ef}$$
12	4 11	cfv	$$class\mathrm{ef}\left(\mathrm{ndx}\right)$$
13		cid	$$class\mathrm{I}$$
14		ve	$$setvare$$
15	9	cpw	$$class𝒫\left(0\dots n\right)$$
16		vx	$$setvarx$$
17		c1	$$class1$$
18	17 8 7	co	$$class\left(1\dots n\right)$$
19	14	cv	$$setvare$$
20	16	cv	$$setvarx$$
21	6 20	cpr	$$class\left\{0,x\right\}$$
22	19 21	wceq	$$wffe=\left\{0,x\right\}$$
23	22 16 18	wrex	$$wff\exists x\in \left(1\dots n\right)e=\left\{0,x\right\}$$
24	23 14 15	crab	$$class\left\{e\in 𝒫\left(0\dots n\right)|\exists x\in \left(1\dots n\right)e=\left\{0,x\right\}\right\}$$
25	13 24	cres	$$class\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)$$
26	12 25	cop	$$class⟨\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\}}⟩$$
27	10 26	cpr	$$class\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\}$$
28	1 2 27	cmpt	$$class\left(n\in {\mathbb{N}}_0⟼\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)$$
29	0 28	wceq	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 wff 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 wff