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 47854
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 47862, (StarGr‘1) will be a single edge (graph with two vertices connected by an edge), see stgr1 47863, 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 47853 . 2 class StarGr
2 vn . . 3 setvar 𝑛
3 cn0 12523 . . 3 class 0
4 cnx 17226 . . . . . 6 class ndx
5 cbs 17244 . . . . . 6 class Base
64, 5cfv 6562 . . . . 5 class (Base‘ndx)
7 cc0 11152 . . . . . 6 class 0
82cv 1535 . . . . . 6 class 𝑛
9 cfz 13543 . . . . . 6 class ...
107, 8, 9co 7430 . . . . 5 class (0...𝑛)
116, 10cop 4636 . . . 4 class ⟨(Base‘ndx), (0...𝑛)⟩
12 cedgf 29017 . . . . . 6 class .ef
134, 12cfv 6562 . . . . 5 class (.ef‘ndx)
14 cid 5581 . . . . . 6 class I
15 ve . . . . . . . . . 10 setvar 𝑒
1615cv 1535 . . . . . . . . 9 class 𝑒
17 vx . . . . . . . . . . 11 setvar 𝑥
1817cv 1535 . . . . . . . . . 10 class 𝑥
197, 18cpr 4632 . . . . . . . . 9 class {0, 𝑥}
2016, 19wceq 1536 . . . . . . . 8 wff 𝑒 = {0, 𝑥}
21 c1 11153 . . . . . . . . 9 class 1
2221, 8, 9co 7430 . . . . . . . 8 class (1...𝑛)
2320, 17, 22wrex 3067 . . . . . . 7 wff 𝑥 ∈ (1...𝑛)𝑒 = {0, 𝑥}
2410cpw 4604 . . . . . . 7 class 𝒫 (0...𝑛)
2523, 15, 24crab 3432 . . . . . 6 class {𝑒 ∈ 𝒫 (0...𝑛) ∣ ∃𝑥 ∈ (1...𝑛)𝑒 = {0, 𝑥}}
2614, 25cres 5690 . . . . 5 class ( I ↾ {𝑒 ∈ 𝒫 (0...𝑛) ∣ ∃𝑥 ∈ (1...𝑛)𝑒 = {0, 𝑥}})
2713, 26cop 4636 . . . 4 class ⟨(.ef‘ndx), ( I ↾ {𝑒 ∈ 𝒫 (0...𝑛) ∣ ∃𝑥 ∈ (1...𝑛)𝑒 = {0, 𝑥}})⟩
2811, 27cpr 4632 . . 3 class {⟨(Base‘ndx), (0...𝑛)⟩, ⟨(.ef‘ndx), ( I ↾ {𝑒 ∈ 𝒫 (0...𝑛) ∣ ∃𝑥 ∈ (1...𝑛)𝑒 = {0, 𝑥}})⟩}
292, 3, 28cmpt 5230 . 2 class (𝑛 ∈ ℕ0 ↦ {⟨(Base‘ndx), (0...𝑛)⟩, ⟨(.ef‘ndx), ( I ↾ {𝑒 ∈ 𝒫 (0...𝑛) ∣ ∃𝑥 ∈ (1...𝑛)𝑒 = {0, 𝑥}})⟩})
301, 29wceq 1536 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  47855
  Copyright terms: Public domain W3C validator