MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  xrex Structured version   Visualization version   GIF version

Theorem xrex 12240
Description: The set of extended reals exists. (Contributed by NM, 24-Dec-2006.)
Assertion
Ref Expression
xrex * ∈ V

Proof of Theorem xrex
StepHypRef Expression
1 df-xr 10532 . 2 * = (ℝ ∪ {+∞, -∞})
2 reex 10481 . . 3 ℝ ∈ V
3 prex 5231 . . 3 {+∞, -∞} ∈ V
42, 3unex 7333 . 2 (ℝ ∪ {+∞, -∞}) ∈ V
51, 4eqeltri 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