Theorem uzval

Description: The value of the upper integers function. (Contributed by NM, 5-Sep-2005) (Revised by Mario Carneiro, 3-Nov-2013)

	Ref	Expression
Assertion	uzval	⊢ ( 𝑁 ∈ ℤ → ( ℤ≥ ‘ 𝑁 ) = { 𝑘 ∈ ℤ ∣ 𝑁 ≤ 𝑘 } )

Proof

Step	Hyp	Ref	Expression
1		breq1	⊢ ( 𝑗 = 𝑁 → ( 𝑗 ≤ 𝑘 ↔ 𝑁 ≤ 𝑘 ) )
2	1	rabbidv	⊢ ( 𝑗 = 𝑁 → { 𝑘 ∈ ℤ ∣ 𝑗 ≤ 𝑘 } = { 𝑘 ∈ ℤ ∣ 𝑁 ≤ 𝑘 } )
3		df-uz	⊢ ℤ≥ = ( 𝑗 ∈ ℤ ↦ { 𝑘 ∈ ℤ ∣ 𝑗 ≤ 𝑘 } )
4		zex	⊢ ℤ ∈ V
5	4	rabex	⊢ { 𝑘 ∈ ℤ ∣ 𝑁 ≤ 𝑘 } ∈ V
6	2 3 5	fvmpt	⊢ ( 𝑁 ∈ ℤ → ( ℤ≥ ‘ 𝑁 ) = { 𝑘 ∈ ℤ ∣ 𝑁 ≤ 𝑘 } )