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	|- USGraph e/ _V

Proof

Step	Hyp	Ref	Expression
1		eqid	|- { <. v , e >. | e : (/) --> (/) } = { <. v , e >. | e : (/) --> (/) }
2	1	griedg0ssusgr	|- { <. v , e >. | e : (/) --> (/) } C_ USGraph
3	1	griedg0prc	|- { <. v , e >. | e : (/) --> (/) } e/ _V
4		prcssprc	|- ( ( { <. v , e >. | e : (/) --> (/) } C_ USGraph /\ { <. v , e >. | e : (/) --> (/) } e/ _V ) -> USGraph e/ _V )
5	2 3 4	mp2an	|- USGraph e/ _V