Theorem umgr2v2eiedg

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

	Ref	Expression
Hypothesis	umgr2v2evtx.g	$$⊢G=⟨V,\left\{⟨0,\left\{A,B\right\}⟩,⟨1,\left\{A,B\right\}⟩\right\}⟩$$
Assertion	umgr2v2eiedg	$$⊢\left(V\in W\wedge A\in V\wedge B\in V\right)\to \mathrm{iEdg}\left(G\right)=\left\{⟨0,\left\{A,B\right\}⟩,⟨1,\left\{A,B\right\}⟩\right\}$$

Proof

Step	Hyp	Ref	Expression
1		umgr2v2evtx.g	$$⊢G=⟨V,\left\{⟨0,\left\{A,B\right\}⟩,⟨1,\left\{A,B\right\}⟩\right\}⟩$$
2	1	fveq2i	$$⊢\mathrm{iEdg}\left(G\right)=\mathrm{iEdg}\left(⟨V,\left\{⟨0,\left\{A,B\right\}⟩,⟨1,\left\{A,B\right\}⟩\right\}⟩\right)$$
3		simp1	$$⊢\left(V\in W\wedge A\in V\wedge B\in V\right)\to V\in W$$
4		prex	$$⊢\left\{⟨0,\left\{A,B\right\}⟩,⟨1,\left\{A,B\right\}⟩\right\}\in \mathrm{V}$$
5		opiedgfv	$$⊢\left(V\in W\wedge \left\{⟨0,\left\{A,B\right\}⟩,⟨1,\left\{A,B\right\}⟩\right\}\in \mathrm{V}\right)\to \mathrm{iEdg}\left(⟨V,\left\{⟨0,\left\{A,B\right\}⟩,⟨1,\left\{A,B\right\}⟩\right\}⟩\right)=\left\{⟨0,\left\{A,B\right\}⟩,⟨1,\left\{A,B\right\}⟩\right\}$$
6	3 4 5	sylancl	$$⊢\left(V\in W\wedge A\in V\wedge B\in V\right)\to \mathrm{iEdg}\left(⟨V,\left\{⟨0,\left\{A,B\right\}⟩,⟨1,\left\{A,B\right\}⟩\right\}⟩\right)=\left\{⟨0,\left\{A,B\right\}⟩,⟨1,\left\{A,B\right\}⟩\right\}$$
7	2 6	syl5eq	$$⊢\left(V\in W\wedge A\in V\wedge B\in V\right)\to \mathrm{iEdg}\left(G\right)=\left\{⟨0,\left\{A,B\right\}⟩,⟨1,\left\{A,B\right\}⟩\right\}$$