![]() |
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.) |
Ref | Expression |
---|---|
pnfex | ⊢ +∞ ∈ V |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | pnfxr 10294 | . 2 ⊢ +∞ ∈ ℝ* | |
2 | 1 | elexi 3365 | 1 ⊢ +∞ ∈ V |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 2145 Vcvv 3351 +∞cpnf 10273 ℝ*cxr 10275 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1870 ax-4 1885 ax-5 1991 ax-6 2057 ax-7 2093 ax-8 2147 ax-9 2154 ax-10 2174 ax-11 2190 ax-12 2203 ax-13 2408 ax-ext 2751 ax-sep 4915 ax-pow 4974 ax-un 7096 ax-cnex 10194 |
This theorem depends on definitions: df-bi 197 df-an 383 df-or 837 df-tru 1634 df-ex 1853 df-nf 1858 df-sb 2050 df-clab 2758 df-cleq 2764 df-clel 2767 df-nfc 2902 df-rex 3067 df-v 3353 df-un 3728 df-in 3730 df-ss 3737 df-pw 4299 df-sn 4317 df-pr 4319 df-uni 4575 df-pnf 10278 df-xr 10280 |
This theorem is referenced by: mnfxr 10298 elxnn0 11568 elxr 12151 xnegex 12240 xaddval 12255 xmulval 12257 xrinfmss 12341 hashgval 13320 hashinf 13322 hashfxnn0 13324 hashfOLD 13326 pcval 15752 pc0 15762 ramcl2 15923 iccpnfhmeo 22960 taylfval 24329 xrlimcnp 24912 xrge0iifcv 30316 xrge0iifiso 30317 xrge0iifhom 30319 sge0f1o 41113 sge0sup 41122 sge0pnfmpt 41176 |
Copyright terms: Public domain | W3C validator |