Theorem elxr 9778

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 7998	. . 3 ⊢ ℝ* = (ℝ ∪ {+∞, -∞})
2	1	eleq2i 2244	. 2 ⊢ (𝐴 ∈ ℝ* ↔ 𝐴 ∈ (ℝ ∪ {+∞, -∞}))
3		elun 3278	. 2 ⊢ (𝐴 ∈ (ℝ ∪ {+∞, -∞}) ↔ (𝐴 ∈ ℝ ∨ 𝐴 ∈ {+∞, -∞}))
4		pnfex 8013	. . . . 5 ⊢ +∞ ∈ V
5		mnfxr 8016	. . . . . 6 ⊢ -∞ ∈ ℝ*
6	5	elexi 2751	. . . . 5 ⊢ -∞ ∈ V
7	4, 6	elpr2 3616	. . . 4 ⊢ (𝐴 ∈ {+∞, -∞} ↔ (𝐴 = +∞ ∨ 𝐴 = -∞))
8	7	orbi2i 762	. . 3 ⊢ ((𝐴 ∈ ℝ ∨ 𝐴 ∈ {+∞, -∞}) ↔ (𝐴 ∈ ℝ ∨ (𝐴 = +∞ ∨ 𝐴 = -∞)))
9		3orass 981	. . 3 ⊢ ((𝐴 ∈ ℝ ∨ 𝐴 = +∞ ∨ 𝐴 = -∞) ↔ (𝐴 ∈ ℝ ∨ (𝐴 = +∞ ∨ 𝐴 = -∞)))
10	8, 9	bitr4i 187	. 2 ⊢ ((𝐴 ∈ ℝ ∨ 𝐴 ∈ {+∞, -∞}) ↔ (𝐴 ∈ ℝ ∨ 𝐴 = +∞ ∨ 𝐴 = -∞))
11	2, 3, 10	3bitri 206	1 ⊢ (𝐴 ∈ ℝ* ↔ (𝐴 ∈ ℝ ∨ 𝐴 = +∞ ∨ 𝐴 = -∞))

Syntax hints:   ↔ wb 105   ∨ wo 708   ∨ w3o 977   = wceq 1353   ∈ wcel 2148   ∪ cun 3129  {cpr 3595  ℝcr 7812  +∞cpnf 7991  -∞cmnf 7992  ℝ^*cxr 7993

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 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-13 2150  ax-14 2151  ax-ext 2159  ax-sep 4123  ax-pow 4176  ax-un 4435  ax-cnex 7904

This theorem depends on definitions:  df-bi 117  df-3or 979  df-tru 1356  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-rex 2461  df-v 2741  df-un 3135  df-in 3137  df-ss 3144  df-pw 3579  df-sn 3600  df-pr 3601  df-uni 3812  df-pnf 7996  df-mnf 7997  df-xr 7998

This theorem is referenced by:  xrnemnf  9779  xrnepnf  9780  xrltnr  9781  xrltnsym  9795  xrlttr  9797  xrltso  9798  xrlttri3  9799  nltpnft  9816  npnflt  9817  ngtmnft  9819  nmnfgt  9820  xrrebnd  9821  xnegcl  9834  xnegneg  9835  xltnegi  9837  xrpnfdc  9844  xrmnfdc  9845  xnegid  9861  xaddcom  9863  xaddid1  9864  xnegdi  9870  xleadd1a  9875  xltadd1  9878  xlt2add  9882  xsubge0  9883  xposdif  9884  xleaddadd  9889  qbtwnxr  10260  xrmaxiflemcl  11255  xrmaxifle  11256  xrmaxiflemab  11257  xrmaxiflemlub  11258  xrmaxltsup  11268  xrmaxadd  11271  xrbdtri  11286  isxmet2d  13933  blssioo  14130