Metamath Proof Explorer

Theorem umgr0e

Description: The empty graph, with vertices but no edges, is a multigraph. (Contributed by Mario Carneiro, 12-Mar-2015) (Revised by AV, 25-Nov-2020)

Ref Expression
Hypotheses umgr0e.g ⊢ φ → G ∈ W
umgr0e.e ⊢ φ → iEdg ⁡ G = ∅
Assertion umgr0e ⊢ φ → G ∈ UMGraph

Proof

Step Hyp Ref Expression
1 umgr0e.g ⊢ φ → G ∈ W
2 umgr0e.e ⊢ φ → iEdg ⁡ G = ∅
3 2 f10d ⊢ φ → iEdg ⁡ G : dom ⁡ iEdg ⁡ G ⟶ 1-1 x ∈ 𝒫 Vtx ⁡ G ∖ ∅ | x = 2
4 f1f ⊢ iEdg ⁡ G : dom ⁡ iEdg ⁡ G ⟶ 1-1 x ∈ 𝒫 Vtx ⁡ G ∖ ∅ | x = 2 → iEdg ⁡ G : dom ⁡ iEdg ⁡ G ⟶ x ∈ 𝒫 Vtx ⁡ G ∖ ∅ | x = 2
5 3 4 syl ⊢ φ → iEdg ⁡ G : dom ⁡ iEdg ⁡ G ⟶ x ∈ 𝒫 Vtx ⁡ G ∖ ∅ | x = 2
6 eqid ⊢ Vtx ⁡ G = Vtx ⁡ G
7 eqid ⊢ iEdg ⁡ G = iEdg ⁡ G
8 6 7 isumgr ⊢ G ∈ W → G ∈ UMGraph ↔ iEdg ⁡ G : dom ⁡ iEdg ⁡ G ⟶ x ∈ 𝒫 Vtx ⁡ G ∖ ∅ | x = 2
9 1 8 syl ⊢ φ → G ∈ UMGraph ↔ iEdg ⁡ G : dom ⁡ iEdg ⁡ G ⟶ x ∈ 𝒫 Vtx ⁡ G ∖ ∅ | x = 2
10 5 9 mpbird ⊢ φ → G ∈ UMGraph