Metamath Proof Explorer


Theorem vtxdgfusgr

Description: In a finite simple graph, the degree of each vertex is finite. (Contributed by Alexander van der Vekens, 10-Mar-2018) (Revised by AV, 12-Dec-2020)

Ref Expression
Hypothesis vtxdgfusgrf.v 𝑉 = ( Vtx ‘ 𝐺 )
Assertion vtxdgfusgr ( 𝐺 ∈ FinUSGraph → ∀ 𝑣𝑉 ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) ∈ ℕ0 )

Proof

Step Hyp Ref Expression
1 vtxdgfusgrf.v 𝑉 = ( Vtx ‘ 𝐺 )
2 1 vtxdgfusgrf ( 𝐺 ∈ FinUSGraph → ( VtxDeg ‘ 𝐺 ) : 𝑉 ⟶ ℕ0 )
3 2 ffvelrnda ( ( 𝐺 ∈ FinUSGraph ∧ 𝑣𝑉 ) → ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) ∈ ℕ0 )
4 3 ralrimiva ( 𝐺 ∈ FinUSGraph → ∀ 𝑣𝑉 ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) ∈ ℕ0 )