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 \in W \land A \in V \land B \in V) \to Edg (G) = \{\{A, B\}\}$

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 \in W \land A \in V \land B \in V) \to Edg (G) = ran iEdg (G)$
4	1	umgr2v2eiedg	$⊢ (V \in W \land A \in V \land B \in V) \to iEdg (G) = \{⟨0, \{A, B\}⟩, ⟨1, \{A, B\}⟩\}$
5	4	rneqd	$⊢ (V \in W \land A \in V \land B \in V) \to ran iEdg (G) = ran \{⟨0, \{A, B\}⟩, ⟨1, \{A, B\}⟩\}$
6		c0ex	$⊢ 0 \in V$
7		1ex	$⊢ 1 \in V$
8		rnpropg	$⊢ (0 \in V \land 1 \in V) \to 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 \in W \land A \in V \land B \in V) \to ran \{⟨0, \{A, B\}⟩, ⟨1, \{A, B\}⟩\} = \{\{A, B\}, \{A, B\}\}$
11		dfsn2	$⊢ \{\{A, B\}\} = \{\{A, B\}, \{A, B\}\}$
12	10 11	eqtr4di	$⊢ (V \in W \land A \in V \land B \in V) \to ran \{⟨0, \{A, B\}⟩, ⟨1, \{A, B\}⟩\} = \{\{A, B\}\}$
13	3 5 12	3eqtrd	$⊢ (V \in W \land A \in V \land B \in V) \to Edg (G) = \{\{A, B\}\}$

Metamath Proof Explorer