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 } } = (/) )