This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem vtxdgelxnn0

Description: The degree of a vertex is either a nonnegative integer or positive infinity. (Contributed by Alexander van der Vekens, 30-Dec-2017) (Revised by AV, 10-Dec-2020) (Revised by AV, 22-Mar-2021)

Ref Expression
Hypothesis vtxdgf.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
Assertion vtxdgelxnn0 ( 𝑋 ∈ 𝑉 → ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑋 ) ∈ ℕ0* )

Proof

Step Hyp Ref Expression
1 vtxdgf.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2 1 1vgrex ⊢ ( 𝑋 ∈ 𝑉 → 𝐺 ∈ V )
3 1 vtxdgf ⊢ ( 𝐺 ∈ V → ( VtxDeg ‘ 𝐺 ) : 𝑉 ⟶ ℕ0* )
4 3 ffvelcdmda ⊢ ( ( 𝐺 ∈ V ∧ 𝑋 ∈ 𝑉 ) → ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑋 ) ∈ ℕ0* )
5 2 4 mpancom ⊢ ( 𝑋 ∈ 𝑉 → ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑋 ) ∈ ℕ0* )