Users' Mathboxes Mathbox for Alexander van der Vekens < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-stgr Structured version   Visualization version   GIF version

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
StepHypRef 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
64, 5cfv 6561 . . . . 5 class (Base‘ndx)
7 cc0 11155 . . . . . 6 class 0
82cv 1539 . . . . . 6 class 𝑛
9 cfz 13547 . . . . . 6 class ...
107, 8, 9co 7431 . . . . 5 class (0...𝑛)
116, 10cop 4632 . . . 4 class ⟨(Base‘ndx), (0...𝑛)⟩
12 cedgf 29003 . . . . . 6 class .ef
134, 12cfv 6561 . . . . 5 class (.ef‘ndx)
14 cid 5577 . . . . . 6 class I
15 ve . . . . . . . . . 10 setvar 𝑒
1615cv 1539 . . . . . . . . 9 class 𝑒
17 vx . . . . . . . . . . 11 setvar 𝑥
1817cv 1539 . . . . . . . . . 10 class 𝑥
197, 18cpr 4628 . . . . . . . . 9 class {0, 𝑥}
2016, 19wceq 1540 . . . . . . . 8 wff 𝑒 = {0, 𝑥}
21 c1 11156 . . . . . . . . 9 class 1
2221, 8, 9co 7431 . . . . . . . 8 class (1...𝑛)
2320, 17, 22wrex 3070 . . . . . . 7 wff 𝑥 ∈ (1...𝑛)𝑒 = {0, 𝑥}
2410cpw 4600 . . . . . . 7 class 𝒫 (0...𝑛)
2523, 15, 24crab 3436 . . . . . 6 class {𝑒 ∈ 𝒫 (0...𝑛) ∣ ∃𝑥 ∈ (1...𝑛)𝑒 = {0, 𝑥}}
2614, 25cres 5687 . . . . 5 class ( I ↾ {𝑒 ∈ 𝒫 (0...𝑛) ∣ ∃𝑥 ∈ (1...𝑛)𝑒 = {0, 𝑥}})
2713, 26cop 4632 . . . 4 class ⟨(.ef‘ndx), ( I ↾ {𝑒 ∈ 𝒫 (0...𝑛) ∣ ∃𝑥 ∈ (1...𝑛)𝑒 = {0, 𝑥}})⟩
2811, 27cpr 4628 . . 3 class {⟨(Base‘ndx), (0...𝑛)⟩, ⟨(.ef‘ndx), ( I ↾ {𝑒 ∈ 𝒫 (0...𝑛) ∣ ∃𝑥 ∈ (1...𝑛)𝑒 = {0, 𝑥}})⟩}
292, 3, 28cmpt 5225 . 2 class (𝑛 ∈ ℕ0 ↦ {⟨(Base‘ndx), (0...𝑛)⟩, ⟨(.ef‘ndx), ( I ↾ {𝑒 ∈ 𝒫 (0...𝑛) ∣ ∃𝑥 ∈ (1...𝑛)𝑒 = {0, 𝑥}})⟩})
301, 29wceq 1540 1 wff StarGr = (𝑛 ∈ ℕ0 ↦ {⟨(Base‘ndx), (0...𝑛)⟩, ⟨(.ef‘ndx), ( I ↾ {𝑒 ∈ 𝒫 (0...𝑛) ∣ ∃𝑥 ∈ (1...𝑛)𝑒 = {0, 𝑥}})⟩})
Colors of variables: wff setvar class
This definition is referenced by:  stgrfv  47920
  Copyright terms: Public domain W3C validator