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

Metamath Proof Explorer

Theorem umgredgne

Description: An edge of a multigraph always connects two different vertices. Analogue of umgrnloopv resp. umgrnloop . (Contributed by AV, 27-Nov-2020)

Ref Expression
Hypothesis umgredgne.v ⊢ 𝐸 = ( Edg ‘ 𝐺 )
Assertion umgredgne ( ( 𝐺 ∈ UMGraph ∧ { 𝑀 , 𝑁 } ∈ 𝐸 ) → 𝑀 ≠ 𝑁 )

Proof

Step Hyp Ref Expression
1 umgredgne.v ⊢ 𝐸 = ( Edg ‘ 𝐺 )
2 1 eleq2i ⊢ ( { 𝑀 , 𝑁 } ∈ 𝐸 ↔ { 𝑀 , 𝑁 } ∈ ( Edg ‘ 𝐺 ) )
3 edgumgr ⊢ ( ( 𝐺 ∈ UMGraph ∧ { 𝑀 , 𝑁 } ∈ ( Edg ‘ 𝐺 ) ) → ( { 𝑀 , 𝑁 } ∈ 𝒫 ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ { 𝑀 , 𝑁 } ) = 2 ) )
4 2 3 sylan2b ⊢ ( ( 𝐺 ∈ UMGraph ∧ { 𝑀 , 𝑁 } ∈ 𝐸 ) → ( { 𝑀 , 𝑁 } ∈ 𝒫 ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ { 𝑀 , 𝑁 } ) = 2 ) )
5 eqid ⊢ { 𝑀 , 𝑁 } = { 𝑀 , 𝑁 }
6 5 hashprdifel ⊢ ( ( ♯ ‘ { 𝑀 , 𝑁 } ) = 2 → ( 𝑀 ∈ { 𝑀 , 𝑁 } ∧ 𝑁 ∈ { 𝑀 , 𝑁 } ∧ 𝑀 ≠ 𝑁 ) )
7 6 simp3d ⊢ ( ( ♯ ‘ { 𝑀 , 𝑁 } ) = 2 → 𝑀 ≠ 𝑁 )
8 4 7 simpl2im ⊢ ( ( 𝐺 ∈ UMGraph ∧ { 𝑀 , 𝑁 } ∈ 𝐸 ) → 𝑀 ≠ 𝑁 )