Database
GRAPH THEORY
Undirected graphs
Vertex degree
vtxdgfusgr
Metamath Proof Explorer
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 )