Metamath Proof Explorer

Theorem rgrprcx

Description: The class of 0-regular graphs is a proper class. (Contributed by AV, 27-Dec-2020)

Ref Expression
Assertion rgrprcx ⊢ g | ∀ v ∈ Vtx ⁡ g VtxDeg ⁡ g ⁡ v = 0 ∉ V

Proof

Step Hyp Ref Expression
1 rgrprc ⊢ g | g RegGraph 0 ∉ V
2 0xnn0 ⊢ 0 ∈ ℕ 0 *
3 vex ⊢ g ∈ V
4 eqid ⊢ Vtx ⁡ g = Vtx ⁡ g
5 eqid ⊢ VtxDeg ⁡ g = VtxDeg ⁡ g
6 4 5 isrgr ⊢ g ∈ V ∧ 0 ∈ ℕ 0 * → g RegGraph 0 ↔ 0 ∈ ℕ 0 * ∧ ∀ v ∈ Vtx ⁡ g VtxDeg ⁡ g ⁡ v = 0
7 3 2 6 mp2an ⊢ g RegGraph 0 ↔ 0 ∈ ℕ 0 * ∧ ∀ v ∈ Vtx ⁡ g VtxDeg ⁡ g ⁡ v = 0
8 2 7 mpbiran ⊢ g RegGraph 0 ↔ ∀ v ∈ Vtx ⁡ g VtxDeg ⁡ g ⁡ v = 0
9 8 bicomi ⊢ ∀ v ∈ Vtx ⁡ g VtxDeg ⁡ g ⁡ v = 0 ↔ g RegGraph 0
10 9 abbii ⊢ g | ∀ v ∈ Vtx ⁡ g VtxDeg ⁡ g ⁡ v = 0 = g | g RegGraph 0
11 neleq1 ⊢ g | ∀ v ∈ Vtx ⁡ g VtxDeg ⁡ g ⁡ v = 0 = g | g RegGraph 0 → g | ∀ v ∈ Vtx ⁡ g VtxDeg ⁡ g ⁡ v = 0 ∉ V ↔ g | g RegGraph 0 ∉ V
12 10 11 ax-mp ⊢ g | ∀ v ∈ Vtx ⁡ g VtxDeg ⁡ g ⁡ v = 0 ∉ V ↔ g | g RegGraph 0 ∉ V
13 1 12 mpbir ⊢ g | ∀ v ∈ Vtx ⁡ g VtxDeg ⁡ g ⁡ v = 0 ∉ V