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 e. NN0* /\ A. v e. ( Vtx ` g ) ( ( VtxDeg ` g ) ` v ) = k ) }

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		crgr	|- RegGraph
1		vg	|- g
2		vk	|- k
3	2	cv	|- k
4		cxnn0	|- NN0*
5	3 4	wcel	|- k e. NN0*
6		vv	|- v
7		cvtx	|- Vtx
8	1	cv	|- g
9	8 7	cfv	|- ( Vtx ` g )
10		cvtxdg	|- VtxDeg
11	8 10	cfv	|- ( VtxDeg ` g )
12	6	cv	|- v
13	12 11	cfv	|- ( ( VtxDeg ` g ) ` v )
14	13 3	wceq	|- ( ( VtxDeg ` g ) ` v ) = k
15	14 6 9	wral	|- A. v e. ( Vtx ` g ) ( ( VtxDeg ` g ) ` v ) = k
16	5 15	wa	|- ( k e. NN0* /\ A. v e. ( Vtx ` g ) ( ( VtxDeg ` g ) ` v ) = k )
17	16 1 2	copab	|- { <. g , k >. | ( k e. NN0* /\ A. v e. ( Vtx ` g ) ( ( VtxDeg ` g ) ` v ) = k ) }
18	0 17	wceq	|- RegGraph = { <. g , k >. | ( k e. NN0* /\ A. v e. ( Vtx ` g ) ( ( VtxDeg ` g ) ` v ) = k ) }