Theorem dfnbgrss

Description: Subset chain for different kinds of neighborhoods of 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	dfnbgrss	$$⊢N\in V\to \left(G\mathrm{NeighbVtx}N\subseteq S\wedge S\subseteq GClNeighbVtxN\right)$$

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	dfnbgr5	$$⊢N\in V\to G\mathrm{NeighbVtx}N=S\setminus \left\{N\right\}$$
5		difss	$$⊢S\setminus \left\{N\right\}\subseteq S$$
6	4 5	eqsstrdi	$$⊢N\in V\to G\mathrm{NeighbVtx}N\subseteq S$$
7		ssun2	$$⊢S\subseteq \left\{N\right\}\cup S$$
8	1 2 3	dfclnbgr5	$$⊢N\in V\to GClNeighbVtxN=\left\{N\right\}\cup S$$
9	7 8	sseqtrrid	$$⊢N\in V\to S\subseteq GClNeighbVtxN$$
10	6 9	jca	$$⊢N\in V\to \left(G\mathrm{NeighbVtx}N\subseteq S\wedge S\subseteq GClNeighbVtxN\right)$$