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	⊢ 𝐺 = ⟨ 𝑉 , { ⟨ 0 , { 𝐴 , 𝐵 } ⟩ , ⟨ 1 , { 𝐴 , 𝐵 } ⟩ } ⟩
Assertion	umgr2v2eedg	⊢ ( ( 𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) → ( Edg ‘ 𝐺 ) = { { 𝐴 , 𝐵 } } )

Proof

Step	Hyp	Ref	Expression
1		umgr2v2evtx.g	⊢ 𝐺 = ⟨ 𝑉 , { ⟨ 0 , { 𝐴 , 𝐵 } ⟩ , ⟨ 1 , { 𝐴 , 𝐵 } ⟩ } ⟩
2		edgval	⊢ ( Edg ‘ 𝐺 ) = ran ( iEdg ‘ 𝐺 )
3	2	a1i	⊢ ( ( 𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) → ( Edg ‘ 𝐺 ) = ran ( iEdg ‘ 𝐺 ) )
4	1	umgr2v2eiedg	⊢ ( ( 𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) → ( iEdg ‘ 𝐺 ) = { ⟨ 0 , { 𝐴 , 𝐵 } ⟩ , ⟨ 1 , { 𝐴 , 𝐵 } ⟩ } )
5	4	rneqd	⊢ ( ( 𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) → ran ( iEdg ‘ 𝐺 ) = ran { ⟨ 0 , { 𝐴 , 𝐵 } ⟩ , ⟨ 1 , { 𝐴 , 𝐵 } ⟩ } )
6		c0ex	⊢ 0 ∈ V
7		1ex	⊢ 1 ∈ V
8		rnpropg	⊢ ( ( 0 ∈ V ∧ 1 ∈ V ) → ran { ⟨ 0 , { 𝐴 , 𝐵 } ⟩ , ⟨ 1 , { 𝐴 , 𝐵 } ⟩ } = { { 𝐴 , 𝐵 } , { 𝐴 , 𝐵 } } )
9	6 7 8	mp2an	⊢ ran { ⟨ 0 , { 𝐴 , 𝐵 } ⟩ , ⟨ 1 , { 𝐴 , 𝐵 } ⟩ } = { { 𝐴 , 𝐵 } , { 𝐴 , 𝐵 } }
10	9	a1i	⊢ ( ( 𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) → ran { ⟨ 0 , { 𝐴 , 𝐵 } ⟩ , ⟨ 1 , { 𝐴 , 𝐵 } ⟩ } = { { 𝐴 , 𝐵 } , { 𝐴 , 𝐵 } } )
11		dfsn2	⊢ { { 𝐴 , 𝐵 } } = { { 𝐴 , 𝐵 } , { 𝐴 , 𝐵 } }
12	10 11	eqtr4di	⊢ ( ( 𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) → ran { ⟨ 0 , { 𝐴 , 𝐵 } ⟩ , ⟨ 1 , { 𝐴 , 𝐵 } ⟩ } = { { 𝐴 , 𝐵 } } )
13	3 5 12	3eqtrd	⊢ ( ( 𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) → ( Edg ‘ 𝐺 ) = { { 𝐴 , 𝐵 } } )