Metamath Proof Explorer

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 ∈ ℕ 0 * ⟼ g | ∀ v ∈ Vtx ⁡ g VtxDeg ⁡ g ⁡ v = k
Assertion rgrx0ndm ⊢ 0 ∉ dom ⁡ R

Proof

Step Hyp Ref Expression
1 rgrx0ndm.u ⊢ R = k ∈ ℕ 0 * ⟼ g | ∀ v ∈ Vtx ⁡ g VtxDeg ⁡ g ⁡ v = k
2 rgrprcx ⊢ g | ∀ v ∈ Vtx ⁡ g VtxDeg ⁡ g ⁡ v = 0 ∉ V
3 2 neli ⊢ ¬ g | ∀ v ∈ Vtx ⁡ g VtxDeg ⁡ g ⁡ v = 0 ∈ V
4 3 intnan ⊢ ¬ 0 ∈ ℕ 0 * ∧ g | ∀ v ∈ Vtx ⁡ g VtxDeg ⁡ g ⁡ v = 0 ∈ V
5 df-nel ⊢ 0 ∉ dom ⁡ R ↔ ¬ 0 ∈ dom ⁡ R
6 eqeq2 ⊢ k = 0 → VtxDeg ⁡ g ⁡ v = k ↔ VtxDeg ⁡ g ⁡ v = 0
7 6 ralbidv ⊢ k = 0 → ∀ v ∈ Vtx ⁡ g VtxDeg ⁡ g ⁡ v = k ↔ ∀ v ∈ Vtx ⁡ g VtxDeg ⁡ g ⁡ v = 0
8 7 abbidv ⊢ k = 0 → g | ∀ v ∈ Vtx ⁡ g VtxDeg ⁡ g ⁡ v = k = g | ∀ v ∈ Vtx ⁡ g VtxDeg ⁡ g ⁡ v = 0
9 8 eleq1d ⊢ k = 0 → g | ∀ v ∈ Vtx ⁡ g VtxDeg ⁡ g ⁡ v = k ∈ V ↔ g | ∀ v ∈ Vtx ⁡ g VtxDeg ⁡ g ⁡ v = 0 ∈ V
10 1 dmmpt ⊢ dom ⁡ R = k ∈ ℕ 0 * | g | ∀ v ∈ Vtx ⁡ g VtxDeg ⁡ g ⁡ v = k ∈ V
11 9 10 elrab2 ⊢ 0 ∈ dom ⁡ R ↔ 0 ∈ ℕ 0 * ∧ g | ∀ v ∈ Vtx ⁡ g VtxDeg ⁡ g ⁡ v = 0 ∈ V
12 5 11 xchbinx ⊢ 0 ∉ dom ⁡ R ↔ ¬ 0 ∈ ℕ 0 * ∧ g | ∀ v ∈ Vtx ⁡ g VtxDeg ⁡ g ⁡ v = 0 ∈ V
13 4 12 mpbir ⊢ 0 ∉ dom ⁡ R