Theorem rgrx0ndm

Description: 0 is not in the domain of the potentially alternative definition of the sets of k-regular graphs for each extended nonnegative integer k. (Contributed by AV, 28-Dec-2020)

	Ref	Expression
Hypothesis	rgrx0ndm.u	|- R = ( k e. NN0* |-> { g | A. v e. ( Vtx ` g ) ( ( VtxDeg ` g ) ` v ) = k } )
Assertion	rgrx0ndm	|- 0 e/ dom R

Proof

Step	Hyp	Ref	Expression
1		rgrx0ndm.u	|- R = ( k e. NN0* |-> { g | A. v e. ( Vtx ` g ) ( ( VtxDeg ` g ) ` v ) = k } )
2		rgrprcx	|- { g | A. v e. ( Vtx ` g ) ( ( VtxDeg ` g ) ` v ) = 0 } e/ _V
3	2	neli	|- -. { g | A. v e. ( Vtx ` g ) ( ( VtxDeg ` g ) ` v ) = 0 } e. _V
4	3	intnan	|- -. ( 0 e. NN0* /\ { g | A. v e. ( Vtx ` g ) ( ( VtxDeg ` g ) ` v ) = 0 } e. _V )
5		df-nel	|- ( 0 e/ dom R <-> -. 0 e. dom R )
6		eqeq2	|- ( k = 0 -> ( ( ( VtxDeg ` g ) ` v ) = k <-> ( ( VtxDeg ` g ) ` v ) = 0 ) )
7	6	ralbidv	|- ( k = 0 -> ( A. v e. ( Vtx ` g ) ( ( VtxDeg ` g ) ` v ) = k <-> A. v e. ( Vtx ` g ) ( ( VtxDeg ` g ) ` v ) = 0 ) )
8	7	abbidv	|- ( k = 0 -> { g | A. v e. ( Vtx ` g ) ( ( VtxDeg ` g ) ` v ) = k } = { g | A. v e. ( Vtx ` g ) ( ( VtxDeg ` g ) ` v ) = 0 } )
9	8	eleq1d	|- ( k = 0 -> ( { g | A. v e. ( Vtx ` g ) ( ( VtxDeg ` g ) ` v ) = k } e. _V <-> { g | A. v e. ( Vtx ` g ) ( ( VtxDeg ` g ) ` v ) = 0 } e. _V ) )
10	1	dmmpt	|- dom R = { k e. NN0* | { g | A. v e. ( Vtx ` g ) ( ( VtxDeg ` g ) ` v ) = k } e. _V }
11	9 10	elrab2	|- ( 0 e. dom R <-> ( 0 e. NN0* /\ { g | A. v e. ( Vtx ` g ) ( ( VtxDeg ` g ) ` v ) = 0 } e. _V ) )
12	5 11	xchbinx	|- ( 0 e/ dom R <-> -. ( 0 e. NN0* /\ { g | A. v e. ( Vtx ` g ) ( ( VtxDeg ` g ) ` v ) = 0 } e. _V ) )
13	4 12	mpbir	|- 0 e/ dom R