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

Metamath Proof Explorer

Theorem hashnn0pnf

Description: The value of the hash function for a set is either a nonnegative integer or positive infinity. TODO-AV: mark as OBSOLETE and replace it by hashxnn0 ? (Contributed by Alexander van der Vekens, 6-Dec-2017)

Ref Expression
Assertion hashnn0pnf ( 𝑀 ∈ 𝑉 → ( ( ♯ ‘ 𝑀 ) ∈ ℕ0 ∨ ( ♯ ‘ 𝑀 ) = +∞ ) )

Proof

Step Hyp Ref Expression
1 hashf ⊢ ♯ : V ⟶ ( ℕ0 ∪ { +∞ } )
2 1 a1i ⊢ ( 𝑀 ∈ 𝑉 → ♯ : V ⟶ ( ℕ0 ∪ { +∞ } ) )
3 elex ⊢ ( 𝑀 ∈ 𝑉 → 𝑀 ∈ V )
4 2 3 ffvelcdmd ⊢ ( 𝑀 ∈ 𝑉 → ( ♯ ‘ 𝑀 ) ∈ ( ℕ0 ∪ { +∞ } ) )
5 elun ⊢ ( ( ♯ ‘ 𝑀 ) ∈ ( ℕ0 ∪ { +∞ } ) ↔ ( ( ♯ ‘ 𝑀 ) ∈ ℕ0 ∨ ( ♯ ‘ 𝑀 ) ∈ { +∞ } ) )
6 elsni ⊢ ( ( ♯ ‘ 𝑀 ) ∈ { +∞ } → ( ♯ ‘ 𝑀 ) = +∞ )
7 6 orim2i ⊢ ( ( ( ♯ ‘ 𝑀 ) ∈ ℕ0 ∨ ( ♯ ‘ 𝑀 ) ∈ { +∞ } ) → ( ( ♯ ‘ 𝑀 ) ∈ ℕ0 ∨ ( ♯ ‘ 𝑀 ) = +∞ ) )
8 5 7 sylbi ⊢ ( ( ♯ ‘ 𝑀 ) ∈ ( ℕ0 ∪ { +∞ } ) → ( ( ♯ ‘ 𝑀 ) ∈ ℕ0 ∨ ( ♯ ‘ 𝑀 ) = +∞ ) )
9 4 8 syl ⊢ ( 𝑀 ∈ 𝑉 → ( ( ♯ ‘ 𝑀 ) ∈ ℕ0 ∨ ( ♯ ‘ 𝑀 ) = +∞ ) )