Theorem nbgrssvwo2

Description: The neighbors of a vertex X form a subset of all vertices except the vertex X itself and a class M which is not a neighbor of X . (Contributed by Alexander van der Vekens, 13-Jul-2018) (Revised by AV, 3-Nov-2020) (Revised by AV, 12-Feb-2022)

	Ref	Expression
Hypothesis	nbgrssovtx.v	$$⊢V=\mathrm{Vtx}\left(G\right)$$
Assertion	nbgrssvwo2	$$⊢M\notin \left(G\mathrm{NeighbVtx}X\right)\to G\mathrm{NeighbVtx}X\subseteq V\setminus \left\{M,X\right\}$$

Proof

Step	Hyp	Ref	Expression
1		nbgrssovtx.v	$$⊢V=\mathrm{Vtx}\left(G\right)$$
2	1	nbgrssovtx	$$⊢G\mathrm{NeighbVtx}X\subseteq V\setminus \left\{X\right\}$$
3		df-nel	$$⊢M\notin \left(G\mathrm{NeighbVtx}X\right)\leftrightarrow \neg M\in \left(G\mathrm{NeighbVtx}X\right)$$
4		disjsn	$$⊢\left(G\mathrm{NeighbVtx}X\right)\cap \left\{M\right\}=\varnothing \leftrightarrow \neg M\in \left(G\mathrm{NeighbVtx}X\right)$$
5	3 4	sylbb2	$$⊢M\notin \left(G\mathrm{NeighbVtx}X\right)\to \left(G\mathrm{NeighbVtx}X\right)\cap \left\{M\right\}=\varnothing$$
6		reldisj	$$⊢G\mathrm{NeighbVtx}X\subseteq V\setminus \left\{X\right\}\to \left(\left(G\mathrm{NeighbVtx}X\right)\cap \left\{M\right\}=\varnothing \leftrightarrow G\mathrm{NeighbVtx}X\subseteq \left(V\setminus \left\{X\right\}\right)\setminus \left\{M\right\}\right)$$
7	5 6	imbitrid	$$⊢G\mathrm{NeighbVtx}X\subseteq V\setminus \left\{X\right\}\to \left(M\notin \left(G\mathrm{NeighbVtx}X\right)\to G\mathrm{NeighbVtx}X\subseteq \left(V\setminus \left\{X\right\}\right)\setminus \left\{M\right\}\right)$$
8	2 7	ax-mp	$$⊢M\notin \left(G\mathrm{NeighbVtx}X\right)\to G\mathrm{NeighbVtx}X\subseteq \left(V\setminus \left\{X\right\}\right)\setminus \left\{M\right\}$$
9		prcom	$$⊢\left\{M,X\right\}=\left\{X,M\right\}$$
10	9	difeq2i	$$⊢V\setminus \left\{M,X\right\}=V\setminus \left\{X,M\right\}$$
11		difpr	$$⊢V\setminus \left\{X,M\right\}=\left(V\setminus \left\{X\right\}\right)\setminus \left\{M\right\}$$
12	10 11	eqtri	$$⊢V\setminus \left\{M,X\right\}=\left(V\setminus \left\{X\right\}\right)\setminus \left\{M\right\}$$
13	8 12	sseqtrrdi	$$⊢M\notin \left(G\mathrm{NeighbVtx}X\right)\to G\mathrm{NeighbVtx}X\subseteq V\setminus \left\{M,X\right\}$$