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

Metamath Proof Explorer

Theorem umgrnloop2

Description: A multigraph has no loops. (Contributed by AV, 27-Oct-2020) (Revised by AV, 30-Nov-2020)

Ref Expression
Assertion umgrnloop2 ( 𝐺 ∈ UMGraph → { 𝑁 , 𝑁 } ∉ ( Edg ‘ 𝐺 ) )

Proof

Step Hyp Ref Expression
1 eqid ⊢ ( Vtx ‘ 𝐺 ) = ( Vtx ‘ 𝐺 )
2 eqid ⊢ ( Edg ‘ 𝐺 ) = ( Edg ‘ 𝐺 )
3 1 2 umgrpredgv ⊢ ( ( 𝐺 ∈ UMGraph ∧ { 𝑁 , 𝑁 } ∈ ( Edg ‘ 𝐺 ) ) → ( 𝑁 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑁 ∈ ( Vtx ‘ 𝐺 ) ) )
4 3 simpld ⊢ ( ( 𝐺 ∈ UMGraph ∧ { 𝑁 , 𝑁 } ∈ ( Edg ‘ 𝐺 ) ) → 𝑁 ∈ ( Vtx ‘ 𝐺 ) )
5 eqid ⊢ 𝑁 = 𝑁
6 2 umgredgne ⊢ ( ( 𝐺 ∈ UMGraph ∧ { 𝑁 , 𝑁 } ∈ ( Edg ‘ 𝐺 ) ) → 𝑁 ≠ 𝑁 )
7 eqneqall ⊢ ( 𝑁 = 𝑁 → ( 𝑁 ≠ 𝑁 → ¬ 𝑁 ∈ ( Vtx ‘ 𝐺 ) ) )
8 5 6 7 mpsyl ⊢ ( ( 𝐺 ∈ UMGraph ∧ { 𝑁 , 𝑁 } ∈ ( Edg ‘ 𝐺 ) ) → ¬ 𝑁 ∈ ( Vtx ‘ 𝐺 ) )
9 4 8 pm2.65da ⊢ ( 𝐺 ∈ UMGraph → ¬ { 𝑁 , 𝑁 } ∈ ( Edg ‘ 𝐺 ) )
10 df-nel ⊢ ( { 𝑁 , 𝑁 } ∉ ( Edg ‘ 𝐺 ) ↔ ¬ { 𝑁 , 𝑁 } ∈ ( Edg ‘ 𝐺 ) )
11 9 10 sylibr ⊢ ( 𝐺 ∈ UMGraph → { 𝑁 , 𝑁 } ∉ ( Edg ‘ 𝐺 ) )