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