This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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