Theorem uzf

Description: The domain and range 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	⊢ ℤ≥ : ℤ ⟶ 𝒫 ℤ