Theorem rgrprc

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

	Ref	Expression
Assertion	rgrprc	$$⊢\left\{g|g\mathrm{RegGraph}0\right\}\notin \mathrm{V}$$

Proof

Step	Hyp	Ref	Expression
1		rusgrrgr	$$⊢g\mathrm{RegUSGraph}0\to g\mathrm{RegGraph}0$$
2	1	ss2abi	$$⊢\left\{g|g\mathrm{RegUSGraph}0\right\}\subseteq \left\{g|g\mathrm{RegGraph}0\right\}$$
3		rusgrprc	$$⊢\left\{g|g\mathrm{RegUSGraph}0\right\}\notin \mathrm{V}$$
4		prcssprc	$$⊢\left(\left\{g|g\mathrm{RegUSGraph}0\right\}\subseteq \left\{g|g\mathrm{RegGraph}0\right\}\wedge \left\{g|g\mathrm{RegUSGraph}0\right\}\notin \mathrm{V}\right)\to \left\{g|g\mathrm{RegGraph}0\right\}\notin \mathrm{V}$$
5	2 3 4	mp2an	$$⊢\left\{g|g\mathrm{RegGraph}0\right\}\notin \mathrm{V}$$