This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ ℤ≥ : ℤ ⟶ 𝒫 ℤ