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

Theorem elxr 12160
Description: Membership in the set of extended reals. (Contributed by NM, 14-Oct-2005.)
Assertion
Ref Expression
elxr (𝐴 ∈ ℝ* ↔ (𝐴 ∈ ℝ ∨ 𝐴 = +∞ ∨ 𝐴 = -∞))

Proof of Theorem elxr
StepHypRef Expression
1 df-xr 10357 . . 3 * = (ℝ ∪ {+∞, -∞})
21eleq2i 2873 . 2 (𝐴 ∈ ℝ*𝐴 ∈ (ℝ ∪ {+∞, -∞}))
3 elun 3946 . 2 (𝐴 ∈ (ℝ ∪ {+∞, -∞}) ↔ (𝐴 ∈ ℝ ∨ 𝐴 ∈ {+∞, -∞}))
4 pnfex 10372 . . . . 5 +∞ ∈ V
5 mnfxr 10375 . . . . . 6 -∞ ∈ ℝ*
65elexi 3403 . . . . 5 -∞ ∈ V
74, 6elpr2 4388 . . . 4 (𝐴 ∈ {+∞, -∞} ↔ (𝐴 = +∞ ∨ 𝐴 = -∞))
87orbi2i 927 . . 3 ((𝐴 ∈ ℝ ∨ 𝐴 ∈ {+∞, -∞}) ↔ (𝐴 ∈ ℝ ∨ (𝐴 = +∞ ∨ 𝐴 = -∞)))
9 3orass 1103 . . 3 ((𝐴 ∈ ℝ ∨ 𝐴 = +∞ ∨ 𝐴 = -∞) ↔ (𝐴 ∈ ℝ ∨ (𝐴 = +∞ ∨ 𝐴 = -∞)))
108, 9bitr4i 269 . 2 ((𝐴 ∈ ℝ ∨ 𝐴 ∈ {+∞, -∞}) ↔ (𝐴 ∈ ℝ ∨ 𝐴 = +∞ ∨ 𝐴 = -∞))
112, 3, 103bitri 288 1 (𝐴 ∈ ℝ* ↔ (𝐴 ∈ ℝ ∨ 𝐴 = +∞ ∨ 𝐴 = -∞))
Colors of variables: wff setvar class
Syntax hints:  wb 197  wo 865  w3o 1099   = wceq 1637  wcel 2155  cun 3761  {cpr 4366  cr 10214  +∞cpnf 10350  -∞cmnf 10351  *cxr 10352
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2067  ax-7 2103  ax-8 2157  ax-9 2164  ax-10 2184  ax-11 2200  ax-12 2213  ax-13 2419  ax-ext 2781  ax-sep 4968  ax-pow 5029  ax-un 7173  ax-cnex 10271
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3or 1101  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2060  df-clab 2789  df-cleq 2795  df-clel 2798  df-nfc 2933  df-rex 3098  df-v 3389  df-un 3768  df-in 3770  df-ss 3777  df-pw 4347  df-sn 4365  df-pr 4367  df-uni 4624  df-pnf 10355  df-mnf 10356  df-xr 10357
This theorem is referenced by:  xrnemnf  12161  xrnepnf  12162  xrltnr  12163  xrltnsym  12180  xrlttri  12182  xrlttr  12183  xrrebnd  12211  qbtwnxr  12243  xnegcl  12256  xnegneg  12257  xltnegi  12259  xaddf  12267  xnegid  12281  xaddcom  12283  xaddid1  12284  xnegdi  12290  xleadd1a  12295  xlt2add  12302  xsubge0  12303  xmullem  12306  xmulid1  12321  xmulgt0  12325  xmulasslem3  12328  xlemul1a  12330  xadddilem  12336  xadddi2  12339  xrsupsslem  12349  xrinfmsslem  12350  xrub  12354  reltxrnmnf  12384  isxmet2d  22339  blssioo  22805  ioombl1  23537  ismbf2d  23615  itg2seq  23717  xaddeq0  29839  iooelexlt  33520  relowlssretop  33521  iccpartiltu  41927  iccpartigtl  41928
  Copyright terms: Public domain W3C validator