This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ∉ V

Proof

Step	Hyp	Ref	Expression
1		eqid	⊢ { ⟨ 𝑣 , 𝑒 ⟩ ∣ 𝑒 : ∅ ⟶ ∅ } = { ⟨ 𝑣 , 𝑒 ⟩ ∣ 𝑒 : ∅ ⟶ ∅ }
2	1	griedg0ssusgr	⊢ { ⟨ 𝑣 , 𝑒 ⟩ ∣ 𝑒 : ∅ ⟶ ∅ } ⊆ USGraph
3	1	griedg0prc	⊢ { ⟨ 𝑣 , 𝑒 ⟩ ∣ 𝑒 : ∅ ⟶ ∅ } ∉ V
4		prcssprc	⊢ ( ( { ⟨ 𝑣 , 𝑒 ⟩ ∣ 𝑒 : ∅ ⟶ ∅ } ⊆ USGraph ∧ { ⟨ 𝑣 , 𝑒 ⟩ ∣ 𝑒 : ∅ ⟶ ∅ } ∉ V ) → USGraph ∉ V )
5	2 3 4	mp2an	⊢ USGraph ∉ V