MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  uzf Structured version   Visualization version   GIF version

Theorem uzf 12238
Description: The domain and range 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.
StepHypRef Expression
1 zex 11982 . . . 4 ℤ ∈ V
2 ssrab2 4054 . . . 4 {𝑘 ∈ ℤ ∣ 𝑗𝑘} ⊆ ℤ
31, 2elpwi2 5240 . . 3 {𝑘 ∈ ℤ ∣ 𝑗𝑘} ∈ 𝒫 ℤ
43rgenw 3148 . 2 𝑗 ∈ ℤ {𝑘 ∈ ℤ ∣ 𝑗𝑘} ∈ 𝒫 ℤ
5 df-uz 12236 . . 3 = (𝑗 ∈ ℤ ↦ {𝑘 ∈ ℤ ∣ 𝑗𝑘})
65fmpt 6867 . 2 (∀𝑗 ∈ ℤ {𝑘 ∈ ℤ ∣ 𝑗𝑘} ∈ 𝒫 ℤ ↔ ℤ:ℤ⟶𝒫 ℤ)
74, 6mpbi 232 1 :ℤ⟶𝒫 ℤ
Colors of variables: wff setvar class
Syntax hints:  wcel 2107  wral 3136  {crab 3140  Vcvv 3493  𝒫 cpw 4537   class class class wbr 5057  wf 6344  cle 10668  cz 11973  cuz 12235
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-ext 2791  ax-sep 5194  ax-nul 5201  ax-pr 5320  ax-cnex 10585  ax-resscn 10586
This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1082  df-3an 1083  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-mo 2616  df-eu 2648  df-clab 2798  df-cleq 2812  df-clel 2891  df-nfc 2961  df-ne 3015  df-ral 3141  df-rex 3142  df-rab 3145  df-v 3495  df-sbc 3771  df-dif 3937  df-un 3939  df-in 3941  df-ss 3950  df-nul 4290  df-if 4466  df-pw 4539  df-sn 4560  df-pr 4562  df-op 4566  df-uni 4831  df-br 5058  df-opab 5120  df-mpt 5138  df-id 5453  df-xp 5554  df-rel 5555  df-cnv 5556  df-co 5557  df-dm 5558  df-rn 5559  df-res 5560  df-ima 5561  df-iota 6307  df-fun 6350  df-fn 6351  df-f 6352  df-fv 6356  df-ov 7151  df-neg 10865  df-z 11974  df-uz 12236
This theorem is referenced by:  eluzel2  12240  uzn0  12252  uzssz  12256  ltweuz  13321  uzin2  14696  rexanuz  14697  sumz  15071  sumss  15073  prod1  15290  prodss  15293  lmbr2  21859  lmff  21901  zfbas  22496  uzrest  22497  lmflf  22605  lmmbr2  23854  caucfil  23878  lmcau  23908  heibor1lem  35074  dmuz  41488
  Copyright terms: Public domain W3C validator