Metamath Proof Explorer


Theorem upgracycumgr

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

Ref Expression
Assertion upgracycumgr ( ( 𝐺 ∈ UPGraph ∧ 𝐺 ∈ AcyclicGraph ) → 𝐺 ∈ UMGraph )

Proof

Step Hyp Ref Expression
1 upgruhgr ( 𝐺 ∈ UPGraph → 𝐺 ∈ UHGraph )
2 1 anim1ci ( ( 𝐺 ∈ UPGraph ∧ 𝐺 ∈ AcyclicGraph ) → ( 𝐺 ∈ AcyclicGraph ∧ 𝐺 ∈ UHGraph ) )
3 eqid ( Vtx ‘ 𝐺 ) = ( Vtx ‘ 𝐺 )
4 eqid ( iEdg ‘ 𝐺 ) = ( iEdg ‘ 𝐺 )
5 3 4 acycgrislfgr ( ( 𝐺 ∈ AcyclicGraph ∧ 𝐺 ∈ UHGraph ) → ( iEdg ‘ 𝐺 ) : dom ( iEdg ‘ 𝐺 ) ⟶ { 𝑥 ∈ 𝒫 ( Vtx ‘ 𝐺 ) ∣ 2 ≤ ( ♯ ‘ 𝑥 ) } )
6 2 5 syl ( ( 𝐺 ∈ UPGraph ∧ 𝐺 ∈ AcyclicGraph ) → ( iEdg ‘ 𝐺 ) : dom ( iEdg ‘ 𝐺 ) ⟶ { 𝑥 ∈ 𝒫 ( Vtx ‘ 𝐺 ) ∣ 2 ≤ ( ♯ ‘ 𝑥 ) } )
7 3 4 umgrislfupgr ( 𝐺 ∈ UMGraph ↔ ( 𝐺 ∈ UPGraph ∧ ( iEdg ‘ 𝐺 ) : dom ( iEdg ‘ 𝐺 ) ⟶ { 𝑥 ∈ 𝒫 ( Vtx ‘ 𝐺 ) ∣ 2 ≤ ( ♯ ‘ 𝑥 ) } ) )
8 7 biimpri ( ( 𝐺 ∈ UPGraph ∧ ( iEdg ‘ 𝐺 ) : dom ( iEdg ‘ 𝐺 ) ⟶ { 𝑥 ∈ 𝒫 ( Vtx ‘ 𝐺 ) ∣ 2 ≤ ( ♯ ‘ 𝑥 ) } ) → 𝐺 ∈ UMGraph )
9 6 8 syldan ( ( 𝐺 ∈ UPGraph ∧ 𝐺 ∈ AcyclicGraph ) → 𝐺 ∈ UMGraph )