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

Metamath Proof Explorer

Theorem nbgrssovtx

Description: The neighbors of a vertex X form a subset of all vertices except the vertex X itself. Stronger version of nbgrssvtx . (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 nbgrssovtx 
|- ( G NeighbVtx X ) C_ ( V \ { X } )

Proof

Step Hyp Ref Expression
1 nbgrssovtx.v 
 |-  V = ( Vtx ` G )
2 1 nbgrisvtx 
 |-  ( v e. ( G NeighbVtx X ) -> v e. V )
3 nbgrnself2 
 |-  X e/ ( G NeighbVtx X )
4 df-nel 
 |-  ( v e/ ( G NeighbVtx X ) <-> -. v e. ( G NeighbVtx X ) )
5 neleq1 
 |-  ( v = X -> ( v e/ ( G NeighbVtx X ) <-> X e/ ( G NeighbVtx X ) ) )
6 4 5 bitr3id 
 |-  ( v = X -> ( -. v e. ( G NeighbVtx X ) <-> X e/ ( G NeighbVtx X ) ) )
7 3 6 mpbiri 
 |-  ( v = X -> -. v e. ( G NeighbVtx X ) )
8 7 necon2ai 
 |-  ( v e. ( G NeighbVtx X ) -> v =/= X )
9 eldifsn 
 |-  ( v e. ( V \ { X } ) <-> ( v e. V /\ v =/= X ) )
10 2 8 9 sylanbrc 
 |-  ( v e. ( G NeighbVtx X ) -> v e. ( V \ { X } ) )
11 10 ssriv 
 |-  ( G NeighbVtx X ) C_ ( V \ { X } )