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 = { ⟨ 𝑔 , 𝑘 ⟩ ∣ ( 𝑘 ∈ ℕ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 ‘ 𝑔 ) ‘ 𝑣 ) = 𝑘 ) }