Theorem rgrprc

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

	Ref	Expression
Assertion	rgrprc	⊢ { 𝑔 ∣ 𝑔 RegGraph 0 } ∉ V

Proof

Step	Hyp	Ref	Expression
1		rusgrrgr	⊢ ( 𝑔 RegUSGraph 0 → 𝑔 RegGraph 0 )
2	1	ss2abi	⊢ { 𝑔 ∣ 𝑔 RegUSGraph 0 } ⊆ { 𝑔 ∣ 𝑔 RegGraph 0 }
3		rusgrprc	⊢ { 𝑔 ∣ 𝑔 RegUSGraph 0 } ∉ V
4		prcssprc	⊢ ( ( { 𝑔 ∣ 𝑔 RegUSGraph 0 } ⊆ { 𝑔 ∣ 𝑔 RegGraph 0 } ∧ { 𝑔 ∣ 𝑔 RegUSGraph 0 } ∉ V ) → { 𝑔 ∣ 𝑔 RegGraph 0 } ∉ V )
5	2 3 4	mp2an	⊢ { 𝑔 ∣ 𝑔 RegGraph 0 } ∉ V