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	$$⊢\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	1loopgredg	$$⊢\phi \to \mathrm{Edg}\left(G\right)=\left\{\left\{N\right\}\right\}$$

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		edgval	$$⊢\mathrm{Edg}\left(G\right)=\mathrm{ran}\mathrm{iEdg}\left(G\right)$$
6	5	a1i	$$⊢\phi \to \mathrm{Edg}\left(G\right)=\mathrm{ran}\mathrm{iEdg}\left(G\right)$$
7	4	rneqd	$$⊢\phi \to \mathrm{ran}\mathrm{iEdg}\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	2 8	syl	$$⊢\phi \to \mathrm{ran}\left\{⟨A,\left\{N\right\}⟩\right\}=\left\{\left\{N\right\}\right\}$$
10	6 7 9	3eqtrd	$$⊢\phi \to \mathrm{Edg}\left(G\right)=\left\{\left\{N\right\}\right\}$$