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

Metamath Proof Explorer

Theorem umgredgnlp

Description: An edge of a multigraph is not a loop. (Contributed by AV, 9-Jan-2020) (Revised by AV, 8-Jun-2021)

Ref Expression
Hypothesis umgredgnlp.e 
|- E = ( Edg ` G )
Assertion umgredgnlp 
|- ( ( G e. UMGraph /\ C e. E ) -> -. E. v C = { v } )

Proof

Step Hyp Ref Expression
1 umgredgnlp.e 
 |-  E = ( Edg ` G )
2 vex 
 |-  v e. _V
3 hashsng 
 |-  ( v e. _V -> ( # ` { v } ) = 1 )
4 1ne2 
 |-  1 =/= 2
5 4 neii 
 |-  -. 1 = 2
6 eqeq1 
 |-  ( ( # ` { v } ) = 1 -> ( ( # ` { v } ) = 2 <-> 1 = 2 ) )
7 5 6 mtbiri 
 |-  ( ( # ` { v } ) = 1 -> -. ( # ` { v } ) = 2 )
8 2 3 7 mp2b 
 |-  -. ( # ` { v } ) = 2
9 fveqeq2 
 |-  ( C = { v } -> ( ( # ` C ) = 2 <-> ( # ` { v } ) = 2 ) )
10 8 9 mtbiri 
 |-  ( C = { v } -> -. ( # ` C ) = 2 )
11 10 intnand 
 |-  ( C = { v } -> -. ( C e. ~P ( Vtx ` G ) /\ ( # ` C ) = 2 ) )
12 1 eleq2i 
 |-  ( C e. E <-> C e. ( Edg ` G ) )
13 edgumgr 
 |-  ( ( G e. UMGraph /\ C e. ( Edg ` G ) ) -> ( C e. ~P ( Vtx ` G ) /\ ( # ` C ) = 2 ) )
14 12 13 sylan2b 
 |-  ( ( G e. UMGraph /\ C e. E ) -> ( C e. ~P ( Vtx ` G ) /\ ( # ` C ) = 2 ) )
15 11 14 nsyl3 
 |-  ( ( G e. UMGraph /\ C e. E ) -> -. C = { v } )
16 15 nexdv 
 |-  ( ( G e. UMGraph /\ C e. E ) -> -. E. v C = { v } )