Theorem hashf2

Description: Lemma for hasheuni . (Contributed by Thierry Arnoux, 19-Nov-2016)

	Ref	Expression
Assertion	hashf2	⊢ ♯ : V ⟶ ( 0 [,] +∞ )

Proof

Step	Hyp	Ref	Expression
1		hashf	⊢ ♯ : V ⟶ ( ℕ0 ∪ { +∞ } )
2		nn0z	⊢ ( 𝑥 ∈ ℕ0 → 𝑥 ∈ ℤ )
3		zre	⊢ ( 𝑥 ∈ ℤ → 𝑥 ∈ ℝ )
4		rexr	⊢ ( 𝑥 ∈ ℝ → 𝑥 ∈ ℝ* )
5	2 3 4	3syl	⊢ ( 𝑥 ∈ ℕ0 → 𝑥 ∈ ℝ* )
6		nn0ge0	⊢ ( 𝑥 ∈ ℕ0 → 0 ≤ 𝑥 )
7		elxrge0	⊢ ( 𝑥 ∈ ( 0 [,] +∞ ) ↔ ( 𝑥 ∈ ℝ* ∧ 0 ≤ 𝑥 ) )
8	5 6 7	sylanbrc	⊢ ( 𝑥 ∈ ℕ0 → 𝑥 ∈ ( 0 [,] +∞ ) )
9	8	ssriv	⊢ ℕ0 ⊆ ( 0 [,] +∞ )
10		0xr	⊢ 0 ∈ ℝ*
11		pnfxr	⊢ +∞ ∈ ℝ*
12		0lepnf	⊢ 0 ≤ +∞
13		ubicc2	⊢ ( ( 0 ∈ ℝ* ∧ +∞ ∈ ℝ* ∧ 0 ≤ +∞ ) → +∞ ∈ ( 0 [,] +∞ ) )
14	10 11 12 13	mp3an	⊢ +∞ ∈ ( 0 [,] +∞ )
15		snssi	⊢ ( +∞ ∈ ( 0 [,] +∞ ) → { +∞ } ⊆ ( 0 [,] +∞ ) )
16	14 15	ax-mp	⊢ { +∞ } ⊆ ( 0 [,] +∞ )
17	9 16	unssi	⊢ ( ℕ0 ∪ { +∞ } ) ⊆ ( 0 [,] +∞ )
18		fss	⊢ ( ( ♯ : V ⟶ ( ℕ0 ∪ { +∞ } ) ∧ ( ℕ0 ∪ { +∞ } ) ⊆ ( 0 [,] +∞ ) ) → ♯ : V ⟶ ( 0 [,] +∞ ) )
19	1 17 18	mp2an	⊢ ♯ : V ⟶ ( 0 [,] +∞ )