Metamath Proof Explorer


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 syl5ib
 |-  ( ( 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 } ) )