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,\left\{⟨A,\left\{N\right\}⟩\right\}⟩$$
Assertion	uspgrloopedg	$$⊢\left(V\in W\wedge A\in X\right)\to \mathrm{Edg}\left(G\right)=\left\{\left\{N\right\}\right\}$$

Proof

Step	Hyp	Ref	Expression
1		uspgrloopvtx.g	$$⊢G=⟨V,\left\{⟨A,\left\{N\right\}⟩\right\}⟩$$
2	1	fveq2i	$$⊢\mathrm{Edg}\left(G\right)=\mathrm{Edg}\left(⟨V,\left\{⟨A,\left\{N\right\}⟩\right\}⟩\right)$$
3		snex	$$⊢\left\{⟨A,\left\{N\right\}⟩\right\}\in \mathrm{V}$$
4	3	a1i	$$⊢A\in X\to \left\{⟨A,\left\{N\right\}⟩\right\}\in \mathrm{V}$$
5		edgopval	$$⊢\left(V\in W\wedge \left\{⟨A,\left\{N\right\}⟩\right\}\in \mathrm{V}\right)\to \mathrm{Edg}\left(⟨V,\left\{⟨A,\left\{N\right\}⟩\right\}⟩\right)=\mathrm{ran}\left\{⟨A,\left\{N\right\}⟩\right\}$$
6	4 5	sylan2	$$⊢\left(V\in W\wedge A\in X\right)\to \mathrm{Edg}\left(⟨V,\left\{⟨A,\left\{N\right\}⟩\right\}⟩\right)=\mathrm{ran}\left\{⟨A,\left\{N\right\}⟩\right\}$$
7	2 6	syl5eq	$$⊢\left(V\in W\wedge A\in X\right)\to \mathrm{Edg}\left(G\right)=\mathrm{ran}\left\{⟨A,\left\{N\right\}⟩\right\}$$
8		rnsnopg	$$⊢A\in X\to \mathrm{ran}\left\{⟨A,\left\{N\right\}⟩\right\}=\left\{\left\{N\right\}\right\}$$
9	8	adantl	$$⊢\left(V\in W\wedge A\in X\right)\to \mathrm{ran}\left\{⟨A,\left\{N\right\}⟩\right\}=\left\{\left\{N\right\}\right\}$$
10	7 9	eqtrd	$$⊢\left(V\in W\wedge A\in X\right)\to \mathrm{Edg}\left(G\right)=\left\{\left\{N\right\}\right\}$$