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

Metamath Proof Explorer

Theorem upgr0eop

Description: The empty graph, with vertices but no edges, is a pseudograph. The empty graph is actually a simple graph, see usgr0eop , and therefore also a multigraph ( G e. UMGraph ). (Contributed by Mario Carneiro, 12-Mar-2015) (Revised by AV, 11-Oct-2020)

		Ref	Expression
	Assertion	upgr0eop	\|- ( V e. W -> <. V , (/) >. e. UPGraph )

Proof

Step	Hyp	Ref	Expression
1		opex	\|- <. V , (/) >. e. _V
2	1	a1i	\|- ( V e. W -> <. V , (/) >. e. _V )
3		0ex	\|- (/) e. _V
4		opiedgfv	\|- ( ( V e. W /\ (/) e. _V ) -> ( iEdg ` <. V , (/) >. ) = (/) )
5	3 4	mpan2	\|- ( V e. W -> ( iEdg ` <. V , (/) >. ) = (/) )
6	2 5	upgr0e	\|- ( V e. W -> <. V , (/) >. e. UPGraph )