Metamath Proof Explorer

Theorem upgracycumgr

Description: An acyclic pseudograph is a multigraph. (Contributed by BTernaryTau, 15-Oct-2023)

Ref Expression
Assertion upgracycumgr ⊢ G ∈ UPGraph ∧ G ∈ AcyclicGraph → G ∈ UMGraph

Proof

Step Hyp Ref Expression
1 upgruhgr ⊢ G ∈ UPGraph → G ∈ UHGraph
2 1 anim1ci ⊢ G ∈ UPGraph ∧ G ∈ AcyclicGraph → G ∈ AcyclicGraph ∧ G ∈ UHGraph
3 eqid ⊢ Vtx ⁡ G = Vtx ⁡ G
4 eqid ⊢ iEdg ⁡ G = iEdg ⁡ G
5 3 4 acycgrislfgr ⊢ G ∈ AcyclicGraph ∧ G ∈ UHGraph → iEdg ⁡ G : dom ⁡ iEdg ⁡ G ⟶ x ∈ 𝒫 Vtx ⁡ G | 2 ≤ x
6 2 5 syl ⊢ G ∈ UPGraph ∧ G ∈ AcyclicGraph → iEdg ⁡ G : dom ⁡ iEdg ⁡ G ⟶ x ∈ 𝒫 Vtx ⁡ G | 2 ≤ x
7 3 4 umgrislfupgr ⊢ G ∈ UMGraph ↔ G ∈ UPGraph ∧ iEdg ⁡ G : dom ⁡ iEdg ⁡ G ⟶ x ∈ 𝒫 Vtx ⁡ G | 2 ≤ x
8 7 biimpri ⊢ G ∈ UPGraph ∧ iEdg ⁡ G : dom ⁡ iEdg ⁡ G ⟶ x ∈ 𝒫 Vtx ⁡ G | 2 ≤ x → G ∈ UMGraph
9 6 8 syldan ⊢ G ∈ UPGraph ∧ G ∈ AcyclicGraph → G ∈ UMGraph