Theorem uspgrloopiedg

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, 21-Feb-2021)

	Ref	Expression
Hypothesis	uspgrloopvtx.g	$$⊢G=⟨V,\left\{⟨A,\left\{N\right\}⟩\right\}⟩$$
Assertion	uspgrloopiedg	$$⊢\left(V\in W\wedge A\in X\right)\to \mathrm{iEdg}\left(G\right)=\left\{⟨A,\left\{N\right\}⟩\right\}$$

Proof

Step	Hyp	Ref	Expression
1		uspgrloopvtx.g	$$⊢G=⟨V,\left\{⟨A,\left\{N\right\}⟩\right\}⟩$$
2	1	fveq2i	$$⊢\mathrm{iEdg}\left(G\right)=\mathrm{iEdg}\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		opiedgfv	$$⊢\left(V\in W\wedge \left\{⟨A,\left\{N\right\}⟩\right\}\in \mathrm{V}\right)\to \mathrm{iEdg}\left(⟨V,\left\{⟨A,\left\{N\right\}⟩\right\}⟩\right)=\left\{⟨A,\left\{N\right\}⟩\right\}$$
6	4 5	sylan2	$$⊢\left(V\in W\wedge A\in X\right)\to \mathrm{iEdg}\left(⟨V,\left\{⟨A,\left\{N\right\}⟩\right\}⟩\right)=\left\{⟨A,\left\{N\right\}⟩\right\}$$
7	2 6	syl5eq	$$⊢\left(V\in W\wedge A\in X\right)\to \mathrm{iEdg}\left(G\right)=\left\{⟨A,\left\{N\right\}⟩\right\}$$