Theorem 1loopgredg

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

	Ref	Expression
Hypotheses	1loopgruspgr.v	|- ( ph -> ( Vtx ` G ) = V )
	1loopgruspgr.a	|- ( ph -> A e. X )
	1loopgruspgr.n	|- ( ph -> N e. V )
	1loopgruspgr.i	|- ( ph -> ( iEdg ` G ) = { <. A , { N } >. } )
Assertion	1loopgredg	|- ( ph -> ( Edg ` G ) = { { N } } )

Proof

Step	Hyp	Ref	Expression
1		1loopgruspgr.v	|- ( ph -> ( Vtx ` G ) = V )
2		1loopgruspgr.a	|- ( ph -> A e. X )
3		1loopgruspgr.n	|- ( ph -> N e. V )
4		1loopgruspgr.i	|- ( ph -> ( iEdg ` G ) = { <. A , { N } >. } )
5		edgval	|- ( Edg ` G ) = ran ( iEdg ` G )
6	5	a1i	|- ( ph -> ( Edg ` G ) = ran ( iEdg ` G ) )
7	4	rneqd	|- ( ph -> ran ( iEdg ` G ) = ran { <. A , { N } >. } )
8		rnsnopg	|- ( A e. X -> ran { <. A , { N } >. } = { { N } } )
9	2 8	syl	|- ( ph -> ran { <. A , { N } >. } = { { N } } )
10	6 7 9	3eqtrd	|- ( ph -> ( Edg ` G ) = { { N } } )