This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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