Theorem uspgrloopvtx

Description: The set of vertices in a graph (simple pseudograph) with one edge which is a loop (see uspgr1v1eop ). (Contributed by AV, 17-Dec-2020)

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

Proof

Step	Hyp	Ref	Expression
1		uspgrloopvtx.g	$$⊢G=⟨V,\left\{⟨A,\left\{N\right\}⟩\right\}⟩$$
2	1	fveq2i	$$⊢\mathrm{Vtx}\left(G\right)=\mathrm{Vtx}\left(⟨V,\left\{⟨A,\left\{N\right\}⟩\right\}⟩\right)$$
3		snex	$$⊢\left\{⟨A,\left\{N\right\}⟩\right\}\in \mathrm{V}$$
4		opvtxfv	$$⊢\left(V\in W\wedge \left\{⟨A,\left\{N\right\}⟩\right\}\in \mathrm{V}\right)\to \mathrm{Vtx}\left(⟨V,\left\{⟨A,\left\{N\right\}⟩\right\}⟩\right)=V$$
5	3 4	mpan2	$$⊢V\in W\to \mathrm{Vtx}\left(⟨V,\left\{⟨A,\left\{N\right\}⟩\right\}⟩\right)=V$$
6	2 5	syl5eq	$$⊢V\in W\to \mathrm{Vtx}\left(G\right)=V$$