Metamath Proof Explorer


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 UMGraph x 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 UMGraph x dom E E x = M N M Vtx G N Vtx G
4 3 imp G UMGraph x dom E E x = M N M Vtx G N Vtx G
5 1 umgrnloopv G UMGraph M Vtx G E x = M N M N
6 5 ex G UMGraph M Vtx G E x = M N M N
7 6 com23 G UMGraph E x = M N M Vtx G M N
8 7 adantr G UMGraph x dom E E x = M N M Vtx G M N
9 8 imp G UMGraph x dom E E x = M N M Vtx G M N
10 9 com12 M Vtx G G UMGraph x dom E E x = M N M N
11 10 adantr M Vtx G N Vtx G G UMGraph x dom E E x = M N M N
12 4 11 mpcom G UMGraph x dom E E x = M N M N
13 12 rexlimdva2 G UMGraph x dom E E x = M N M N