![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > pnfex | Structured version Visualization version GIF version |
Description: Plus infinity exists. (Contributed by David A. Wheeler, 8-Dec-2018.) (Revised by Steven Nguyen, 7-Dec-2022.) |
Ref | Expression |
---|---|
pnfex | ⊢ +∞ ∈ V |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-pnf 10482 | . 2 ⊢ +∞ = 𝒫 ∪ ℂ | |
2 | cnex 10422 | . . . 4 ⊢ ℂ ∈ V | |
3 | 2 | uniex 7289 | . . 3 ⊢ ∪ ℂ ∈ V |
4 | 3 | pwex 5138 | . 2 ⊢ 𝒫 ∪ ℂ ∈ V |
5 | 1, 4 | eqeltri 2864 | 1 ⊢ +∞ ∈ V |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 2051 Vcvv 3417 𝒫 cpw 4425 ∪ cuni 4717 ℂcc 10339 +∞cpnf 10477 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1759 ax-4 1773 ax-5 1870 ax-6 1929 ax-7 1966 ax-8 2053 ax-9 2060 ax-10 2080 ax-11 2094 ax-12 2107 ax-ext 2752 ax-sep 5064 ax-pow 5123 ax-un 7285 ax-cnex 10397 |
This theorem depends on definitions: df-bi 199 df-an 388 df-or 835 df-tru 1511 df-ex 1744 df-nf 1748 df-sb 2017 df-clab 2761 df-cleq 2773 df-clel 2848 df-nfc 2920 df-rex 3096 df-v 3419 df-in 3838 df-ss 3845 df-pw 4427 df-uni 4718 df-pnf 10482 |
This theorem is referenced by: pnfxr 10500 mnfxr 10504 elxnn0 11787 elxr 12334 xnegex 12424 xaddval 12439 xmulval 12441 xrinfmss 12525 hashgval 13514 hashinf 13516 hashfxnn0 13518 pcval 16043 pc0 16053 ramcl2 16214 iccpnfhmeo 23267 taylfval 24665 xrlimcnp 25263 xrge0iifcv 30853 xrge0iifiso 30854 xrge0iifhom 30856 sge0f1o 42130 sge0sup 42139 sge0pnfmpt 42193 |
Copyright terms: Public domain | W3C validator |