Definition df-rgr 29069

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 (𝐾 ∈ ℕ₀^*), 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

Step	Hyp	Ref	Expression
1		crgr 29067	. 2 class RegGraph
2		vk	. . . . . 6 setvar 𝑘
3	2	cv 1540	. . . . 5 class 𝑘
4		cxnn0 12548	. . . . 5 class ℕ0*
5	3, 4	wcel 2106	. . . 4 wff 𝑘 ∈ ℕ0*
6		vv	. . . . . . . 8 setvar 𝑣
7	6	cv 1540	. . . . . . 7 class 𝑣
8		vg	. . . . . . . . 9 setvar 𝑔
9	8	cv 1540	. . . . . . . 8 class 𝑔
10		cvtxdg 28977	. . . . . . . 8 class VtxDeg
11	9, 10	cfv 6543	. . . . . . 7 class (VtxDeg‘𝑔)
12	7, 11	cfv 6543	. . . . . 6 class ((VtxDeg‘𝑔)‘𝑣)
13	12, 3	wceq 1541	. . . . 5 wff ((VtxDeg‘𝑔)‘𝑣) = 𝑘
14		cvtx 28511	. . . . . 6 class Vtx
15	9, 14	cfv 6543	. . . . 5 class (Vtx‘𝑔)
16	13, 6, 15	wral 3061	. . . 4 wff ∀𝑣 ∈ (Vtx‘𝑔)((VtxDeg‘𝑔)‘𝑣) = 𝑘
17	5, 16	wa 396	. . 3 wff (𝑘 ∈ ℕ0* ∧ ∀𝑣 ∈ (Vtx‘𝑔)((VtxDeg‘𝑔)‘𝑣) = 𝑘)
18	17, 8, 2	copab 5210	. 2 class {⟨𝑔, 𝑘⟩ ∣ (𝑘 ∈ ℕ0* ∧ ∀𝑣 ∈ (Vtx‘𝑔)((VtxDeg‘𝑔)‘𝑣) = 𝑘)}
19	1, 18	wceq 1541	1 wff RegGraph = {⟨𝑔, 𝑘⟩ ∣ (𝑘 ∈ ℕ0* ∧ ∀𝑣 ∈ (Vtx‘𝑔)((VtxDeg‘𝑔)‘𝑣) = 𝑘)}

This definition is referenced by:  isrgr  29071  rgrprop  29072