Metamath Proof Explorer


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 [,] +∞ )