This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.
Database GRAPH THEORY Undirected graphs Vertex degree 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
ffvelcdmda ⊢ ( ( 𝐺 ∈ FinUSGraph ∧ 𝑣 ∈ 𝑉 ) → ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) ∈ ℕ0 )
4
3
ralrimiva ⊢ ( 𝐺 ∈ FinUSGraph → ∀ 𝑣 ∈ 𝑉 ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) ∈ ℕ0 )