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

Metamath Proof Explorer

Theorem umgrnloop0

Description: A multigraph has no loops. (Contributed by Alexander van der Vekens, 6-Dec-2017) (Revised by AV, 11-Dec-2020)

Ref Expression
Hypothesis umgrnloopv.e 
|- E = ( iEdg ` G )
Assertion umgrnloop0 
|- ( G e. UMGraph -> { x e. dom E | ( E ` x ) = { U } } = (/) )

Proof

Step Hyp Ref Expression
1 umgrnloopv.e 
 |-  E = ( iEdg ` G )
2 neirr 
 |-  -. U =/= U
3 1 umgrnloop 
 |-  ( G e. UMGraph -> ( E. x e. dom E ( E ` x ) = { U , U } -> U =/= U ) )
4 2 3 mtoi 
 |-  ( G e. UMGraph -> -. E. x e. dom E ( E ` x ) = { U , U } )
5 simpr 
 |-  ( ( G e. UMGraph /\ ( E ` x ) = { U } ) -> ( E ` x ) = { U } )
6 dfsn2 
 |-  { U } = { U , U }
7 5 6 eqtrdi 
 |-  ( ( G e. UMGraph /\ ( E ` x ) = { U } ) -> ( E ` x ) = { U , U } )
8 7 ex 
 |-  ( G e. UMGraph -> ( ( E ` x ) = { U } -> ( E ` x ) = { U , U } ) )
9 8 reximdv 
 |-  ( G e. UMGraph -> ( E. x e. dom E ( E ` x ) = { U } -> E. x e. dom E ( E ` x ) = { U , U } ) )
10 4 9 mtod 
 |-  ( G e. UMGraph -> -. E. x e. dom E ( E ` x ) = { U } )
11 ralnex 
 |-  ( A. x e. dom E -. ( E ` x ) = { U } <-> -. E. x e. dom E ( E ` x ) = { U } )
12 10 11 sylibr 
 |-  ( G e. UMGraph -> A. x e. dom E -. ( E ` x ) = { U } )
13 rabeq0 
 |-  ( { x e. dom E | ( E ` x ) = { U } } = (/) <-> A. x e. dom E -. ( E ` x ) = { U } )
14 12 13 sylibr 
 |-  ( G e. UMGraph -> { x e. dom E | ( E ` x ) = { U } } = (/) )