Metamath Proof Explorer

Theorem umgrnloopv

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

Ref Expression
Hypothesis umgrnloopv.e ⊢ E = iEdg ⁡ G
Assertion umgrnloopv ⊢ G ∈ UMGraph ∧ M ∈ W → E ⁡ X = M N → M ≠ N

Proof

Step Hyp Ref Expression
1 umgrnloopv.e ⊢ E = iEdg ⁡ G
2 prnzg ⊢ M ∈ W → M N ≠ ∅
3 2 adantl ⊢ E ⁡ X = M N ∧ M ∈ W → M N ≠ ∅
4 neeq1 ⊢ E ⁡ X = M N → E ⁡ X ≠ ∅ ↔ M N ≠ ∅
5 4 adantr ⊢ E ⁡ X = M N ∧ M ∈ W → E ⁡ X ≠ ∅ ↔ M N ≠ ∅
6 3 5 mpbird ⊢ E ⁡ X = M N ∧ M ∈ W → E ⁡ X ≠ ∅
7 fvfundmfvn0 ⊢ E ⁡ X ≠ ∅ → X ∈ dom ⁡ E ∧ Fun ⁡ E ↾ X
8 6 7 syl ⊢ E ⁡ X = M N ∧ M ∈ W → X ∈ dom ⁡ E ∧ Fun ⁡ E ↾ X
9 eqid ⊢ Vtx ⁡ G = Vtx ⁡ G
10 9 1 umgredg2 ⊢ G ∈ UMGraph ∧ X ∈ dom ⁡ E → E ⁡ X = 2
11 fveqeq2 ⊢ E ⁡ X = M N → E ⁡ X = 2 ↔ M N = 2
12 eqid ⊢ M N = M N
13 12 hashprdifel ⊢ M N = 2 → M ∈ M N ∧ N ∈ M N ∧ M ≠ N
14 13 simp3d ⊢ M N = 2 → M ≠ N
15 11 14 biimtrdi ⊢ E ⁡ X = M N → E ⁡ X = 2 → M ≠ N
16 15 adantr ⊢ E ⁡ X = M N ∧ M ∈ W → E ⁡ X = 2 → M ≠ N
17 10 16 syl5com ⊢ G ∈ UMGraph ∧ X ∈ dom ⁡ E → E ⁡ X = M N ∧ M ∈ W → M ≠ N
18 17 expcom ⊢ X ∈ dom ⁡ E → G ∈ UMGraph → E ⁡ X = M N ∧ M ∈ W → M ≠ N
19 18 com23 ⊢ X ∈ dom ⁡ E → E ⁡ X = M N ∧ M ∈ W → G ∈ UMGraph → M ≠ N
20 19 adantr ⊢ X ∈ dom ⁡ E ∧ Fun ⁡ E ↾ X → E ⁡ X = M N ∧ M ∈ W → G ∈ UMGraph → M ≠ N
21 8 20 mpcom ⊢ E ⁡ X = M N ∧ M ∈ W → G ∈ UMGraph → M ≠ N
22 21 ex ⊢ E ⁡ X = M N → M ∈ W → G ∈ UMGraph → M ≠ N
23 22 com13 ⊢ G ∈ UMGraph → M ∈ W → E ⁡ X = M N → M ≠ N
24 23 imp ⊢ G ∈ UMGraph ∧ M ∈ W → E ⁡ X = M N → M ≠ N