Metamath Proof Explorer

Theorem rusgrprc

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

Ref Expression
Assertion rusgrprc ⊢ g | g RegUSGraph 0 ∉ V

Proof

Step Hyp Ref Expression
1 rgrusgrprc ⊢ g ∈ USGraph | ∀ v ∈ Vtx ⁡ g VtxDeg ⁡ g ⁡ v = 0 ∉ V
2 vex ⊢ g ∈ V
3 0xnn0 ⊢ 0 ∈ ℕ 0 *
4 eqid ⊢ Vtx ⁡ g = Vtx ⁡ g
5 eqid ⊢ VtxDeg ⁡ g = VtxDeg ⁡ g
6 4 5 isrusgr0 ⊢ g ∈ V ∧ 0 ∈ ℕ 0 * → g RegUSGraph 0 ↔ g ∈ USGraph ∧ 0 ∈ ℕ 0 * ∧ ∀ v ∈ Vtx ⁡ g VtxDeg ⁡ g ⁡ v = 0
7 2 3 6 mp2an ⊢ g RegUSGraph 0 ↔ g ∈ USGraph ∧ 0 ∈ ℕ 0 * ∧ ∀ v ∈ Vtx ⁡ g VtxDeg ⁡ g ⁡ v = 0
8 3ancomb ⊢ g ∈ USGraph ∧ 0 ∈ ℕ 0 * ∧ ∀ v ∈ Vtx ⁡ g VtxDeg ⁡ g ⁡ v = 0 ↔ g ∈ USGraph ∧ ∀ v ∈ Vtx ⁡ g VtxDeg ⁡ g ⁡ v = 0 ∧ 0 ∈ ℕ 0 *
9 df-3an ⊢ g ∈ USGraph ∧ ∀ v ∈ Vtx ⁡ g VtxDeg ⁡ g ⁡ v = 0 ∧ 0 ∈ ℕ 0 * ↔ g ∈ USGraph ∧ ∀ v ∈ Vtx ⁡ g VtxDeg ⁡ g ⁡ v = 0 ∧ 0 ∈ ℕ 0 *
10 3 9 mpbiran2 ⊢ g ∈ USGraph ∧ ∀ v ∈ Vtx ⁡ g VtxDeg ⁡ g ⁡ v = 0 ∧ 0 ∈ ℕ 0 * ↔ g ∈ USGraph ∧ ∀ v ∈ Vtx ⁡ g VtxDeg ⁡ g ⁡ v = 0
11 7 8 10 3bitri ⊢ g RegUSGraph 0 ↔ g ∈ USGraph ∧ ∀ v ∈ Vtx ⁡ g VtxDeg ⁡ g ⁡ v = 0
12 11 abbii ⊢ g | g RegUSGraph 0 = g | g ∈ USGraph ∧ ∀ v ∈ Vtx ⁡ g VtxDeg ⁡ g ⁡ v = 0
13 df-rab ⊢ g ∈ USGraph | ∀ v ∈ Vtx ⁡ g VtxDeg ⁡ g ⁡ v = 0 = g | g ∈ USGraph ∧ ∀ v ∈ Vtx ⁡ g VtxDeg ⁡ g ⁡ v = 0
14 12 13 eqtr4i ⊢ g | g RegUSGraph 0 = g ∈ USGraph | ∀ v ∈ Vtx ⁡ g VtxDeg ⁡ g ⁡ v = 0
15 neleq1 ⊢ g | g RegUSGraph 0 = g ∈ USGraph | ∀ v ∈ Vtx ⁡ g VtxDeg ⁡ g ⁡ v = 0 → g | g RegUSGraph 0 ∉ V ↔ g ∈ USGraph | ∀ v ∈ Vtx ⁡ g VtxDeg ⁡ g ⁡ v = 0 ∉ V
16 14 15 ax-mp ⊢ g | g RegUSGraph 0 ∉ V ↔ g ∈ USGraph | ∀ v ∈ Vtx ⁡ g VtxDeg ⁡ g ⁡ v = 0 ∉ V
17 1 16 mpbir ⊢ g | g RegUSGraph 0 ∉ V