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

Metamath Proof Explorer

Theorem nbgrnself

Description: A vertex in a graph is not a neighbor of itself. (Contributed by Alexander van der Vekens, 12-Oct-2017) (Revised by AV, 3-Nov-2020) (Revised by AV, 21-Mar-2021)

Ref Expression
Hypothesis nbgrnself.v 
|- V = ( Vtx ` G )
Assertion nbgrnself 
|- A. v e. V v e/ ( G NeighbVtx v )

Proof

Step Hyp Ref Expression
1 nbgrnself.v 
 |-  V = ( Vtx ` G )
2 neldifsnd 
 |-  ( v e. V -> -. v e. ( V \ { v } ) )
3 2 intnanrd 
 |-  ( v e. V -> -. ( v e. ( V \ { v } ) /\ E. e e. ( Edg ` G ) { v , v } C_ e ) )
4 df-nel 
 |-  ( v e/ { n e. ( V \ { v } ) | E. e e. ( Edg ` G ) { v , n } C_ e } <-> -. v e. { n e. ( V \ { v } ) | E. e e. ( Edg ` G ) { v , n } C_ e } )
5 preq2 
 |-  ( n = v -> { v , n } = { v , v } )
6 5 sseq1d 
 |-  ( n = v -> ( { v , n } C_ e <-> { v , v } C_ e ) )
7 6 rexbidv 
 |-  ( n = v -> ( E. e e. ( Edg ` G ) { v , n } C_ e <-> E. e e. ( Edg ` G ) { v , v } C_ e ) )
8 7 elrab 
 |-  ( v e. { n e. ( V \ { v } ) | E. e e. ( Edg ` G ) { v , n } C_ e } <-> ( v e. ( V \ { v } ) /\ E. e e. ( Edg ` G ) { v , v } C_ e ) )
9 4 8 xchbinx 
 |-  ( v e/ { n e. ( V \ { v } ) | E. e e. ( Edg ` G ) { v , n } C_ e } <-> -. ( v e. ( V \ { v } ) /\ E. e e. ( Edg ` G ) { v , v } C_ e ) )
10 3 9 sylibr 
 |-  ( v e. V -> v e/ { n e. ( V \ { v } ) | E. e e. ( Edg ` G ) { v , n } C_ e } )
11 eqidd 
 |-  ( v e. V -> v = v )
12 eqid 
 |-  ( Edg ` G ) = ( Edg ` G )
13 1 12 nbgrval 
 |-  ( v e. V -> ( G NeighbVtx v ) = { n e. ( V \ { v } ) | E. e e. ( Edg ` G ) { v , n } C_ e } )
14 11 13 neleq12d 
 |-  ( v e. V -> ( v e/ ( G NeighbVtx v ) <-> v e/ { n e. ( V \ { v } ) | E. e e. ( Edg ` G ) { v , n } C_ e } ) )
15 10 14 mpbird 
 |-  ( v e. V -> v e/ ( G NeighbVtx v ) )
16 15 rgen 
 |-  A. v e. V v e/ ( G NeighbVtx v )