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}\leftrightarrow \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$$