MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-rgr Structured version   Visualization version   GIF version

Definition df-rgr 28814
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 28812 . 2 class RegGraph
2 vk . . . . . 6 setvar π‘˜
32cv 1541 . . . . 5 class π‘˜
4 cxnn0 12544 . . . . 5 class β„•0*
53, 4wcel 2107 . . . 4 wff π‘˜ ∈ β„•0*
6 vv . . . . . . . 8 setvar 𝑣
76cv 1541 . . . . . . 7 class 𝑣
8 vg . . . . . . . . 9 setvar 𝑔
98cv 1541 . . . . . . . 8 class 𝑔
10 cvtxdg 28722 . . . . . . . 8 class VtxDeg
119, 10cfv 6544 . . . . . . 7 class (VtxDegβ€˜π‘”)
127, 11cfv 6544 . . . . . 6 class ((VtxDegβ€˜π‘”)β€˜π‘£)
1312, 3wceq 1542 . . . . 5 wff ((VtxDegβ€˜π‘”)β€˜π‘£) = π‘˜
14 cvtx 28256 . . . . . 6 class Vtx
159, 14cfv 6544 . . . . 5 class (Vtxβ€˜π‘”)
1613, 6, 15wral 3062 . . . 4 wff βˆ€π‘£ ∈ (Vtxβ€˜π‘”)((VtxDegβ€˜π‘”)β€˜π‘£) = π‘˜
175, 16wa 397 . . 3 wff (π‘˜ ∈ β„•0* ∧ βˆ€π‘£ ∈ (Vtxβ€˜π‘”)((VtxDegβ€˜π‘”)β€˜π‘£) = π‘˜)
1817, 8, 2copab 5211 . 2 class {βŸ¨π‘”, π‘˜βŸ© ∣ (π‘˜ ∈ β„•0* ∧ βˆ€π‘£ ∈ (Vtxβ€˜π‘”)((VtxDegβ€˜π‘”)β€˜π‘£) = π‘˜)}
191, 18wceq 1542 1 wff RegGraph = {βŸ¨π‘”, π‘˜βŸ© ∣ (π‘˜ ∈ β„•0* ∧ βˆ€π‘£ ∈ (Vtxβ€˜π‘”)((VtxDegβ€˜π‘”)β€˜π‘£) = π‘˜)}
Colors of variables: wff setvar class
This definition is referenced by:  isrgr  28816  rgrprop  28817
  Copyright terms: Public domain W3C validator