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⁡gVtxDeg⁡g⁡v=0∉V

Proof

Step Hyp Ref Expression
1 rgrprc ⊢g|gRegGraph0∉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*→gRegGraph0↔0∈ℕ0*∧∀v∈Vtx⁡gVtxDeg⁡g⁡v=0
7 3 2 6 mp2an ⊢gRegGraph0↔0∈ℕ0*∧∀v∈Vtx⁡gVtxDeg⁡g⁡v=0
8 2 7 mpbiran ⊢gRegGraph0↔∀v∈Vtx⁡gVtxDeg⁡g⁡v=0
9 8 bicomi ⊢∀v∈Vtx⁡gVtxDeg⁡g⁡v=0↔gRegGraph0
10 9 abbii ⊢g|∀v∈Vtx⁡gVtxDeg⁡g⁡v=0=g|gRegGraph0
11 neleq1 ⊢g|∀v∈Vtx⁡gVtxDeg⁡g⁡v=0=g|gRegGraph0→g|∀v∈Vtx⁡gVtxDeg⁡g⁡v=0∉V↔g|gRegGraph0∉V
12 10 11 ax-mp ⊢g|∀v∈Vtx⁡gVtxDeg⁡g⁡v=0∉V↔g|gRegGraph0∉V
13 1 12 mpbir ⊢g|∀v∈Vtx⁡gVtxDeg⁡g⁡v=0∉V