![]() |
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 11300 | . 2 ⊢ +∞ = 𝒫 ∪ ℂ | |
2 | cnex 11239 | . . . 4 ⊢ ℂ ∈ V | |
3 | 2 | uniex 7752 | . . 3 ⊢ ∪ ℂ ∈ V |
4 | 3 | pwex 5384 | . 2 ⊢ 𝒫 ∪ ℂ ∈ V |
5 | 1, 4 | eqeltri 2822 | 1 ⊢ +∞ ∈ V |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 2099 Vcvv 3462 𝒫 cpw 4607 ∪ cuni 4913 ℂcc 11156 +∞cpnf 11295 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 ax-5 1906 ax-6 1964 ax-7 2004 ax-8 2101 ax-9 2109 ax-ext 2697 ax-sep 5304 ax-pow 5369 ax-un 7746 ax-cnex 11214 |
This theorem depends on definitions: df-bi 206 df-an 395 df-tru 1537 df-ex 1775 df-sb 2061 df-clab 2704 df-cleq 2718 df-clel 2803 df-v 3464 df-ss 3964 df-pw 4609 df-uni 4914 df-pnf 11300 |
This theorem is referenced by: pnfxr 11318 mnfxr 11321 elxnn0 12598 elxr 13150 xnegex 13241 xaddval 13256 xmulval 13258 xrinfmss 13343 hashgval 14350 hashinf 14352 hashfxnn0 14354 pcval 16846 pc0 16856 ramcl2 17018 iccpnfhmeo 24961 taylfval 26386 xrlimcnp 26996 xrge0iifcv 33749 xrge0iifiso 33750 xrge0iifhom 33752 sge0f1o 46003 sge0sup 46012 sge0pnfmpt 46066 |
Copyright terms: Public domain | W3C validator |