Theorem elxr 9940

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 8153	. . 3 ⊢ ℝ* = (ℝ ∪ {+∞, -∞})
2	1	eleq2i 2276	. 2 ⊢ (𝐴 ∈ ℝ* ↔ 𝐴 ∈ (ℝ ∪ {+∞, -∞}))
3		elun 3325	. 2 ⊢ (𝐴 ∈ (ℝ ∪ {+∞, -∞}) ↔ (𝐴 ∈ ℝ ∨ 𝐴 ∈ {+∞, -∞}))
4		pnfex 8168	. . . . 5 ⊢ +∞ ∈ V
5		mnfxr 8171	. . . . . 6 ⊢ -∞ ∈ ℝ*
6	5	elexi 2792	. . . . 5 ⊢ -∞ ∈ V
7	4, 6	elpr2 3668	. . . 4 ⊢ (𝐴 ∈ {+∞, -∞} ↔ (𝐴 = +∞ ∨ 𝐴 = -∞))
8	7	orbi2i 766	. . 3 ⊢ ((𝐴 ∈ ℝ ∨ 𝐴 ∈ {+∞, -∞}) ↔ (𝐴 ∈ ℝ ∨ (𝐴 = +∞ ∨ 𝐴 = -∞)))
9		3orass 986	. . 3 ⊢ ((𝐴 ∈ ℝ ∨ 𝐴 = +∞ ∨ 𝐴 = -∞) ↔ (𝐴 ∈ ℝ ∨ (𝐴 = +∞ ∨ 𝐴 = -∞)))
10	8, 9	bitr4i 187	. 2 ⊢ ((𝐴 ∈ ℝ ∨ 𝐴 ∈ {+∞, -∞}) ↔ (𝐴 ∈ ℝ ∨ 𝐴 = +∞ ∨ 𝐴 = -∞))
11	2, 3, 10	3bitri 206	1 ⊢ (𝐴 ∈ ℝ* ↔ (𝐴 ∈ ℝ ∨ 𝐴 = +∞ ∨ 𝐴 = -∞))

Syntax hints:   ↔ wb 105   ∨ wo 712   ∨ w3o 982   = wceq 1375   ∈ wcel 2180   ∪ cun 3175  {cpr 3647  ℝcr 7966  +∞cpnf 8146  -∞cmnf 8147  ℝ^*cxr 8148

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 713  ax-5 1473  ax-7 1474  ax-gen 1475  ax-ie1 1519  ax-ie2 1520  ax-8 1530  ax-10 1531  ax-11 1532  ax-i12 1533  ax-bndl 1535  ax-4 1536  ax-17 1552  ax-i9 1556  ax-ial 1560  ax-i5r 1561  ax-13 2182  ax-14 2183  ax-ext 2191  ax-sep 4181  ax-pow 4237  ax-un 4501  ax-cnex 8058

This theorem depends on definitions:  df-bi 117  df-3or 984  df-tru 1378  df-nf 1487  df-sb 1789  df-clab 2196  df-cleq 2202  df-clel 2205  df-nfc 2341  df-rex 2494  df-v 2781  df-un 3181  df-in 3183  df-ss 3190  df-pw 3631  df-sn 3652  df-pr 3653  df-uni 3868  df-pnf 8151  df-mnf 8152  df-xr 8153

This theorem is referenced by:  xrnemnf  9941  xrnepnf  9942  xrltnr  9943  xrltnsym  9957  xrlttr  9959  xrltso  9960  xrlttri3  9961  nltpnft  9978  npnflt  9979  ngtmnft  9981  nmnfgt  9982  xrrebnd  9983  xnegcl  9996  xnegneg  9997  xltnegi  9999  xrpnfdc  10006  xrmnfdc  10007  xnegid  10023  xaddcom  10025  xaddid1  10026  xnegdi  10032  xleadd1a  10037  xltadd1  10040  xlt2add  10044  xsubge0  10045  xposdif  10046  xleaddadd  10051  qbtwnxr  10444  xrmaxiflemcl  11722  xrmaxifle  11723  xrmaxiflemab  11724  xrmaxiflemlub  11725  xrmaxltsup  11735  xrmaxadd  11738  xrbdtri  11753  isxmet2d  14987  blssioo  15192