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 } } )