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	ffvelrnda	⊢ ( ( 𝐺 ∈ V ∧ 𝑋 ∈ 𝑉 ) → ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑋 ) ∈ ℕ0* )
5	2 4	mpancom	⊢ ( 𝑋 ∈ 𝑉 → ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑋 ) ∈ ℕ0* )