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 ⊢ x ∈ ℕ 0 → x ∈ ℤ
3 zre ⊢ x ∈ ℤ → x ∈ ℝ
4 rexr ⊢ x ∈ ℝ → x ∈ ℝ *
5 2 3 4 3syl ⊢ x ∈ ℕ 0 → x ∈ ℝ *
6 nn0ge0 ⊢ x ∈ ℕ 0 → 0 ≤ x
7 elxrge0 ⊢ x ∈ 0 +∞ ↔ x ∈ ℝ * ∧ 0 ≤ x
8 5 6 7 sylanbrc ⊢ x ∈ ℕ 0 → x ∈ 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 +∞