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 = ( Vtx ` G )
Assertion	nbgrssvwo2	|- ( M e/ ( G NeighbVtx X ) -> ( G NeighbVtx X ) C_ ( V \ { M , X } ) )

Proof

Step	Hyp	Ref	Expression
1		nbgrssovtx.v	|- V = ( Vtx ` G )
2	1	nbgrssovtx	|- ( G NeighbVtx X ) C_ ( V \ { X } )
3		df-nel	|- ( M e/ ( G NeighbVtx X ) <-> -. M e. ( G NeighbVtx X ) )
4		disjsn	|- ( ( ( G NeighbVtx X ) i^i { M } ) = (/) <-> -. M e. ( G NeighbVtx X ) )
5	3 4	sylbb2	|- ( M e/ ( G NeighbVtx X ) -> ( ( G NeighbVtx X ) i^i { M } ) = (/) )
6		reldisj	|- ( ( G NeighbVtx X ) C_ ( V \ { X } ) -> ( ( ( G NeighbVtx X ) i^i { M } ) = (/) <-> ( G NeighbVtx X ) C_ ( ( V \ { X } ) \ { M } ) ) )
7	5 6	imbitrid	|- ( ( G NeighbVtx X ) C_ ( V \ { X } ) -> ( M e/ ( G NeighbVtx X ) -> ( G NeighbVtx X ) C_ ( ( V \ { X } ) \ { M } ) ) )
8	2 7	ax-mp	|- ( M e/ ( G NeighbVtx X ) -> ( G NeighbVtx X ) C_ ( ( V \ { X } ) \ { M } ) )
9		prcom	|- { M , X } = { X , M }
10	9	difeq2i	|- ( V \ { M , X } ) = ( V \ { X , M } )
11		difpr	|- ( V \ { X , M } ) = ( ( V \ { X } ) \ { M } )
12	10 11	eqtri	|- ( V \ { M , X } ) = ( ( V \ { X } ) \ { M } )
13	8 12	sseqtrrdi	|- ( M e/ ( G NeighbVtx X ) -> ( G NeighbVtx X ) C_ ( V \ { M , X } ) )