Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > uzf | Structured version Visualization version GIF version |
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 |
---|---|
uzf | ⊢ ℤ≥:ℤ⟶𝒫 ℤ |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | zex 12072 | . . . 4 ⊢ ℤ ∈ V | |
2 | ssrab2 3970 | . . . 4 ⊢ {𝑘 ∈ ℤ ∣ 𝑗 ≤ 𝑘} ⊆ ℤ | |
3 | 1, 2 | elpwi2 5215 | . . 3 ⊢ {𝑘 ∈ ℤ ∣ 𝑗 ≤ 𝑘} ∈ 𝒫 ℤ |
4 | 3 | rgenw 3065 | . 2 ⊢ ∀𝑗 ∈ ℤ {𝑘 ∈ ℤ ∣ 𝑗 ≤ 𝑘} ∈ 𝒫 ℤ |
5 | df-uz 12326 | . . 3 ⊢ ℤ≥ = (𝑗 ∈ ℤ ↦ {𝑘 ∈ ℤ ∣ 𝑗 ≤ 𝑘}) | |
6 | 5 | fmpt 6885 | . 2 ⊢ (∀𝑗 ∈ ℤ {𝑘 ∈ ℤ ∣ 𝑗 ≤ 𝑘} ∈ 𝒫 ℤ ↔ ℤ≥:ℤ⟶𝒫 ℤ) |
7 | 4, 6 | mpbi 233 | 1 ⊢ ℤ≥:ℤ⟶𝒫 ℤ |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 2113 ∀wral 3053 {crab 3057 Vcvv 3398 𝒫 cpw 4489 class class class wbr 5031 ⟶wf 6336 ≤ cle 10755 ℤcz 12063 ℤ≥cuz 12325 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1802 ax-4 1816 ax-5 1916 ax-6 1974 ax-7 2019 ax-8 2115 ax-9 2123 ax-10 2144 ax-11 2161 ax-12 2178 ax-ext 2710 ax-sep 5168 ax-nul 5175 ax-pr 5297 ax-cnex 10672 ax-resscn 10673 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 847 df-3or 1089 df-3an 1090 df-tru 1545 df-fal 1555 df-ex 1787 df-nf 1791 df-sb 2074 df-mo 2540 df-eu 2570 df-clab 2717 df-cleq 2730 df-clel 2811 df-nfc 2881 df-ral 3058 df-rex 3059 df-rab 3062 df-v 3400 df-dif 3847 df-un 3849 df-in 3851 df-ss 3861 df-nul 4213 df-if 4416 df-pw 4491 df-sn 4518 df-pr 4520 df-op 4524 df-uni 4798 df-br 5032 df-opab 5094 df-mpt 5112 df-id 5430 df-xp 5532 df-rel 5533 df-cnv 5534 df-co 5535 df-dm 5536 df-rn 5537 df-res 5538 df-ima 5539 df-iota 6298 df-fun 6342 df-fn 6343 df-f 6344 df-fv 6348 df-ov 7174 df-neg 10952 df-z 12064 df-uz 12326 |
This theorem is referenced by: eluzel2 12330 uzn0 12342 uzssz 12346 ltweuz 13421 uzin2 14795 rexanuz 14796 sumz 15173 sumss 15175 prod1 15391 prodss 15394 lmbr2 22011 lmff 22053 zfbas 22648 uzrest 22649 lmflf 22757 lmmbr2 24012 caucfil 24036 lmcau 24066 heibor1lem 35587 dmuz 42307 |
Copyright terms: Public domain | W3C validator |