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 \notin V$

Proof

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

Metamath Proof Explorer

Theorem usgrprc

Proof