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

Definition df-rgr 40738
Description: Define the "k-regular" predicate, which is true for a "graph" being k-regular: read 𝐺 RegGraph 𝐾 as "𝐺 is 𝐾-regular" or "𝐺 is a 𝐾-regular graph". Note that 𝐾 is allowed to be positive infinity (𝐾 ∈ ℕ0*), as proposed by GL. (Contributed by Alexander van der Vekens, 6-Jul-2018.) (Revised by AV, 26-Dec-2020.)
Assertion
Ref Expression
df-rgr RegGraph = {⟨𝑔, 𝑘⟩ ∣ (𝑘 ∈ ℕ0* ∧ ∀𝑣 ∈ (Vtx‘𝑔)((VtxDeg‘𝑔)‘𝑣) = 𝑘)}
Distinct variable group:   𝑔,𝑘,𝑣

Detailed syntax breakdown of Definition df-rgr
StepHypRef Expression
1 crgr 40736 . 2 class RegGraph
2 vk . . . . . 6 setvar 𝑘
32cv 1473 . . . . 5 class 𝑘
4 cxnn0 40178 . . . . 5 class 0*
53, 4wcel 1976 . . . 4 wff 𝑘 ∈ ℕ0*
6 vv . . . . . . . 8 setvar 𝑣
76cv 1473 . . . . . . 7 class 𝑣
8 vg . . . . . . . . 9 setvar 𝑔
98cv 1473 . . . . . . . 8 class 𝑔
10 cvtxdg 40662 . . . . . . . 8 class VtxDeg
119, 10cfv 5789 . . . . . . 7 class (VtxDeg‘𝑔)
127, 11cfv 5789 . . . . . 6 class ((VtxDeg‘𝑔)‘𝑣)
1312, 3wceq 1474 . . . . 5 wff ((VtxDeg‘𝑔)‘𝑣) = 𝑘
14 cvtx 40210 . . . . . 6 class Vtx
159, 14cfv 5789 . . . . 5 class (Vtx‘𝑔)
1613, 6, 15wral 2895 . . . 4 wff 𝑣 ∈ (Vtx‘𝑔)((VtxDeg‘𝑔)‘𝑣) = 𝑘
175, 16wa 382 . . 3 wff (𝑘 ∈ ℕ0* ∧ ∀𝑣 ∈ (Vtx‘𝑔)((VtxDeg‘𝑔)‘𝑣) = 𝑘)
1817, 8, 2copab 4636 . 2 class {⟨𝑔, 𝑘⟩ ∣ (𝑘 ∈ ℕ0* ∧ ∀𝑣 ∈ (Vtx‘𝑔)((VtxDeg‘𝑔)‘𝑣) = 𝑘)}
191, 18wceq 1474 1 wff RegGraph = {⟨𝑔, 𝑘⟩ ∣ (𝑘 ∈ ℕ0* ∧ ∀𝑣 ∈ (Vtx‘𝑔)((VtxDeg‘𝑔)‘𝑣) = 𝑘)}
Colors of variables: wff setvar class
This definition is referenced by:  isrgr  40740  rgrprop  40741
  Copyright terms: Public domain W3C validator