Theorem sclnbgrisvtx

Description: Every member X of the semiclosed neighborhood of a vertex N is a vertex. (Contributed by AV, 16-May-2025)

	Ref	Expression
Hypotheses	dfsclnbgr2.v	$$⊢V=\mathrm{Vtx}\left(G\right)$$
	dfsclnbgr2.s	$$⊢S=\left\{n\in V|\exists e\in E\left\{N,n\right\}\subseteq e\right\}$$
	dfsclnbgr2.e	$$⊢E=\mathrm{Edg}\left(G\right)$$
Assertion	sclnbgrisvtx	$$⊢X\in S\to X\in V$$

Proof

Step	Hyp	Ref	Expression
1		dfsclnbgr2.v	$$⊢V=\mathrm{Vtx}\left(G\right)$$
2		dfsclnbgr2.s	$$⊢S=\left\{n\in V|\exists e\in E\left\{N,n\right\}\subseteq e\right\}$$
3		dfsclnbgr2.e	$$⊢E=\mathrm{Edg}\left(G\right)$$
4	1 2 3	sclnbgrel	$$⊢X\in S\leftrightarrow \left(X\in V\wedge \exists e\in E\left\{N,X\right\}\subseteq e\right)$$
5	4	simplbi	$$⊢X\in S\to X\in V$$