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 ⊢ V = Vtx ⁡ G
Assertion vtxdgfusgr ⊢ G ∈ FinUSGraph → ∀ v ∈ V VtxDeg ⁡ G ⁡ v ∈ ℕ 0

Proof

Step Hyp Ref Expression
1 vtxdgfusgrf.v ⊢ V = Vtx ⁡ G
2 1 vtxdgfusgrf ⊢ G ∈ FinUSGraph → VtxDeg ⁡ G : V ⟶ ℕ 0
3 2 ffvelcdmda ⊢ G ∈ FinUSGraph ∧ v ∈ V → VtxDeg ⁡ G ⁡ v ∈ ℕ 0
4 3 ralrimiva ⊢ G ∈ FinUSGraph → ∀ v ∈ V VtxDeg ⁡ G ⁡ v ∈ ℕ 0