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	⊢ ( 𝑉 ∈ 𝑊 → ⟨ 𝑉 , ∅ ⟩ ∈ UPGraph )

Proof

Step	Hyp	Ref	Expression
1		opex	⊢ ⟨ 𝑉 , ∅ ⟩ ∈ V
2	1	a1i	⊢ ( 𝑉 ∈ 𝑊 → ⟨ 𝑉 , ∅ ⟩ ∈ V )
3		0ex	⊢ ∅ ∈ V
4		opiedgfv	⊢ ( ( 𝑉 ∈ 𝑊 ∧ ∅ ∈ V ) → ( iEdg ‘ ⟨ 𝑉 , ∅ ⟩ ) = ∅ )
5	3 4	mpan2	⊢ ( 𝑉 ∈ 𝑊 → ( iEdg ‘ ⟨ 𝑉 , ∅ ⟩ ) = ∅ )
6	2 5	upgr0e	⊢ ( 𝑉 ∈ 𝑊 → ⟨ 𝑉 , ∅ ⟩ ∈ UPGraph )