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\in W\to ⟨V,\varnothing ⟩\in \mathrm{UPGraph}$$

Proof

Step	Hyp	Ref	Expression
1		opex	$$⊢⟨V,\varnothing ⟩\in \mathrm{V}$$
2	1	a1i	$$⊢V\in W\to ⟨V,\varnothing ⟩\in \mathrm{V}$$
3		0ex	$$⊢\varnothing \in \mathrm{V}$$
4		opiedgfv	$$⊢\left(V\in W\wedge \varnothing \in \mathrm{V}\right)\to \mathrm{iEdg}\left(⟨V,\varnothing ⟩\right)=\varnothing$$
5	3 4	mpan2	$$⊢V\in W\to \mathrm{iEdg}\left(⟨V,\varnothing ⟩\right)=\varnothing$$
6	2 5	upgr0e	$$⊢V\in W\to ⟨V,\varnothing ⟩\in \mathrm{UPGraph}$$