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 = ( 𝑛 ∈ ℕ0 ↦ { ⟨ ( Base ‘ ndx ) , ( 0 ... 𝑛 ) ⟩ , ⟨ ( .ef ‘ ndx ) , ( I ↾ { 𝑒 ∈ 𝒫 ( 0 ... 𝑛 ) ∣ ∃ 𝑥 ∈ ( 1 ... 𝑛 ) 𝑒 = { 0 , 𝑥 } } ) ⟩ } )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cstgr	⊢ StarGr
1		vn	⊢ 𝑛
2		cn0	⊢ ℕ0
3		cbs	⊢ Base
4		cnx	⊢ ndx
5	4 3	cfv	⊢ ( Base ‘ ndx )
6		cc0	⊢ 0
7		cfz	⊢ ...
8	1	cv	⊢ 𝑛
9	6 8 7	co	⊢ ( 0 ... 𝑛 )
10	5 9	cop	⊢ ⟨ ( Base ‘ ndx ) , ( 0 ... 𝑛 ) ⟩
11		cedgf	⊢ .ef
12	4 11	cfv	⊢ ( .ef ‘ ndx )
13		cid	⊢ I
14		ve	⊢ 𝑒
15	9	cpw	⊢ 𝒫 ( 0 ... 𝑛 )
16		vx	⊢ 𝑥
17		c1	⊢ 1
18	17 8 7	co	⊢ ( 1 ... 𝑛 )
19	14	cv	⊢ 𝑒
20	16	cv	⊢ 𝑥
21	6 20	cpr	⊢ { 0 , 𝑥 }
22	19 21	wceq	⊢ 𝑒 = { 0 , 𝑥 }
23	22 16 18	wrex	⊢ ∃ 𝑥 ∈ ( 1 ... 𝑛 ) 𝑒 = { 0 , 𝑥 }
24	23 14 15	crab	⊢ { 𝑒 ∈ 𝒫 ( 0 ... 𝑛 ) ∣ ∃ 𝑥 ∈ ( 1 ... 𝑛 ) 𝑒 = { 0 , 𝑥 } }
25	13 24	cres	⊢ ( I ↾ { 𝑒 ∈ 𝒫 ( 0 ... 𝑛 ) ∣ ∃ 𝑥 ∈ ( 1 ... 𝑛 ) 𝑒 = { 0 , 𝑥 } } )
26	12 25	cop	⊢ ⟨ ( .ef ‘ ndx ) , ( I ↾ { 𝑒 ∈ 𝒫 ( 0 ... 𝑛 ) ∣ ∃ 𝑥 ∈ ( 1 ... 𝑛 ) 𝑒 = { 0 , 𝑥 } } ) ⟩
27	10 26	cpr	⊢ { ⟨ ( Base ‘ ndx ) , ( 0 ... 𝑛 ) ⟩ , ⟨ ( .ef ‘ ndx ) , ( I ↾ { 𝑒 ∈ 𝒫 ( 0 ... 𝑛 ) ∣ ∃ 𝑥 ∈ ( 1 ... 𝑛 ) 𝑒 = { 0 , 𝑥 } } ) ⟩ }
28	1 2 27	cmpt	⊢ ( 𝑛 ∈ ℕ0 ↦ { ⟨ ( Base ‘ ndx ) , ( 0 ... 𝑛 ) ⟩ , ⟨ ( .ef ‘ ndx ) , ( I ↾ { 𝑒 ∈ 𝒫 ( 0 ... 𝑛 ) ∣ ∃ 𝑥 ∈ ( 1 ... 𝑛 ) 𝑒 = { 0 , 𝑥 } } ) ⟩ } )
29	0 28	wceq	⊢ StarGr = ( 𝑛 ∈ ℕ0 ↦ { ⟨ ( Base ‘ ndx ) , ( 0 ... 𝑛 ) ⟩ , ⟨ ( .ef ‘ ndx ) , ( I ↾ { 𝑒 ∈ 𝒫 ( 0 ... 𝑛 ) ∣ ∃ 𝑥 ∈ ( 1 ... 𝑛 ) 𝑒 = { 0 , 𝑥 } } ) ⟩ } )