# Metamath Proof Explorer

## Theorem rgrusgrprc

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

Ref Expression
Assertion rgrusgrprc ${⊢}\left\{{g}\in \mathrm{USGraph}|\forall {v}\in \mathrm{Vtx}\left({g}\right)\phantom{\rule{.4em}{0ex}}\mathrm{VtxDeg}\left({g}\right)\left({v}\right)=0\right\}\notin \mathrm{V}$

### Proof

Step Hyp Ref Expression
1 elopab ${⊢}{p}\in \left\{⟨{v},{e}⟩|{e}:\varnothing ⟶\varnothing \right\}↔\exists {v}\phantom{\rule{.4em}{0ex}}\exists {e}\phantom{\rule{.4em}{0ex}}\left({p}=⟨{v},{e}⟩\wedge {e}:\varnothing ⟶\varnothing \right)$
2 f0bi ${⊢}{e}:\varnothing ⟶\varnothing ↔{e}=\varnothing$
3 opeq2 ${⊢}{e}=\varnothing \to ⟨{v},{e}⟩=⟨{v},\varnothing ⟩$
4 usgr0eop ${⊢}{v}\in \mathrm{V}\to ⟨{v},\varnothing ⟩\in \mathrm{USGraph}$
5 4 elv ${⊢}⟨{v},\varnothing ⟩\in \mathrm{USGraph}$
6 3 5 syl6eqel ${⊢}{e}=\varnothing \to ⟨{v},{e}⟩\in \mathrm{USGraph}$
7 vex ${⊢}{v}\in \mathrm{V}$
8 vex ${⊢}{e}\in \mathrm{V}$
9 7 8 opiedgfvi ${⊢}\mathrm{iEdg}\left(⟨{v},{e}⟩\right)={e}$
10 id ${⊢}{e}=\varnothing \to {e}=\varnothing$
11 9 10 syl5eq ${⊢}{e}=\varnothing \to \mathrm{iEdg}\left(⟨{v},{e}⟩\right)=\varnothing$
12 6 11 jca ${⊢}{e}=\varnothing \to \left(⟨{v},{e}⟩\in \mathrm{USGraph}\wedge \mathrm{iEdg}\left(⟨{v},{e}⟩\right)=\varnothing \right)$
13 2 12 sylbi ${⊢}{e}:\varnothing ⟶\varnothing \to \left(⟨{v},{e}⟩\in \mathrm{USGraph}\wedge \mathrm{iEdg}\left(⟨{v},{e}⟩\right)=\varnothing \right)$
14 13 adantl ${⊢}\left({p}=⟨{v},{e}⟩\wedge {e}:\varnothing ⟶\varnothing \right)\to \left(⟨{v},{e}⟩\in \mathrm{USGraph}\wedge \mathrm{iEdg}\left(⟨{v},{e}⟩\right)=\varnothing \right)$
15 eleq1 ${⊢}{p}=⟨{v},{e}⟩\to \left({p}\in \mathrm{USGraph}↔⟨{v},{e}⟩\in \mathrm{USGraph}\right)$
16 fveqeq2 ${⊢}{p}=⟨{v},{e}⟩\to \left(\mathrm{iEdg}\left({p}\right)=\varnothing ↔\mathrm{iEdg}\left(⟨{v},{e}⟩\right)=\varnothing \right)$
17 15 16 anbi12d ${⊢}{p}=⟨{v},{e}⟩\to \left(\left({p}\in \mathrm{USGraph}\wedge \mathrm{iEdg}\left({p}\right)=\varnothing \right)↔\left(⟨{v},{e}⟩\in \mathrm{USGraph}\wedge \mathrm{iEdg}\left(⟨{v},{e}⟩\right)=\varnothing \right)\right)$
18 17 adantr ${⊢}\left({p}=⟨{v},{e}⟩\wedge {e}:\varnothing ⟶\varnothing \right)\to \left(\left({p}\in \mathrm{USGraph}\wedge \mathrm{iEdg}\left({p}\right)=\varnothing \right)↔\left(⟨{v},{e}⟩\in \mathrm{USGraph}\wedge \mathrm{iEdg}\left(⟨{v},{e}⟩\right)=\varnothing \right)\right)$
19 14 18 mpbird ${⊢}\left({p}=⟨{v},{e}⟩\wedge {e}:\varnothing ⟶\varnothing \right)\to \left({p}\in \mathrm{USGraph}\wedge \mathrm{iEdg}\left({p}\right)=\varnothing \right)$
20 fveqeq2 ${⊢}{g}={p}\to \left(\mathrm{iEdg}\left({g}\right)=\varnothing ↔\mathrm{iEdg}\left({p}\right)=\varnothing \right)$
21 20 elrab ${⊢}{p}\in \left\{{g}\in \mathrm{USGraph}|\mathrm{iEdg}\left({g}\right)=\varnothing \right\}↔\left({p}\in \mathrm{USGraph}\wedge \mathrm{iEdg}\left({p}\right)=\varnothing \right)$
22 19 21 sylibr ${⊢}\left({p}=⟨{v},{e}⟩\wedge {e}:\varnothing ⟶\varnothing \right)\to {p}\in \left\{{g}\in \mathrm{USGraph}|\mathrm{iEdg}\left({g}\right)=\varnothing \right\}$
23 22 exlimivv ${⊢}\exists {v}\phantom{\rule{.4em}{0ex}}\exists {e}\phantom{\rule{.4em}{0ex}}\left({p}=⟨{v},{e}⟩\wedge {e}:\varnothing ⟶\varnothing \right)\to {p}\in \left\{{g}\in \mathrm{USGraph}|\mathrm{iEdg}\left({g}\right)=\varnothing \right\}$
24 1 23 sylbi ${⊢}{p}\in \left\{⟨{v},{e}⟩|{e}:\varnothing ⟶\varnothing \right\}\to {p}\in \left\{{g}\in \mathrm{USGraph}|\mathrm{iEdg}\left({g}\right)=\varnothing \right\}$
25 24 ssriv ${⊢}\left\{⟨{v},{e}⟩|{e}:\varnothing ⟶\varnothing \right\}\subseteq \left\{{g}\in \mathrm{USGraph}|\mathrm{iEdg}\left({g}\right)=\varnothing \right\}$
26 eqid ${⊢}\left\{⟨{v},{e}⟩|{e}:\varnothing ⟶\varnothing \right\}=\left\{⟨{v},{e}⟩|{e}:\varnothing ⟶\varnothing \right\}$
27 26 griedg0prc ${⊢}\left\{⟨{v},{e}⟩|{e}:\varnothing ⟶\varnothing \right\}\notin \mathrm{V}$
28 prcssprc ${⊢}\left(\left\{⟨{v},{e}⟩|{e}:\varnothing ⟶\varnothing \right\}\subseteq \left\{{g}\in \mathrm{USGraph}|\mathrm{iEdg}\left({g}\right)=\varnothing \right\}\wedge \left\{⟨{v},{e}⟩|{e}:\varnothing ⟶\varnothing \right\}\notin \mathrm{V}\right)\to \left\{{g}\in \mathrm{USGraph}|\mathrm{iEdg}\left({g}\right)=\varnothing \right\}\notin \mathrm{V}$
29 25 27 28 mp2an ${⊢}\left\{{g}\in \mathrm{USGraph}|\mathrm{iEdg}\left({g}\right)=\varnothing \right\}\notin \mathrm{V}$
30 df-3an ${⊢}\left({g}\in \mathrm{USGraph}\wedge 0\in {ℕ}_{0}^{*}\wedge \forall {v}\in \mathrm{Vtx}\left({g}\right)\phantom{\rule{.4em}{0ex}}\mathrm{VtxDeg}\left({g}\right)\left({v}\right)=0\right)↔\left(\left({g}\in \mathrm{USGraph}\wedge 0\in {ℕ}_{0}^{*}\right)\wedge \forall {v}\in \mathrm{Vtx}\left({g}\right)\phantom{\rule{.4em}{0ex}}\mathrm{VtxDeg}\left({g}\right)\left({v}\right)=0\right)$
31 30 bicomi ${⊢}\left(\left({g}\in \mathrm{USGraph}\wedge 0\in {ℕ}_{0}^{*}\right)\wedge \forall {v}\in \mathrm{Vtx}\left({g}\right)\phantom{\rule{.4em}{0ex}}\mathrm{VtxDeg}\left({g}\right)\left({v}\right)=0\right)↔\left({g}\in \mathrm{USGraph}\wedge 0\in {ℕ}_{0}^{*}\wedge \forall {v}\in \mathrm{Vtx}\left({g}\right)\phantom{\rule{.4em}{0ex}}\mathrm{VtxDeg}\left({g}\right)\left({v}\right)=0\right)$
32 31 a1i ${⊢}{g}\in \mathrm{USGraph}\to \left(\left(\left({g}\in \mathrm{USGraph}\wedge 0\in {ℕ}_{0}^{*}\right)\wedge \forall {v}\in \mathrm{Vtx}\left({g}\right)\phantom{\rule{.4em}{0ex}}\mathrm{VtxDeg}\left({g}\right)\left({v}\right)=0\right)↔\left({g}\in \mathrm{USGraph}\wedge 0\in {ℕ}_{0}^{*}\wedge \forall {v}\in \mathrm{Vtx}\left({g}\right)\phantom{\rule{.4em}{0ex}}\mathrm{VtxDeg}\left({g}\right)\left({v}\right)=0\right)\right)$
33 0xnn0 ${⊢}0\in {ℕ}_{0}^{*}$
34 ibar ${⊢}\left({g}\in \mathrm{USGraph}\wedge 0\in {ℕ}_{0}^{*}\right)\to \left(\forall {v}\in \mathrm{Vtx}\left({g}\right)\phantom{\rule{.4em}{0ex}}\mathrm{VtxDeg}\left({g}\right)\left({v}\right)=0↔\left(\left({g}\in \mathrm{USGraph}\wedge 0\in {ℕ}_{0}^{*}\right)\wedge \forall {v}\in \mathrm{Vtx}\left({g}\right)\phantom{\rule{.4em}{0ex}}\mathrm{VtxDeg}\left({g}\right)\left({v}\right)=0\right)\right)$
35 33 34 mpan2 ${⊢}{g}\in \mathrm{USGraph}\to \left(\forall {v}\in \mathrm{Vtx}\left({g}\right)\phantom{\rule{.4em}{0ex}}\mathrm{VtxDeg}\left({g}\right)\left({v}\right)=0↔\left(\left({g}\in \mathrm{USGraph}\wedge 0\in {ℕ}_{0}^{*}\right)\wedge \forall {v}\in \mathrm{Vtx}\left({g}\right)\phantom{\rule{.4em}{0ex}}\mathrm{VtxDeg}\left({g}\right)\left({v}\right)=0\right)\right)$
36 eqid ${⊢}\mathrm{Vtx}\left({g}\right)=\mathrm{Vtx}\left({g}\right)$
37 eqid ${⊢}\mathrm{VtxDeg}\left({g}\right)=\mathrm{VtxDeg}\left({g}\right)$
38 36 37 isrusgr0 ${⊢}\left({g}\in \mathrm{USGraph}\wedge 0\in {ℕ}_{0}^{*}\right)\to \left({g}\mathrm{RegUSGraph}0↔\left({g}\in \mathrm{USGraph}\wedge 0\in {ℕ}_{0}^{*}\wedge \forall {v}\in \mathrm{Vtx}\left({g}\right)\phantom{\rule{.4em}{0ex}}\mathrm{VtxDeg}\left({g}\right)\left({v}\right)=0\right)\right)$
39 33 38 mpan2 ${⊢}{g}\in \mathrm{USGraph}\to \left({g}\mathrm{RegUSGraph}0↔\left({g}\in \mathrm{USGraph}\wedge 0\in {ℕ}_{0}^{*}\wedge \forall {v}\in \mathrm{Vtx}\left({g}\right)\phantom{\rule{.4em}{0ex}}\mathrm{VtxDeg}\left({g}\right)\left({v}\right)=0\right)\right)$
40 32 35 39 3bitr4d ${⊢}{g}\in \mathrm{USGraph}\to \left(\forall {v}\in \mathrm{Vtx}\left({g}\right)\phantom{\rule{.4em}{0ex}}\mathrm{VtxDeg}\left({g}\right)\left({v}\right)=0↔{g}\mathrm{RegUSGraph}0\right)$
41 40 rabbiia ${⊢}\left\{{g}\in \mathrm{USGraph}|\forall {v}\in \mathrm{Vtx}\left({g}\right)\phantom{\rule{.4em}{0ex}}\mathrm{VtxDeg}\left({g}\right)\left({v}\right)=0\right\}=\left\{{g}\in \mathrm{USGraph}|{g}\mathrm{RegUSGraph}0\right\}$
42 usgr0edg0rusgr ${⊢}{g}\in \mathrm{USGraph}\to \left({g}\mathrm{RegUSGraph}0↔\mathrm{Edg}\left({g}\right)=\varnothing \right)$
43 usgruhgr ${⊢}{g}\in \mathrm{USGraph}\to {g}\in \mathrm{UHGraph}$
44 uhgriedg0edg0 ${⊢}{g}\in \mathrm{UHGraph}\to \left(\mathrm{Edg}\left({g}\right)=\varnothing ↔\mathrm{iEdg}\left({g}\right)=\varnothing \right)$
45 43 44 syl ${⊢}{g}\in \mathrm{USGraph}\to \left(\mathrm{Edg}\left({g}\right)=\varnothing ↔\mathrm{iEdg}\left({g}\right)=\varnothing \right)$
46 42 45 bitrd ${⊢}{g}\in \mathrm{USGraph}\to \left({g}\mathrm{RegUSGraph}0↔\mathrm{iEdg}\left({g}\right)=\varnothing \right)$
47 46 rabbiia ${⊢}\left\{{g}\in \mathrm{USGraph}|{g}\mathrm{RegUSGraph}0\right\}=\left\{{g}\in \mathrm{USGraph}|\mathrm{iEdg}\left({g}\right)=\varnothing \right\}$
48 41 47 eqtri ${⊢}\left\{{g}\in \mathrm{USGraph}|\forall {v}\in \mathrm{Vtx}\left({g}\right)\phantom{\rule{.4em}{0ex}}\mathrm{VtxDeg}\left({g}\right)\left({v}\right)=0\right\}=\left\{{g}\in \mathrm{USGraph}|\mathrm{iEdg}\left({g}\right)=\varnothing \right\}$
49 neleq1 ${⊢}\left\{{g}\in \mathrm{USGraph}|\forall {v}\in \mathrm{Vtx}\left({g}\right)\phantom{\rule{.4em}{0ex}}\mathrm{VtxDeg}\left({g}\right)\left({v}\right)=0\right\}=\left\{{g}\in \mathrm{USGraph}|\mathrm{iEdg}\left({g}\right)=\varnothing \right\}\to \left(\left\{{g}\in \mathrm{USGraph}|\forall {v}\in \mathrm{Vtx}\left({g}\right)\phantom{\rule{.4em}{0ex}}\mathrm{VtxDeg}\left({g}\right)\left({v}\right)=0\right\}\notin \mathrm{V}↔\left\{{g}\in \mathrm{USGraph}|\mathrm{iEdg}\left({g}\right)=\varnothing \right\}\notin \mathrm{V}\right)$
50 48 49 ax-mp ${⊢}\left\{{g}\in \mathrm{USGraph}|\forall {v}\in \mathrm{Vtx}\left({g}\right)\phantom{\rule{.4em}{0ex}}\mathrm{VtxDeg}\left({g}\right)\left({v}\right)=0\right\}\notin \mathrm{V}↔\left\{{g}\in \mathrm{USGraph}|\mathrm{iEdg}\left({g}\right)=\varnothing \right\}\notin \mathrm{V}$
51 29 50 mpbir ${⊢}\left\{{g}\in \mathrm{USGraph}|\forall {v}\in \mathrm{Vtx}\left({g}\right)\phantom{\rule{.4em}{0ex}}\mathrm{VtxDeg}\left({g}\right)\left({v}\right)=0\right\}\notin \mathrm{V}$