Metamath Proof Explorer

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

Proof

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 e. W /\ A e. V /\ B e. V ) -> ( Edg ` G ) = ran ( iEdg ` G ) )
4 1 umgr2v2eiedg 
 |-  ( ( V e. W /\ A e. V /\ B e. V ) -> ( iEdg ` G ) = { <. 0 , { A , B } >. , <. 1 , { A , B } >. } )
5 4 rneqd 
 |-  ( ( V e. W /\ A e. V /\ B e. V ) -> ran ( iEdg ` G ) = ran { <. 0 , { A , B } >. , <. 1 , { A , B } >. } )
6 c0ex 
 |-  0 e. _V
7 1ex 
 |-  1 e. _V
8 rnpropg 
 |-  ( ( 0 e. _V /\ 1 e. _V ) -> 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 e. W /\ A e. V /\ B e. V ) -> ran { <. 0 , { A , B } >. , <. 1 , { A , B } >. } = { { A , B } , { A , B } } )
11 dfsn2 
 |-  { { A , B } } = { { A , B } , { A , B } }
12 10 11 eqtr4di 
 |-  ( ( V e. W /\ A e. V /\ B e. V ) -> ran { <. 0 , { A , B } >. , <. 1 , { A , B } >. } = { { A , B } } )
13 3 5 12 3eqtrd 
 |-  ( ( V e. W /\ A e. V /\ B e. V ) -> ( Edg ` G ) = { { A , B } } )