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 = { ⟨ 𝑔 , 𝑘 ⟩ ∣ ( 𝑘 ∈ ℕ0* ∧ ∀ 𝑣 ∈ ( Vtx ‘ 𝑔 ) ( ( VtxDeg ‘ 𝑔 ) ‘ 𝑣 ) = 𝑘 ) }

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		crgr	⊢ RegGraph
1		vg	⊢ 𝑔
2		vk	⊢ 𝑘
3	2	cv	⊢ 𝑘
4		cxnn0	⊢ ℕ0*
5	3 4	wcel	⊢ 𝑘 ∈ ℕ0*
6		vv	⊢ 𝑣
7		cvtx	⊢ Vtx
8	1	cv	⊢ 𝑔
9	8 7	cfv	⊢ ( Vtx ‘ 𝑔 )
10		cvtxdg	⊢ VtxDeg
11	8 10	cfv	⊢ ( VtxDeg ‘ 𝑔 )
12	6	cv	⊢ 𝑣
13	12 11	cfv	⊢ ( ( VtxDeg ‘ 𝑔 ) ‘ 𝑣 )
14	13 3	wceq	⊢ ( ( VtxDeg ‘ 𝑔 ) ‘ 𝑣 ) = 𝑘
15	14 6 9	wral	⊢ ∀ 𝑣 ∈ ( Vtx ‘ 𝑔 ) ( ( VtxDeg ‘ 𝑔 ) ‘ 𝑣 ) = 𝑘
16	5 15	wa	⊢ ( 𝑘 ∈ ℕ0* ∧ ∀ 𝑣 ∈ ( Vtx ‘ 𝑔 ) ( ( VtxDeg ‘ 𝑔 ) ‘ 𝑣 ) = 𝑘 )
17	16 1 2	copab	⊢ { ⟨ 𝑔 , 𝑘 ⟩ ∣ ( 𝑘 ∈ ℕ0* ∧ ∀ 𝑣 ∈ ( Vtx ‘ 𝑔 ) ( ( VtxDeg ‘ 𝑔 ) ‘ 𝑣 ) = 𝑘 ) }
18	0 17	wceq	⊢ RegGraph = { ⟨ 𝑔 , 𝑘 ⟩ ∣ ( 𝑘 ∈ ℕ0* ∧ ∀ 𝑣 ∈ ( Vtx ‘ 𝑔 ) ( ( VtxDeg ‘ 𝑔 ) ‘ 𝑣 ) = 𝑘 ) }