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 )