Theorem elxr 13132

Description: Membership in the set of extended reals. (Contributed by NM, 14-Oct-2005.)

Assertion

Ref	Expression
elxr	⊢ (𝐴 ∈ ℝ* ↔ (𝐴 ∈ ℝ ∨ 𝐴 = +∞ ∨ 𝐴 = -∞))

Proof of Theorem elxr

Step	Hyp	Ref	Expression
1		df-xr 11235	. . 3 ⊢ ℝ* = (ℝ ∪ {+∞, -∞})
2	1	eleq2i 2857	. 2 ⊢ (𝐴 ∈ ℝ* ↔ 𝐴 ∈ (ℝ ∪ {+∞, -∞}))
3		elun 4109	. 2 ⊢ (𝐴 ∈ (ℝ ∪ {+∞, -∞}) ↔ (𝐴 ∈ ℝ ∨ 𝐴 ∈ {+∞, -∞}))
4		pnfex 11250	. . . . 5 ⊢ +∞ ∈ V
5		mnfxr 11254	. . . . . 6 ⊢ -∞ ∈ ℝ*
6	5	elexi 3479	. . . . 5 ⊢ -∞ ∈ V
7	4, 6	elpr2 4612	. . . 4 ⊢ (𝐴 ∈ {+∞, -∞} ↔ (𝐴 = +∞ ∨ 𝐴 = -∞))
8	7	orbi2i 925	. . 3 ⊢ ((𝐴 ∈ ℝ ∨ 𝐴 ∈ {+∞, -∞}) ↔ (𝐴 ∈ ℝ ∨ (𝐴 = +∞ ∨ 𝐴 = -∞)))
9		3orass 1104	. . 3 ⊢ ((𝐴 ∈ ℝ ∨ 𝐴 = +∞ ∨ 𝐴 = -∞) ↔ (𝐴 ∈ ℝ ∨ (𝐴 = +∞ ∨ 𝐴 = -∞)))
10	8, 9	bitr4i 281	. 2 ⊢ ((𝐴 ∈ ℝ ∨ 𝐴 ∈ {+∞, -∞}) ↔ (𝐴 ∈ ℝ ∨ 𝐴 = +∞ ∨ 𝐴 = -∞))
11	2, 3, 10	3bitri 300	1 ⊢ (𝐴 ∈ ℝ* ↔ (𝐴 ∈ ℝ ∨ 𝐴 = +∞ ∨ 𝐴 = -∞))

Syntax hints:   ↔ wb 209   ∨ wo 860   ∨ w3o 1100   = wceq 1563   ∈ wcel 2145   ∪ cun 3905  {cpr 4587  ℝcr 11087  +∞cpnf 11228  -∞cmnf 11229  ℝ^*cxr 11230

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-ext 2737  ax-sep 5251  ax-pow 5327  ax-un 7722  ax-cnex 11144

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1102  df-tru 1566  df-ex 1803  df-sb 2094  df-clab 2744  df-cleq 2757  df-clel 2840  df-v 3459  df-un 3912  df-ss 3924  df-pw 4560  df-sn 4586  df-pr 4588  df-uni 4869  df-pnf 11233  df-mnf 11234  df-xr 11235

This theorem is referenced by:  xrnemnf  13133  xrnepnf  13134  xrltnr  13135  xrltnsym  13153  xrlttri  13155  xrlttr  13156  xrrebnd  13185  qbtwnxr  13217  xnegcl  13230  xnegneg  13231  xltnegi  13233  xaddf  13241  xnegid  13255  xaddcom  13257  xaddrid  13258  xnegdi  13265  xleadd1a  13270  xlt2add  13277  xsubge0  13278  xmullem  13281  xmulrid  13296  xmulgt0  13300  xmulasslem3  13303  xlemul1a  13305  xadddilem  13311  xadddi2  13314  xrsupsslem  13324  xrinfmsslem  13325  xrub  13329  reltxrnmnf  13360  isxmet2d  24445  blssioo  24913  ioombl1  25682  ismbf2d  25760  itg2seq  25862  xaddeq0  33010  rexmul2  33011  iooelexlt  37868  relowlssretop  37869  iccpartiltu  48026  iccpartigtl  48027