Metamath Proof Explorer

Definition df-rgr

Description: Define the "k-regular" predicate, which is true for a "graph" being k-regular: read G RegGraph K as " G is K-regular" or " G is a K-regular graph". Note that K is allowed to be positive infinity ( K e. NN0* ), as proposed by GL. (Contributed by Alexander van der Vekens, 6-Jul-2018) (Revised by AV, 26-Dec-2020)

Ref Expression
Assertion df-rgr ⊢ RegGraph = g k | k ∈ ℕ 0 * ∧ ∀ v ∈ Vtx ⁡ g VtxDeg ⁡ g ⁡ v = k

Detailed syntax breakdown

Step Hyp Ref Expression
0 crgr class RegGraph
1 vg setvar g
2 vk setvar k
3 2 cv setvar k
4 cxnn0 class ℕ 0 *
5 3 4 wcel wff k ∈ ℕ 0 *
6 vv setvar v
7 cvtx class Vtx
8 1 cv setvar g
9 8 7 cfv class Vtx ⁡ g
10 cvtxdg class VtxDeg
11 8 10 cfv class VtxDeg ⁡ g
12 6 cv setvar v
13 12 11 cfv class VtxDeg ⁡ g ⁡ v
14 13 3 wceq wff VtxDeg ⁡ g ⁡ v = k
15 14 6 9 wral wff ∀ v ∈ Vtx ⁡ g VtxDeg ⁡ g ⁡ v = k
16 5 15 wa wff k ∈ ℕ 0 * ∧ ∀ v ∈ Vtx ⁡ g VtxDeg ⁡ g ⁡ v = k
17 16 1 2 copab class g k | k ∈ ℕ 0 * ∧ ∀ v ∈ Vtx ⁡ g VtxDeg ⁡ g ⁡ v = k
18 0 17 wceq wff RegGraph = g k | k ∈ ℕ 0 * ∧ ∀ v ∈ Vtx ⁡ g VtxDeg ⁡ g ⁡ v = k