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	$$⊢\phi \to \mathrm{Vtx}\left(G\right)=V$$
	1loopgruspgr.a	$$⊢\phi \to A\in X$$
	1loopgruspgr.n	$$⊢\phi \to N\in V$$
	1loopgruspgr.i	$$⊢\phi \to \mathrm{iEdg}\left(G\right)=\left\{⟨A,\left\{N\right\}⟩\right\}$$
Assertion	1loopgruspgr	$$⊢\phi \to G\in \mathrm{USHGraph}$$

Proof

Step	Hyp	Ref	Expression
1		1loopgruspgr.v	$$⊢\phi \to \mathrm{Vtx}\left(G\right)=V$$
2		1loopgruspgr.a	$$⊢\phi \to A\in X$$
3		1loopgruspgr.n	$$⊢\phi \to N\in V$$
4		1loopgruspgr.i	$$⊢\phi \to \mathrm{iEdg}\left(G\right)=\left\{⟨A,\left\{N\right\}⟩\right\}$$
5		eqid	$$⊢\mathrm{Vtx}\left(G\right)=\mathrm{Vtx}\left(G\right)$$
6	3 1	eleqtrrd	$$⊢\phi \to N\in \mathrm{Vtx}\left(G\right)$$
7		dfsn2	$$⊢\left\{N\right\}=\left\{N,N\right\}$$
8	7	a1i	$$⊢\phi \to \left\{N\right\}=\left\{N,N\right\}$$
9	8	opeq2d	$$⊢\phi \to ⟨A,\left\{N\right\}⟩=⟨A,\left\{N,N\right\}⟩$$
10	9	sneqd	$$⊢\phi \to \left\{⟨A,\left\{N\right\}⟩\right\}=\left\{⟨A,\left\{N,N\right\}⟩\right\}$$
11	4 10	eqtrd	$$⊢\phi \to \mathrm{iEdg}\left(G\right)=\left\{⟨A,\left\{N,N\right\}⟩\right\}$$
12	5 2 6 6 11	uspgr1e	$$⊢\phi \to G\in \mathrm{USHGraph}$$