Metamath Proof Explorer


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