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 
|- E = ( Edg ` G )
Assertion umgredgne 
|- ( ( G e. UMGraph /\ { M , N } e. E ) -> M =/= N )

Proof

Step Hyp Ref Expression
1 umgredgne.v 
 |-  E = ( Edg ` G )
2 1 eleq2i 
 |-  ( { M , N } e. E <-> { M , N } e. ( Edg ` G ) )
3 edgumgr 
 |-  ( ( G e. UMGraph /\ { M , N } e. ( Edg ` G ) ) -> ( { M , N } e. ~P ( Vtx ` G ) /\ ( # ` { M , N } ) = 2 ) )
4 2 3 sylan2b 
 |-  ( ( G e. UMGraph /\ { M , N } e. E ) -> ( { M , N } e. ~P ( Vtx ` G ) /\ ( # ` { M , N } ) = 2 ) )
5 eqid 
 |-  { M , N } = { M , N }
6 5 hashprdifel 
 |-  ( ( # ` { M , N } ) = 2 -> ( M e. { M , N } /\ N e. { M , N } /\ M =/= N ) )
7 6 simp3d 
 |-  ( ( # ` { M , N } ) = 2 -> M =/= N )
8 4 7 simpl2im 
 |-  ( ( G e. UMGraph /\ { M , N } e. E ) -> M =/= N )