Definition df-stgr 47919

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

Assertion

Ref	Expression
df-stgr	⊢ StarGr = (𝑛 ∈ ℕ0 ↦ {⟨(Base‘ndx), (0...𝑛)⟩, ⟨(.ef‘ndx), ( I ↾ {𝑒 ∈ 𝒫 (0...𝑛) ∣ ∃𝑥 ∈ (1...𝑛)𝑒 = {0, 𝑥}})⟩})

Distinct variable group:   𝑒,𝑛,𝑥

Detailed syntax breakdown of Definition df-stgr

Step	Hyp	Ref	Expression
1		cstgr 47918	. 2 class StarGr
2		vn	. . 3 setvar 𝑛
3		cn0 12526	. . 3 class ℕ0
4		cnx 17230	. . . . . 6 class ndx
5		cbs 17247	. . . . . 6 class Base
6	4, 5	cfv 6561	. . . . 5 class (Base‘ndx)
7		cc0 11155	. . . . . 6 class 0
8	2	cv 1539	. . . . . 6 class 𝑛
9		cfz 13547	. . . . . 6 class ...
10	7, 8, 9	co 7431	. . . . 5 class (0...𝑛)
11	6, 10	cop 4632	. . . 4 class ⟨(Base‘ndx), (0...𝑛)⟩
12		cedgf 29003	. . . . . 6 class .ef
13	4, 12	cfv 6561	. . . . 5 class (.ef‘ndx)
14		cid 5577	. . . . . 6 class I
15		ve	. . . . . . . . . 10 setvar 𝑒
16	15	cv 1539	. . . . . . . . 9 class 𝑒
17		vx	. . . . . . . . . . 11 setvar 𝑥
18	17	cv 1539	. . . . . . . . . 10 class 𝑥
19	7, 18	cpr 4628	. . . . . . . . 9 class {0, 𝑥}
20	16, 19	wceq 1540	. . . . . . . 8 wff 𝑒 = {0, 𝑥}
21		c1 11156	. . . . . . . . 9 class 1
22	21, 8, 9	co 7431	. . . . . . . 8 class (1...𝑛)
23	20, 17, 22	wrex 3070	. . . . . . 7 wff ∃𝑥 ∈ (1...𝑛)𝑒 = {0, 𝑥}
24	10	cpw 4600	. . . . . . 7 class 𝒫 (0...𝑛)
25	23, 15, 24	crab 3436	. . . . . 6 class {𝑒 ∈ 𝒫 (0...𝑛) ∣ ∃𝑥 ∈ (1...𝑛)𝑒 = {0, 𝑥}}
26	14, 25	cres 5687	. . . . 5 class ( I ↾ {𝑒 ∈ 𝒫 (0...𝑛) ∣ ∃𝑥 ∈ (1...𝑛)𝑒 = {0, 𝑥}})
27	13, 26	cop 4632	. . . 4 class ⟨(.ef‘ndx), ( I ↾ {𝑒 ∈ 𝒫 (0...𝑛) ∣ ∃𝑥 ∈ (1...𝑛)𝑒 = {0, 𝑥}})⟩
28	11, 27	cpr 4628	. . 3 class {⟨(Base‘ndx), (0...𝑛)⟩, ⟨(.ef‘ndx), ( I ↾ {𝑒 ∈ 𝒫 (0...𝑛) ∣ ∃𝑥 ∈ (1...𝑛)𝑒 = {0, 𝑥}})⟩}
29	2, 3, 28	cmpt 5225	. 2 class (𝑛 ∈ ℕ0 ↦ {⟨(Base‘ndx), (0...𝑛)⟩, ⟨(.ef‘ndx), ( I ↾ {𝑒 ∈ 𝒫 (0...𝑛) ∣ ∃𝑥 ∈ (1...𝑛)𝑒 = {0, 𝑥}})⟩})
30	1, 29	wceq 1540	1 wff StarGr = (𝑛 ∈ ℕ0 ↦ {⟨(Base‘ndx), (0...𝑛)⟩, ⟨(.ef‘ndx), ( I ↾ {𝑒 ∈ 𝒫 (0...𝑛) ∣ ∃𝑥 ∈ (1...𝑛)𝑒 = {0, 𝑥}})⟩})

This definition is referenced by:  stgrfv  47920