Theorem hashxnn0

Description: The value of the hash function for a set is an extended nonnegative integer. (Contributed by Alexander van der Vekens, 6-Dec-2017) (Revised by AV, 10-Dec-2020)

	Ref	Expression
Assertion	hashxnn0	⊢ ( 𝑀 ∈ 𝑉 → ( ♯ ‘ 𝑀 ) ∈ ℕ0* )

Proof

Step	Hyp	Ref	Expression
1		hashfxnn0	⊢ ♯ : V ⟶ ℕ0*
2	1	a1i	⊢ ( 𝑀 ∈ 𝑉 → ♯ : V ⟶ ℕ0* )
3		elex	⊢ ( 𝑀 ∈ 𝑉 → 𝑀 ∈ V )
4	2 3	ffvelrnd	⊢ ( 𝑀 ∈ 𝑉 → ( ♯ ‘ 𝑀 ) ∈ ℕ0* )