Metamath Proof Explorer

Theorem umgr2v2eedg

Description: The set of edges in a multigraph with two edges connecting the same two vertices. (Contributed by AV, 17-Dec-2020)

Ref Expression
Hypothesis umgr2v2evtx.g ⊢ G = V 0 A B 1 A B
Assertion umgr2v2eedg ⊢ V ∈ W ∧ A ∈ V ∧ B ∈ V → Edg ⁡ G = A B

Proof

Step Hyp Ref Expression
1 umgr2v2evtx.g ⊢ G = V 0 A B 1 A B
2 edgval ⊢ Edg ⁡ G = ran ⁡ iEdg ⁡ G
3 2 a1i ⊢ V ∈ W ∧ A ∈ V ∧ B ∈ V → Edg ⁡ G = ran ⁡ iEdg ⁡ G
4 1 umgr2v2eiedg ⊢ V ∈ W ∧ A ∈ V ∧ B ∈ V → iEdg ⁡ G = 0 A B 1 A B
5 4 rneqd ⊢ V ∈ W ∧ A ∈ V ∧ B ∈ V → ran ⁡ iEdg ⁡ G = ran ⁡ 0 A B 1 A B
6 c0ex ⊢ 0 ∈ V
7 1ex ⊢ 1 ∈ V
8 rnpropg ⊢ 0 ∈ V ∧ 1 ∈ V → ran ⁡ 0 A B 1 A B = A B A B
9 6 7 8 mp2an ⊢ ran ⁡ 0 A B 1 A B = A B A B
10 9 a1i ⊢ V ∈ W ∧ A ∈ V ∧ B ∈ V → ran ⁡ 0 A B 1 A B = A B A B
11 dfsn2 ⊢ A B = A B A B
12 10 11 eqtr4di ⊢ V ∈ W ∧ A ∈ V ∧ B ∈ V → ran ⁡ 0 A B 1 A B = A B
13 3 5 12 3eqtrd ⊢ V ∈ W ∧ A ∈ V ∧ B ∈ V → Edg ⁡ G = A B