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

Metamath Proof Explorer

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 ffvelcdmd ⊢ ( 𝑀 ∈ 𝑉 → ( ♯ ‘ 𝑀 ) ∈ ℕ0* )