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	|- StarGr = ( n e. NN0 |-> { <. ( Base ` ndx ) , ( 0 ... n ) >. , <. ( .ef ` ndx ) , ( _I |` { e e. ~P ( 0 ... n ) | E. x e. ( 1 ... n ) e = { 0 , x } } ) >. } )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cstgr	|- StarGr
1		vn	|- n
2		cn0	|- NN0
3		cbs	|- Base
4		cnx	|- ndx
5	4 3	cfv	|- ( Base ` ndx )
6		cc0	|- 0
7		cfz	|- ...
8	1	cv	|- n
9	6 8 7	co	|- ( 0 ... n )
10	5 9	cop	|- <. ( Base ` ndx ) , ( 0 ... n ) >.
11		cedgf	|- .ef
12	4 11	cfv	|- ( .ef ` ndx )
13		cid	|- _I
14		ve	|- e
15	9	cpw	|- ~P ( 0 ... n )
16		vx	|- x
17		c1	|- 1
18	17 8 7	co	|- ( 1 ... n )
19	14	cv	|- e
20	16	cv	|- x
21	6 20	cpr	|- { 0 , x }
22	19 21	wceq	|- e = { 0 , x }
23	22 16 18	wrex	|- E. x e. ( 1 ... n ) e = { 0 , x }
24	23 14 15	crab	|- { e e. ~P ( 0 ... n ) | E. x e. ( 1 ... n ) e = { 0 , x } }
25	13 24	cres	|- ( _I |` { e e. ~P ( 0 ... n ) | E. x e. ( 1 ... n ) e = { 0 , x } } )
26	12 25	cop	|- <. ( .ef ` ndx ) , ( _I |` { e e. ~P ( 0 ... n ) | E. x e. ( 1 ... n ) e = { 0 , x } } ) >.
27	10 26	cpr	|- { <. ( Base ` ndx ) , ( 0 ... n ) >. , <. ( .ef ` ndx ) , ( _I |` { e e. ~P ( 0 ... n ) | E. x e. ( 1 ... n ) e = { 0 , x } } ) >. }
28	1 2 27	cmpt	|- ( n e. NN0 |-> { <. ( Base ` ndx ) , ( 0 ... n ) >. , <. ( .ef ` ndx ) , ( _I |` { e e. ~P ( 0 ... n ) | E. x e. ( 1 ... n ) e = { 0 , x } } ) >. } )
29	0 28	wceq	|- StarGr = ( n e. NN0 |-> { <. ( Base ` ndx ) , ( 0 ... n ) >. , <. ( .ef ` ndx ) , ( _I |` { e e. ~P ( 0 ... n ) | E. x e. ( 1 ... n ) e = { 0 , x } } ) >. } )