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	⊢ 𝑅 = ( 𝑘 ∈ ℕ0* ↦ { 𝑔 ∣ ∀ 𝑣 ∈ ( Vtx ‘ 𝑔 ) ( ( VtxDeg ‘ 𝑔 ) ‘ 𝑣 ) = 𝑘 } )
Assertion	rgrx0ndm	⊢ 0 ∉ dom 𝑅

Proof

Step	Hyp	Ref	Expression
1		rgrx0ndm.u	⊢ 𝑅 = ( 𝑘 ∈ ℕ0* ↦ { 𝑔 ∣ ∀ 𝑣 ∈ ( Vtx ‘ 𝑔 ) ( ( VtxDeg ‘ 𝑔 ) ‘ 𝑣 ) = 𝑘 } )
2		rgrprcx	⊢ { 𝑔 ∣ ∀ 𝑣 ∈ ( Vtx ‘ 𝑔 ) ( ( VtxDeg ‘ 𝑔 ) ‘ 𝑣 ) = 0 } ∉ V
3	2	neli	⊢ ¬ { 𝑔 ∣ ∀ 𝑣 ∈ ( Vtx ‘ 𝑔 ) ( ( VtxDeg ‘ 𝑔 ) ‘ 𝑣 ) = 0 } ∈ V
4	3	intnan	⊢ ¬ ( 0 ∈ ℕ0* ∧ { 𝑔 ∣ ∀ 𝑣 ∈ ( Vtx ‘ 𝑔 ) ( ( VtxDeg ‘ 𝑔 ) ‘ 𝑣 ) = 0 } ∈ V )
5		df-nel	⊢ ( 0 ∉ dom 𝑅 ↔ ¬ 0 ∈ dom 𝑅 )
6		eqeq2	⊢ ( 𝑘 = 0 → ( ( ( VtxDeg ‘ 𝑔 ) ‘ 𝑣 ) = 𝑘 ↔ ( ( VtxDeg ‘ 𝑔 ) ‘ 𝑣 ) = 0 ) )
7	6	ralbidv	⊢ ( 𝑘 = 0 → ( ∀ 𝑣 ∈ ( Vtx ‘ 𝑔 ) ( ( VtxDeg ‘ 𝑔 ) ‘ 𝑣 ) = 𝑘 ↔ ∀ 𝑣 ∈ ( Vtx ‘ 𝑔 ) ( ( VtxDeg ‘ 𝑔 ) ‘ 𝑣 ) = 0 ) )
8	7	abbidv	⊢ ( 𝑘 = 0 → { 𝑔 ∣ ∀ 𝑣 ∈ ( Vtx ‘ 𝑔 ) ( ( VtxDeg ‘ 𝑔 ) ‘ 𝑣 ) = 𝑘 } = { 𝑔 ∣ ∀ 𝑣 ∈ ( Vtx ‘ 𝑔 ) ( ( VtxDeg ‘ 𝑔 ) ‘ 𝑣 ) = 0 } )
9	8	eleq1d	⊢ ( 𝑘 = 0 → ( { 𝑔 ∣ ∀ 𝑣 ∈ ( Vtx ‘ 𝑔 ) ( ( VtxDeg ‘ 𝑔 ) ‘ 𝑣 ) = 𝑘 } ∈ V ↔ { 𝑔 ∣ ∀ 𝑣 ∈ ( Vtx ‘ 𝑔 ) ( ( VtxDeg ‘ 𝑔 ) ‘ 𝑣 ) = 0 } ∈ V ) )
10	1	dmmpt	⊢ dom 𝑅 = { 𝑘 ∈ ℕ0* ∣ { 𝑔 ∣ ∀ 𝑣 ∈ ( Vtx ‘ 𝑔 ) ( ( VtxDeg ‘ 𝑔 ) ‘ 𝑣 ) = 𝑘 } ∈ V }
11	9 10	elrab2	⊢ ( 0 ∈ dom 𝑅 ↔ ( 0 ∈ ℕ0* ∧ { 𝑔 ∣ ∀ 𝑣 ∈ ( Vtx ‘ 𝑔 ) ( ( VtxDeg ‘ 𝑔 ) ‘ 𝑣 ) = 0 } ∈ V ) )
12	5 11	xchbinx	⊢ ( 0 ∉ dom 𝑅 ↔ ¬ ( 0 ∈ ℕ0* ∧ { 𝑔 ∣ ∀ 𝑣 ∈ ( Vtx ‘ 𝑔 ) ( ( VtxDeg ‘ 𝑔 ) ‘ 𝑣 ) = 0 } ∈ V ) )
13	4 12	mpbir	⊢ 0 ∉ dom 𝑅