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 ∈ W → V ∅ ∈ UPGraph

Proof

Step Hyp Ref Expression
1 opex ⊢ V ∅ ∈ V
2 1 a1i ⊢ V ∈ W → V ∅ ∈ V
3 0ex ⊢ ∅ ∈ V
4 opiedgfv ⊢ V ∈ W ∧ ∅ ∈ V → iEdg ⁡ V ∅ = ∅
5 3 4 mpan2 ⊢ V ∈ W → iEdg ⁡ V ∅ = ∅
6 2 5 upgr0e ⊢ V ∈ W → V ∅ ∈ UPGraph