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

Metamath Proof Explorer

Theorem vtxdg0v

Description: The degree of a vertex in the null graph is zero (or anything else), because there are no vertices. (Contributed by AV, 11-Dec-2020)

Ref Expression
Hypothesis vtxdgf.v 
|- V = ( Vtx ` G )
Assertion vtxdg0v 
|- ( ( G = (/) /\ U e. V ) -> ( ( VtxDeg ` G ) ` U ) = 0 )

Proof

Step Hyp Ref Expression
1 vtxdgf.v 
 |-  V = ( Vtx ` G )
2 1 eleq2i 
 |-  ( U e. V <-> U e. ( Vtx ` G ) )
3 fveq2 
 |-  ( G = (/) -> ( Vtx ` G ) = ( Vtx ` (/) ) )
4 vtxval0 
 |-  ( Vtx ` (/) ) = (/)
5 3 4 eqtrdi 
 |-  ( G = (/) -> ( Vtx ` G ) = (/) )
6 5 eleq2d 
 |-  ( G = (/) -> ( U e. ( Vtx ` G ) <-> U e. (/) ) )
7 2 6 bitrid 
 |-  ( G = (/) -> ( U e. V <-> U e. (/) ) )
8 noel 
 |-  -. U e. (/)
9 8 pm2.21i 
 |-  ( U e. (/) -> ( ( VtxDeg ` G ) ` U ) = 0 )
10 7 9 biimtrdi 
 |-  ( G = (/) -> ( U e. V -> ( ( VtxDeg ` G ) ` U ) = 0 ) )
11 10 imp 
 |-  ( ( G = (/) /\ U e. V ) -> ( ( VtxDeg ` G ) ` U ) = 0 )