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 ${⊢}\left({G}\in \mathrm{UMGraph}\wedge {F}\mathrm{Cycles}\left({G}\right){P}\right)\to \left|{F}\right|\ne 1$

Proof

Step Hyp Ref Expression
1 eqid ${⊢}\mathrm{Vtx}\left({G}\right)=\mathrm{Vtx}\left({G}\right)$
2 eqid ${⊢}\mathrm{iEdg}\left({G}\right)=\mathrm{iEdg}\left({G}\right)$
3 1 2 umgrislfupgr ${⊢}{G}\in \mathrm{UMGraph}↔\left({G}\in \mathrm{UPGraph}\wedge \mathrm{iEdg}\left({G}\right):\mathrm{dom}\mathrm{iEdg}\left({G}\right)⟶\left\{{x}\in 𝒫\mathrm{Vtx}\left({G}\right)|2\le \left|{x}\right|\right\}\right)$
4 1 2 lfgrn1cycl ${⊢}\mathrm{iEdg}\left({G}\right):\mathrm{dom}\mathrm{iEdg}\left({G}\right)⟶\left\{{x}\in 𝒫\mathrm{Vtx}\left({G}\right)|2\le \left|{x}\right|\right\}\to \left({F}\mathrm{Cycles}\left({G}\right){P}\to \left|{F}\right|\ne 1\right)$
5 3 4 simplbiim ${⊢}{G}\in \mathrm{UMGraph}\to \left({F}\mathrm{Cycles}\left({G}\right){P}\to \left|{F}\right|\ne 1\right)$
6 5 imp ${⊢}\left({G}\in \mathrm{UMGraph}\wedge {F}\mathrm{Cycles}\left({G}\right){P}\right)\to \left|{F}\right|\ne 1$