This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ( ( 𝐺 ∈ UMGraph ∧ 𝐹 ( Cycles ‘ 𝐺 ) 𝑃 ) → ( ♯ ‘ 𝐹 ) ≠ 1 )

Proof

Step Hyp Ref Expression
1 eqid ⊢ ( Vtx ‘ 𝐺 ) = ( Vtx ‘ 𝐺 )
2 eqid ⊢ ( iEdg ‘ 𝐺 ) = ( iEdg ‘ 𝐺 )
3 1 2 umgrislfupgr ⊢ ( 𝐺 ∈ UMGraph ↔ ( 𝐺 ∈ UPGraph ∧ ( iEdg ‘ 𝐺 ) : dom ( iEdg ‘ 𝐺 ) ⟶ { 𝑥 ∈ 𝒫 ( Vtx ‘ 𝐺 ) ∣ 2 ≤ ( ♯ ‘ 𝑥 ) } ) )
4 1 2 lfgrn1cycl ⊢ ( ( iEdg ‘ 𝐺 ) : dom ( iEdg ‘ 𝐺 ) ⟶ { 𝑥 ∈ 𝒫 ( Vtx ‘ 𝐺 ) ∣ 2 ≤ ( ♯ ‘ 𝑥 ) } → ( 𝐹 ( Cycles ‘ 𝐺 ) 𝑃 → ( ♯ ‘ 𝐹 ) ≠ 1 ) )
5 3 4 simplbiim ⊢ ( 𝐺 ∈ UMGraph → ( 𝐹 ( Cycles ‘ 𝐺 ) 𝑃 → ( ♯ ‘ 𝐹 ) ≠ 1 ) )
6 5 imp ⊢ ( ( 𝐺 ∈ UMGraph ∧ 𝐹 ( Cycles ‘ 𝐺 ) 𝑃 ) → ( ♯ ‘ 𝐹 ) ≠ 1 )