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 )