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	ffvelrnd	⊢ ( 𝑀 ∈ 𝑉 → ( ♯ ‘ 𝑀 ) ∈ ( ℕ0 ∪ { +∞ } ) )
5		elun	⊢ ( ( ♯ ‘ 𝑀 ) ∈ ( ℕ0 ∪ { +∞ } ) ↔ ( ( ♯ ‘ 𝑀 ) ∈ ℕ0 ∨ ( ♯ ‘ 𝑀 ) ∈ { +∞ } ) )
6		elsni	⊢ ( ( ♯ ‘ 𝑀 ) ∈ { +∞ } → ( ♯ ‘ 𝑀 ) = +∞ )
7	6	orim2i	⊢ ( ( ( ♯ ‘ 𝑀 ) ∈ ℕ0 ∨ ( ♯ ‘ 𝑀 ) ∈ { +∞ } ) → ( ( ♯ ‘ 𝑀 ) ∈ ℕ0 ∨ ( ♯ ‘ 𝑀 ) = +∞ ) )
8	5 7	sylbi	⊢ ( ( ♯ ‘ 𝑀 ) ∈ ( ℕ0 ∪ { +∞ } ) → ( ( ♯ ‘ 𝑀 ) ∈ ℕ0 ∨ ( ♯ ‘ 𝑀 ) = +∞ ) )
9	4 8	syl	⊢ ( 𝑀 ∈ 𝑉 → ( ( ♯ ‘ 𝑀 ) ∈ ℕ0 ∨ ( ♯ ‘ 𝑀 ) = +∞ ) )