![]() |
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 10532 | . 2 ⊢ ℝ* = (ℝ ∪ {+∞, -∞}) | |
2 | reex 10481 | . . 3 ⊢ ℝ ∈ V | |
3 | prex 5231 | . . 3 ⊢ {+∞, -∞} ∈ V | |
4 | 2, 3 | unex 7333 | . 2 ⊢ (ℝ ∪ {+∞, -∞}) ∈ V |
5 | 1, 4 | eqeltri 2881 | 1 ⊢ ℝ* ∈ V |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 2083 Vcvv 3440 ∪ cun 3863 {cpr 4480 ℝcr 10389 +∞cpnf 10525 -∞cmnf 10526 ℝ*cxr 10527 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1781 ax-4 1795 ax-5 1892 ax-6 1951 ax-7 1996 ax-8 2085 ax-9 2093 ax-10 2114 ax-11 2128 ax-12 2143 ax-ext 2771 ax-sep 5101 ax-nul 5108 ax-pr 5228 ax-un 7326 ax-cnex 10446 ax-resscn 10447 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 843 df-tru 1528 df-ex 1766 df-nf 1770 df-sb 2045 df-clab 2778 df-cleq 2790 df-clel 2865 df-nfc 2937 df-rex 3113 df-v 3442 df-dif 3868 df-un 3870 df-in 3872 df-ss 3880 df-nul 4218 df-sn 4479 df-pr 4481 df-uni 4752 df-xr 10532 |
This theorem is referenced by: ixxval 12600 ixxf 12602 ixxex 12603 limsuple 14673 limsuplt 14674 limsupbnd1 14677 prdsds 16570 letsr 17670 xrsbas 20247 xrsadd 20248 xrsmul 20249 xrsle 20251 xrs1mnd 20269 xrs10 20270 xrs1cmn 20271 xrge0subm 20272 xrge0cmn 20273 xrsds 20274 znle 20369 leordtval2 21508 lecldbas 21515 ispsmet 22601 isxmet 22621 imasdsf1olem 22670 blfvalps 22680 nmoffn 23007 nmofval 23010 xrsxmet 23104 xrge0gsumle 23128 xrge0tsms 23129 xrlimcnp 25232 xrge00 30343 xrge0tsmsd 30499 xrhval 30872 icof 41043 elicores 41372 fuzxrpmcn 41672 gsumge0cl 42217 ovnval2b 42398 volicorescl 42399 ovnsubaddlem1 42416 |
Copyright terms: Public domain | W3C validator |