Theorem usgrprc

Description: The class of simple graphs is a proper class (and therefore, because of prcssprc , the classes of multigraphs, pseudographs and hypergraphs are proper classes, too). (Contributed by AV, 27-Dec-2020)

	Ref	Expression
Assertion	usgrprc	$$⊢\mathrm{USGraph}\notin \mathrm{V}$$

Proof

Step	Hyp	Ref	Expression
1		eqid	$$⊢\left\{⟨v,e⟩|e:\varnothing ⟶\varnothing \right\}=\left\{⟨v,e⟩|e:\varnothing ⟶\varnothing \right\}$$
2	1	griedg0ssusgr	$$⊢\left\{⟨v,e⟩|e:\varnothing ⟶\varnothing \right\}\subseteq \mathrm{USGraph}$$
3	1	griedg0prc	$$⊢\left\{⟨v,e⟩|e:\varnothing ⟶\varnothing \right\}\notin \mathrm{V}$$
4		prcssprc	$$⊢\left(\left\{⟨v,e⟩|e:\varnothing ⟶\varnothing \right\}\subseteq \mathrm{USGraph}\wedge \left\{⟨v,e⟩|e:\varnothing ⟶\varnothing \right\}\notin \mathrm{V}\right)\to \mathrm{USGraph}\notin \mathrm{V}$$
5	2 3 4	mp2an	$$⊢\mathrm{USGraph}\notin \mathrm{V}$$