![]() |
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 11190 | . 2 ⊢ +∞ = 𝒫 ∪ ℂ | |
2 | cnex 11131 | . . . 4 ⊢ ℂ ∈ V | |
3 | 2 | uniex 7677 | . . 3 ⊢ ∪ ℂ ∈ V |
4 | 3 | pwex 5335 | . 2 ⊢ 𝒫 ∪ ℂ ∈ V |
5 | 1, 4 | eqeltri 2834 | 1 ⊢ +∞ ∈ V |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 2106 Vcvv 3445 𝒫 cpw 4560 ∪ cuni 4865 ℂcc 11048 +∞cpnf 11185 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-ext 2707 ax-sep 5256 ax-pow 5320 ax-un 7671 ax-cnex 11106 |
This theorem depends on definitions: df-bi 206 df-an 397 df-tru 1544 df-ex 1782 df-sb 2068 df-clab 2714 df-cleq 2728 df-clel 2814 df-v 3447 df-in 3917 df-ss 3927 df-pw 4562 df-uni 4866 df-pnf 11190 |
This theorem is referenced by: pnfxr 11208 mnfxr 11211 elxnn0 12486 elxr 13036 xnegex 13126 xaddval 13141 xmulval 13143 xrinfmss 13228 hashgval 14232 hashinf 14234 hashfxnn0 14236 pcval 16715 pc0 16725 ramcl2 16887 iccpnfhmeo 24306 taylfval 25716 xrlimcnp 26316 xrge0iifcv 32506 xrge0iifiso 32507 xrge0iifhom 32509 sge0f1o 44595 sge0sup 44604 sge0pnfmpt 44658 |
Copyright terms: Public domain | W3C validator |