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

Metamath Proof Explorer

Theorem usgrvd0nedg

Description: If a vertex in a simple graph has degree 0, the vertex is not adjacent to another vertex via an edge. (Contributed by Alexander van der Vekens, 20-Dec-2017) (Revised by AV, 16-Dec-2020) (Proof shortened by AV, 23-Dec-2020)

Ref Expression
Hypotheses vtxdusgradjvtx.v 
|- V = ( Vtx ` G )
vtxdusgradjvtx.e 
|- E = ( Edg ` G )
Assertion usgrvd0nedg 
|- ( ( G e. USGraph /\ U e. V ) -> ( ( ( VtxDeg ` G ) ` U ) = 0 -> -. E. v e. V { U , v } e. E ) )

Proof

Step Hyp Ref Expression
1 vtxdusgradjvtx.v 
 |-  V = ( Vtx ` G )
2 vtxdusgradjvtx.e 
 |-  E = ( Edg ` G )
3 1 2 vtxdusgradjvtx 
 |-  ( ( G e. USGraph /\ U e. V ) -> ( ( VtxDeg ` G ) ` U ) = ( # ` { v e. V | { U , v } e. E } ) )
4 3 eqeq1d 
 |-  ( ( G e. USGraph /\ U e. V ) -> ( ( ( VtxDeg ` G ) ` U ) = 0 <-> ( # ` { v e. V | { U , v } e. E } ) = 0 ) )
5 1 fvexi 
 |-  V e. _V
6 5 rabex 
 |-  { v e. V | { U , v } e. E } e. _V
7 hasheq0 
 |-  ( { v e. V | { U , v } e. E } e. _V -> ( ( # ` { v e. V | { U , v } e. E } ) = 0 <-> { v e. V | { U , v } e. E } = (/) ) )
8 6 7 ax-mp 
 |-  ( ( # ` { v e. V | { U , v } e. E } ) = 0 <-> { v e. V | { U , v } e. E } = (/) )
9 rabeq0 
 |-  ( { v e. V | { U , v } e. E } = (/) <-> A. v e. V -. { U , v } e. E )
10 ralnex 
 |-  ( A. v e. V -. { U , v } e. E <-> -. E. v e. V { U , v } e. E )
11 10 biimpi 
 |-  ( A. v e. V -. { U , v } e. E -> -. E. v e. V { U , v } e. E )
12 11 a1i 
 |-  ( ( G e. USGraph /\ U e. V ) -> ( A. v e. V -. { U , v } e. E -> -. E. v e. V { U , v } e. E ) )
13 9 12 biimtrid 
 |-  ( ( G e. USGraph /\ U e. V ) -> ( { v e. V | { U , v } e. E } = (/) -> -. E. v e. V { U , v } e. E ) )
14 8 13 biimtrid 
 |-  ( ( G e. USGraph /\ U e. V ) -> ( ( # ` { v e. V | { U , v } e. E } ) = 0 -> -. E. v e. V { U , v } e. E ) )
15 4 14 sylbid 
 |-  ( ( G e. USGraph /\ U e. V ) -> ( ( ( VtxDeg ` G ) ` U ) = 0 -> -. E. v e. V { U , v } e. E ) )