Theorem vtxdgfusgrf

Description: The vertex degree function on finite simple graphs is a function from vertices to nonnegative integers. (Contributed by AV, 12-Dec-2020)

	Ref	Expression
Hypothesis	vtxdgfusgrf.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
Assertion	vtxdgfusgrf	⊢ ( 𝐺 ∈ FinUSGraph → ( VtxDeg ‘ 𝐺 ) : 𝑉 ⟶ ℕ0 )

Proof

Step	Hyp	Ref	Expression
1		vtxdgfusgrf.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2		fusgrfis	⊢ ( 𝐺 ∈ FinUSGraph → ( Edg ‘ 𝐺 ) ∈ Fin )
3		fusgrusgr	⊢ ( 𝐺 ∈ FinUSGraph → 𝐺 ∈ USGraph )
4		eqid	⊢ ( iEdg ‘ 𝐺 ) = ( iEdg ‘ 𝐺 )
5		eqid	⊢ ( Edg ‘ 𝐺 ) = ( Edg ‘ 𝐺 )
6	4 5	usgredgffibi	⊢ ( 𝐺 ∈ USGraph → ( ( Edg ‘ 𝐺 ) ∈ Fin ↔ ( iEdg ‘ 𝐺 ) ∈ Fin ) )
7	3 6	syl	⊢ ( 𝐺 ∈ FinUSGraph → ( ( Edg ‘ 𝐺 ) ∈ Fin ↔ ( iEdg ‘ 𝐺 ) ∈ Fin ) )
8		usgrfun	⊢ ( 𝐺 ∈ USGraph → Fun ( iEdg ‘ 𝐺 ) )
9		fundmfibi	⊢ ( Fun ( iEdg ‘ 𝐺 ) → ( ( iEdg ‘ 𝐺 ) ∈ Fin ↔ dom ( iEdg ‘ 𝐺 ) ∈ Fin ) )
10	3 8 9	3syl	⊢ ( 𝐺 ∈ FinUSGraph → ( ( iEdg ‘ 𝐺 ) ∈ Fin ↔ dom ( iEdg ‘ 𝐺 ) ∈ Fin ) )
11	7 10	bitrd	⊢ ( 𝐺 ∈ FinUSGraph → ( ( Edg ‘ 𝐺 ) ∈ Fin ↔ dom ( iEdg ‘ 𝐺 ) ∈ Fin ) )
12	2 11	mpbid	⊢ ( 𝐺 ∈ FinUSGraph → dom ( iEdg ‘ 𝐺 ) ∈ Fin )
13		eqid	⊢ dom ( iEdg ‘ 𝐺 ) = dom ( iEdg ‘ 𝐺 )
14	1 4 13	vtxdgfisf	⊢ ( ( 𝐺 ∈ FinUSGraph ∧ dom ( iEdg ‘ 𝐺 ) ∈ Fin ) → ( VtxDeg ‘ 𝐺 ) : 𝑉 ⟶ ℕ0 )
15	12 14	mpdan	⊢ ( 𝐺 ∈ FinUSGraph → ( VtxDeg ‘ 𝐺 ) : 𝑉 ⟶ ℕ0 )