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 , { <. 0 , { A , B } >. , <. 1 , { A , B } >. } >.
Assertion	umgr2v2eiedg	|- ( ( V e. W /\ A e. V /\ B e. V ) -> ( iEdg ` G ) = { <. 0 , { A , B } >. , <. 1 , { A , B } >. } )

Proof

Step	Hyp	Ref	Expression
1		umgr2v2evtx.g	|- G = <. V , { <. 0 , { A , B } >. , <. 1 , { A , B } >. } >.
2	1	fveq2i	|- ( iEdg ` G ) = ( iEdg ` <. V , { <. 0 , { A , B } >. , <. 1 , { A , B } >. } >. )
3		simp1	|- ( ( V e. W /\ A e. V /\ B e. V ) -> V e. W )
4		prex	|- { <. 0 , { A , B } >. , <. 1 , { A , B } >. } e. _V
5		opiedgfv	|- ( ( V e. W /\ { <. 0 , { A , B } >. , <. 1 , { A , B } >. } e. _V ) -> ( iEdg ` <. V , { <. 0 , { A , B } >. , <. 1 , { A , B } >. } >. ) = { <. 0 , { A , B } >. , <. 1 , { A , B } >. } )
6	3 4 5	sylancl	|- ( ( V e. W /\ A e. V /\ B e. V ) -> ( iEdg ` <. V , { <. 0 , { A , B } >. , <. 1 , { A , B } >. } >. ) = { <. 0 , { A , B } >. , <. 1 , { A , B } >. } )
7	2 6	syl5eq	|- ( ( V e. W /\ A e. V /\ B e. V ) -> ( iEdg ` G ) = { <. 0 , { A , B } >. , <. 1 , { A , B } >. } )