Theorem elxr 9842

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 8058	. . 3 ⊢ ℝ* = (ℝ ∪ {+∞, -∞})
2	1	eleq2i 2260	. 2 ⊢ (𝐴 ∈ ℝ* ↔ 𝐴 ∈ (ℝ ∪ {+∞, -∞}))
3		elun 3300	. 2 ⊢ (𝐴 ∈ (ℝ ∪ {+∞, -∞}) ↔ (𝐴 ∈ ℝ ∨ 𝐴 ∈ {+∞, -∞}))
4		pnfex 8073	. . . . 5 ⊢ +∞ ∈ V
5		mnfxr 8076	. . . . . 6 ⊢ -∞ ∈ ℝ*
6	5	elexi 2772	. . . . 5 ⊢ -∞ ∈ V
7	4, 6	elpr2 3640	. . . 4 ⊢ (𝐴 ∈ {+∞, -∞} ↔ (𝐴 = +∞ ∨ 𝐴 = -∞))
8	7	orbi2i 763	. . 3 ⊢ ((𝐴 ∈ ℝ ∨ 𝐴 ∈ {+∞, -∞}) ↔ (𝐴 ∈ ℝ ∨ (𝐴 = +∞ ∨ 𝐴 = -∞)))
9		3orass 983	. . 3 ⊢ ((𝐴 ∈ ℝ ∨ 𝐴 = +∞ ∨ 𝐴 = -∞) ↔ (𝐴 ∈ ℝ ∨ (𝐴 = +∞ ∨ 𝐴 = -∞)))
10	8, 9	bitr4i 187	. 2 ⊢ ((𝐴 ∈ ℝ ∨ 𝐴 ∈ {+∞, -∞}) ↔ (𝐴 ∈ ℝ ∨ 𝐴 = +∞ ∨ 𝐴 = -∞))
11	2, 3, 10	3bitri 206	1 ⊢ (𝐴 ∈ ℝ* ↔ (𝐴 ∈ ℝ ∨ 𝐴 = +∞ ∨ 𝐴 = -∞))

Syntax hints:   ↔ wb 105   ∨ wo 709   ∨ w3o 979   = wceq 1364   ∈ wcel 2164   ∪ cun 3151  {cpr 3619  ℝcr 7871  +∞cpnf 8051  -∞cmnf 8052  ℝ^*cxr 8053

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 710  ax-5 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-13 2166  ax-14 2167  ax-ext 2175  ax-sep 4147  ax-pow 4203  ax-un 4464  ax-cnex 7963

This theorem depends on definitions:  df-bi 117  df-3or 981  df-tru 1367  df-nf 1472  df-sb 1774  df-clab 2180  df-cleq 2186  df-clel 2189  df-nfc 2325  df-rex 2478  df-v 2762  df-un 3157  df-in 3159  df-ss 3166  df-pw 3603  df-sn 3624  df-pr 3625  df-uni 3836  df-pnf 8056  df-mnf 8057  df-xr 8058

This theorem is referenced by:  xrnemnf  9843  xrnepnf  9844  xrltnr  9845  xrltnsym  9859  xrlttr  9861  xrltso  9862  xrlttri3  9863  nltpnft  9880  npnflt  9881  ngtmnft  9883  nmnfgt  9884  xrrebnd  9885  xnegcl  9898  xnegneg  9899  xltnegi  9901  xrpnfdc  9908  xrmnfdc  9909  xnegid  9925  xaddcom  9927  xaddid1  9928  xnegdi  9934  xleadd1a  9939  xltadd1  9942  xlt2add  9946  xsubge0  9947  xposdif  9948  xleaddadd  9953  qbtwnxr  10326  xrmaxiflemcl  11388  xrmaxifle  11389  xrmaxiflemab  11390  xrmaxiflemlub  11391  xrmaxltsup  11401  xrmaxadd  11404  xrbdtri  11419  isxmet2d  14516  blssioo  14713