Metamath Proof Explorer

Theorem umgrn1cycl

Description: In a multigraph graph (with no loops!) there are no cycles with length 1 (consisting of one edge). (Contributed by Alexander van der Vekens, 7-Nov-2017) (Revised by AV, 2-Feb-2021)

Ref Expression
Assertion umgrn1cycl ⊢ G ∈ UMGraph ∧ F Cycles ⁡ G P → F ≠ 1

Proof

Step Hyp Ref Expression
1 eqid ⊢ Vtx ⁡ G = Vtx ⁡ G
2 eqid ⊢ iEdg ⁡ G = iEdg ⁡ G
3 1 2 umgrislfupgr ⊢ G ∈ UMGraph ↔ G ∈ UPGraph ∧ iEdg ⁡ G : dom ⁡ iEdg ⁡ G ⟶ x ∈ 𝒫 Vtx ⁡ G | 2 ≤ x
4 1 2 lfgrn1cycl ⊢ iEdg ⁡ G : dom ⁡ iEdg ⁡ G ⟶ x ∈ 𝒫 Vtx ⁡ G | 2 ≤ x → F Cycles ⁡ G P → F ≠ 1
5 3 4 simplbiim ⊢ G ∈ UMGraph → F Cycles ⁡ G P → F ≠ 1
6 5 imp ⊢ G ∈ UMGraph ∧ F Cycles ⁡ G P → F ≠ 1