Metamath Proof Explorer


Theorem usgr0eop

Description: The empty graph, with vertices but no edges, is a simple graph. (Contributed by Alexander van der Vekens, 10-Aug-2017) (Revised by AV, 16-Oct-2020)

Ref Expression
Assertion usgr0eop ( 𝑉𝑊 → ⟨ 𝑉 , ∅ ⟩ ∈ USGraph )

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