Theorem 1loopgruspgr

Description: A graph with one edge which is a loop is a simple pseudograph (see also uspgr1v1eop ). (Contributed 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	1loopgruspgr	|- ( ph -> G e. USPGraph )

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		eqid	|- ( Vtx ` G ) = ( Vtx ` G )
6	3 1	eleqtrrd	|- ( ph -> N e. ( Vtx ` G ) )
7		dfsn2	|- { N } = { N , N }
8	7	a1i	|- ( ph -> { N } = { N , N } )
9	8	opeq2d	|- ( ph -> <. A , { N } >. = <. A , { N , N } >. )
10	9	sneqd	|- ( ph -> { <. A , { N } >. } = { <. A , { N , N } >. } )
11	4 10	eqtrd	|- ( ph -> ( iEdg ` G ) = { <. A , { N , N } >. } )
12	5 2 6 6 11	uspgr1e	|- ( ph -> G e. USPGraph )