Metamath Proof Explorer

Theorem usgrumgr

Description: A simple graph is an undirected multigraph. (Contributed by AV, 25-Nov-2020)

Ref Expression
Assertion usgrumgr ⊢ G ∈ USGraph → G ∈ UMGraph

Proof

Step Hyp Ref Expression
1 eqid ⊢ Vtx ⁡ G = Vtx ⁡ G
2 eqid ⊢ iEdg ⁡ G = iEdg ⁡ G
3 1 2 usgrfs ⊢ G ∈ USGraph → 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 ⊢ G ∈ USGraph → iEdg ⁡ G : dom ⁡ iEdg ⁡ G ⟶ x ∈ 𝒫 Vtx ⁡ G | x = 2
6 1 2 isumgrs ⊢ G ∈ USGraph → G ∈ UMGraph ↔ iEdg ⁡ G : dom ⁡ iEdg ⁡ G ⟶ x ∈ 𝒫 Vtx ⁡ G | x = 2
7 5 6 mpbird ⊢ G ∈ USGraph → G ∈ UMGraph