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

Metamath Proof Explorer

Theorem vtxdgfisf

Description: The vertex degree function on graphs of finite size is a function from vertices to nonnegative integers. (Contributed by Mario Carneiro, 12-Mar-2015) (Revised by Alexander van der Vekens, 20-Dec-2017) (Revised by AV, 11-Dec-2020)

Ref Expression
Hypotheses vtxdgf.v 
|- V = ( Vtx ` G )
vtxdg0e.i 
|- I = ( iEdg ` G )
vtxdgfisnn0.a 
|- A = dom I
Assertion vtxdgfisf 
|- ( ( G e. W /\ A e. Fin ) -> ( VtxDeg ` G ) : V --> NN0 )

Proof

Step Hyp Ref Expression
1 vtxdgf.v 
 |-  V = ( Vtx ` G )
2 vtxdg0e.i 
 |-  I = ( iEdg ` G )
3 vtxdgfisnn0.a 
 |-  A = dom I
4 1 vtxdgf 
 |-  ( G e. W -> ( VtxDeg ` G ) : V --> NN0* )
5 4 adantr 
 |-  ( ( G e. W /\ A e. Fin ) -> ( VtxDeg ` G ) : V --> NN0* )
6 5 ffnd 
 |-  ( ( G e. W /\ A e. Fin ) -> ( VtxDeg ` G ) Fn V )
7 1 2 3 vtxdgfisnn0 
 |-  ( ( A e. Fin /\ u e. V ) -> ( ( VtxDeg ` G ) ` u ) e. NN0 )
8 7 adantll 
 |-  ( ( ( G e. W /\ A e. Fin ) /\ u e. V ) -> ( ( VtxDeg ` G ) ` u ) e. NN0 )
9 8 ralrimiva 
 |-  ( ( G e. W /\ A e. Fin ) -> A. u e. V ( ( VtxDeg ` G ) ` u ) e. NN0 )
10 ffnfv 
 |-  ( ( VtxDeg ` G ) : V --> NN0 <-> ( ( VtxDeg ` G ) Fn V /\ A. u e. V ( ( VtxDeg ` G ) ` u ) e. NN0 ) )
11 6 9 10 sylanbrc 
 |-  ( ( G e. W /\ A e. Fin ) -> ( VtxDeg ` G ) : V --> NN0 )