![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > xrex | Structured version Visualization version GIF version |
Description: The set of extended reals exists. (Contributed by NM, 24-Dec-2006.) |
Ref | Expression |
---|---|
xrex | ⊢ ℝ* ∈ V |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-xr 11304 | . 2 ⊢ ℝ* = (ℝ ∪ {+∞, -∞}) | |
2 | reex 11251 | . . 3 ⊢ ℝ ∈ V | |
3 | prex 5440 | . . 3 ⊢ {+∞, -∞} ∈ V | |
4 | 2, 3 | unex 7756 | . 2 ⊢ (ℝ ∪ {+∞, -∞}) ∈ V |
5 | 1, 4 | eqeltri 2822 | 1 ⊢ ℝ* ∈ V |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 2099 Vcvv 3462 ∪ cun 3945 {cpr 4635 ℝcr 11159 +∞cpnf 11297 -∞cmnf 11298 ℝ*cxr 11299 |
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 5306 ax-nul 5313 ax-pr 5435 ax-un 7748 ax-cnex 11216 ax-resscn 11217 |
This theorem depends on definitions: df-bi 206 df-an 395 df-or 846 df-3an 1086 df-tru 1537 df-fal 1547 df-ex 1775 df-sb 2061 df-clab 2704 df-cleq 2718 df-clel 2803 df-rab 3420 df-v 3464 df-dif 3950 df-un 3952 df-in 3954 df-ss 3964 df-nul 4326 df-sn 4634 df-pr 4636 df-uni 4916 df-xr 11304 |
This theorem is referenced by: ixxval 13388 ixxf 13390 ixxex 13391 limsuple 15482 limsuplt 15483 limsupbnd1 15486 prdsds 17481 letsr 18620 xrsbas 21377 xrsadd 21378 xrsmul 21379 xrsle 21381 xrs1mnd 21403 xrs10 21404 xrs1cmn 21405 xrge0subm 21406 xrge0cmn 21407 xrsds 21408 znle 21532 leordtval2 23210 lecldbas 23217 ispsmet 24304 isxmet 24324 imasdsf1olem 24373 blfvalps 24383 nmoffn 24722 nmofval 24725 xrsxmet 24819 xrge0gsumle 24843 xrge0tsms 24844 xrlimcnp 26999 xrge00 32897 xrge0tsmsd 32928 xrhval 33835 ltex 41971 leex 41972 icof 44844 elicores 45169 fuzxrpmcn 45467 gsumge0cl 46010 ovnval2b 46191 volicorescl 46192 ovnsubaddlem1 46209 |
Copyright terms: Public domain | W3C validator |