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 syl5bb
 |-  ( G = (/) -> ( U e. V <-> U e. (/) ) )
8 noel
 |-  -. U e. (/)
9 8 pm2.21i
 |-  ( U e. (/) -> ( ( VtxDeg ` G ) ` U ) = 0 )
10 7 9 syl6bi
 |-  ( G = (/) -> ( U e. V -> ( ( VtxDeg ` G ) ` U ) = 0 ) )
11 10 imp
 |-  ( ( G = (/) /\ U e. V ) -> ( ( VtxDeg ` G ) ` U ) = 0 )