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

Metamath Proof Explorer

Theorem uspgrloopedg

Description: The set of edges in a graph (simple pseudograph) with one edge which is a loop (see uspgr1v1eop ) is a singleton of a singleton. (Contributed by AV, 17-Dec-2020)

Ref Expression
Hypothesis uspgrloopvtx.g 
|- G = <. V , { <. A , { N } >. } >.
Assertion uspgrloopedg 
|- ( ( V e. W /\ A e. X ) -> ( Edg ` G ) = { { N } } )

Proof

Step Hyp Ref Expression
1 uspgrloopvtx.g 
 |-  G = <. V , { <. A , { N } >. } >.
2 1 fveq2i 
 |-  ( Edg ` G ) = ( Edg ` <. V , { <. A , { N } >. } >. )
3 snex 
 |-  { <. A , { N } >. } e. _V
4 3 a1i 
 |-  ( A e. X -> { <. A , { N } >. } e. _V )
5 edgopval 
 |-  ( ( V e. W /\ { <. A , { N } >. } e. _V ) -> ( Edg ` <. V , { <. A , { N } >. } >. ) = ran { <. A , { N } >. } )
6 4 5 sylan2 
 |-  ( ( V e. W /\ A e. X ) -> ( Edg ` <. V , { <. A , { N } >. } >. ) = ran { <. A , { N } >. } )
7 2 6 eqtrid 
 |-  ( ( V e. W /\ A e. X ) -> ( Edg ` G ) = ran { <. A , { N } >. } )
8 rnsnopg 
 |-  ( A e. X -> ran { <. A , { N } >. } = { { N } } )
9 8 adantl 
 |-  ( ( V e. W /\ A e. X ) -> ran { <. A , { N } >. } = { { N } } )
10 7 9 eqtrd 
 |-  ( ( V e. W /\ A e. X ) -> ( Edg ` G ) = { { N } } )