Theorem umgrnloop

Description: In a multigraph, there is no loop, i.e. no edge connecting a vertex with itself. (Contributed by Alexander van der Vekens, 19-Aug-2017) (Revised by AV, 11-Dec-2020)

	Ref	Expression
Hypothesis	umgrnloopv.e	|- E = ( iEdg ` G )
Assertion	umgrnloop	|- ( G e. UMGraph -> ( E. x e. dom E ( E ` x ) = { M , N } -> M =/= N ) )

Proof

Step	Hyp	Ref	Expression
1		umgrnloopv.e	|- E = ( iEdg ` G )
2		eqid	|- ( Vtx ` G ) = ( Vtx ` G )
3	1 2	umgredgprv	|- ( ( G e. UMGraph /\ x e. dom E ) -> ( ( E ` x ) = { M , N } -> ( M e. ( Vtx ` G ) /\ N e. ( Vtx ` G ) ) ) )
4	3	imp	|- ( ( ( G e. UMGraph /\ x e. dom E ) /\ ( E ` x ) = { M , N } ) -> ( M e. ( Vtx ` G ) /\ N e. ( Vtx ` G ) ) )
5	1	umgrnloopv	|- ( ( G e. UMGraph /\ M e. ( Vtx ` G ) ) -> ( ( E ` x ) = { M , N } -> M =/= N ) )
6	5	ex	|- ( G e. UMGraph -> ( M e. ( Vtx ` G ) -> ( ( E ` x ) = { M , N } -> M =/= N ) ) )
7	6	com23	|- ( G e. UMGraph -> ( ( E ` x ) = { M , N } -> ( M e. ( Vtx ` G ) -> M =/= N ) ) )
8	7	adantr	|- ( ( G e. UMGraph /\ x e. dom E ) -> ( ( E ` x ) = { M , N } -> ( M e. ( Vtx ` G ) -> M =/= N ) ) )
9	8	imp	|- ( ( ( G e. UMGraph /\ x e. dom E ) /\ ( E ` x ) = { M , N } ) -> ( M e. ( Vtx ` G ) -> M =/= N ) )
10	9	com12	|- ( M e. ( Vtx ` G ) -> ( ( ( G e. UMGraph /\ x e. dom E ) /\ ( E ` x ) = { M , N } ) -> M =/= N ) )
11	10	adantr	|- ( ( M e. ( Vtx ` G ) /\ N e. ( Vtx ` G ) ) -> ( ( ( G e. UMGraph /\ x e. dom E ) /\ ( E ` x ) = { M , N } ) -> M =/= N ) )
12	4 11	mpcom	|- ( ( ( G e. UMGraph /\ x e. dom E ) /\ ( E ` x ) = { M , N } ) -> M =/= N )
13	12	rexlimdva2	|- ( G e. UMGraph -> ( E. x e. dom E ( E ` x ) = { M , N } -> M =/= N ) )