Metamath Proof Explorer
Theorem uzf
Description: The domain and codomain of the upper integers function. (Contributed by Scott Fenton, 8-Aug-2013) (Revised by Mario Carneiro, 3-Nov-2013)
|
|
Ref |
Expression |
|
Assertion |
uzf |
⊢ ℤ≥ : ℤ ⟶ 𝒫 ℤ |
Proof
Step |
Hyp |
Ref |
Expression |
1 |
|
zex |
⊢ ℤ ∈ V |
2 |
|
ssrab2 |
⊢ { 𝑘 ∈ ℤ ∣ 𝑗 ≤ 𝑘 } ⊆ ℤ |
3 |
1 2
|
elpwi2 |
⊢ { 𝑘 ∈ ℤ ∣ 𝑗 ≤ 𝑘 } ∈ 𝒫 ℤ |
4 |
3
|
rgenw |
⊢ ∀ 𝑗 ∈ ℤ { 𝑘 ∈ ℤ ∣ 𝑗 ≤ 𝑘 } ∈ 𝒫 ℤ |
5 |
|
df-uz |
⊢ ℤ≥ = ( 𝑗 ∈ ℤ ↦ { 𝑘 ∈ ℤ ∣ 𝑗 ≤ 𝑘 } ) |
6 |
5
|
fmpt |
⊢ ( ∀ 𝑗 ∈ ℤ { 𝑘 ∈ ℤ ∣ 𝑗 ≤ 𝑘 } ∈ 𝒫 ℤ ↔ ℤ≥ : ℤ ⟶ 𝒫 ℤ ) |
7 |
4 6
|
mpbi |
⊢ ℤ≥ : ℤ ⟶ 𝒫 ℤ |