Theorem uzf 12785

Description: The domain and codomain of the upper integers function. (Contributed by Scott Fenton, 8-Aug-2013.) (Revised by Mario Carneiro, 3-Nov-2013.)

Assertion

Ref	Expression
uzf	⊢ ℤ≥:ℤ⟶𝒫 ℤ

Proof of Theorem uzf

Dummy variables 𝑗 𝑘 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		zex 12527	. . . 4 ⊢ ℤ ∈ V
2		ssrab2 4014	. . . 4 ⊢ {𝑘 ∈ ℤ ∣ 𝑗 ≤ 𝑘} ⊆ ℤ
3	1, 2	elpwi2 5266	. . 3 ⊢ {𝑘 ∈ ℤ ∣ 𝑗 ≤ 𝑘} ∈ 𝒫 ℤ
4	3	rgenw 3054	. 2 ⊢ ∀𝑗 ∈ ℤ {𝑘 ∈ ℤ ∣ 𝑗 ≤ 𝑘} ∈ 𝒫 ℤ
5		df-uz 12783	. . 3 ⊢ ℤ≥ = (𝑗 ∈ ℤ ↦ {𝑘 ∈ ℤ ∣ 𝑗 ≤ 𝑘})
6	5	fmpt 7054	. 2 ⊢ (∀𝑗 ∈ ℤ {𝑘 ∈ ℤ ∣ 𝑗 ≤ 𝑘} ∈ 𝒫 ℤ ↔ ℤ≥:ℤ⟶𝒫 ℤ)
7	4, 6	mpbi 231	1 ⊢ ℤ≥:ℤ⟶𝒫 ℤ

Syntax hints:   ∈ wcel 2115  ∀wral 3050  {crab 3388  Vcvv 3428  𝒫 cpw 4532   class class class wbr 5075  ⟶wf 6484   ≤ cle 11174  ℤcz 12518  ℤ_≥cuz 12782

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1970  ax-7 2011  ax-8 2117  ax-9 2125  ax-10 2148  ax-11 2164  ax-12 2185  ax-ext 2708  ax-sep 5221  ax-pr 5365  ax-cnex 11088  ax-resscn 11089

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 850  df-3or 1089  df-3an 1090  df-tru 1546  df-fal 1556  df-ex 1783  df-nf 1787  df-sb 2070  df-mo 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-ral 3051  df-rex 3061  df-rab 3389  df-v 3430  df-dif 3889  df-un 3891  df-in 3893  df-ss 3903  df-nul 4265  df-if 4458  df-pw 4534  df-sn 4559  df-pr 4561  df-op 4565  df-uni 4842  df-br 5076  df-opab 5138  df-mpt 5157  df-id 5516  df-xp 5627  df-rel 5628  df-cnv 5629  df-co 5630  df-dm 5631  df-rn 5632  df-res 5633  df-ima 5634  df-iota 6444  df-fun 6490  df-fn 6491  df-f 6492  df-fv 6496  df-ov 7362  df-neg 11374  df-z 12519  df-uz 12783

This theorem is referenced by:  eluzel2  12787  uzn0  12799  uzssz  12803  ltweuz  13917  uzin2  15301  rexanuz  15302  sumz  15678  sumss  15680  prod1  15903  prodss  15906  lmbr2  23245  lmff  23287  zfbas  23882  uzrest  23883  lmflf  23991  lmmbr2  25247  caucfil  25271  lmcau  25301  heibor1lem  38173  dmuz  45675