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 ∧ { 𝑀 , 𝑁 } ∈ 𝐸 ) → 𝑀 ≠ 𝑁 )