Theorem elxr 9556

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 7797	. . 3 ⊢ ℝ* = (ℝ ∪ {+∞, -∞})
2	1	eleq2i 2204	. 2 ⊢ (𝐴 ∈ ℝ* ↔ 𝐴 ∈ (ℝ ∪ {+∞, -∞}))
3		elun 3212	. 2 ⊢ (𝐴 ∈ (ℝ ∪ {+∞, -∞}) ↔ (𝐴 ∈ ℝ ∨ 𝐴 ∈ {+∞, -∞}))
4		pnfex 7812	. . . . 5 ⊢ +∞ ∈ V
5		mnfxr 7815	. . . . . 6 ⊢ -∞ ∈ ℝ*
6	5	elexi 2693	. . . . 5 ⊢ -∞ ∈ V
7	4, 6	elpr2 3544	. . . 4 ⊢ (𝐴 ∈ {+∞, -∞} ↔ (𝐴 = +∞ ∨ 𝐴 = -∞))
8	7	orbi2i 751	. . 3 ⊢ ((𝐴 ∈ ℝ ∨ 𝐴 ∈ {+∞, -∞}) ↔ (𝐴 ∈ ℝ ∨ (𝐴 = +∞ ∨ 𝐴 = -∞)))
9		3orass 965	. . 3 ⊢ ((𝐴 ∈ ℝ ∨ 𝐴 = +∞ ∨ 𝐴 = -∞) ↔ (𝐴 ∈ ℝ ∨ (𝐴 = +∞ ∨ 𝐴 = -∞)))
10	8, 9	bitr4i 186	. 2 ⊢ ((𝐴 ∈ ℝ ∨ 𝐴 ∈ {+∞, -∞}) ↔ (𝐴 ∈ ℝ ∨ 𝐴 = +∞ ∨ 𝐴 = -∞))
11	2, 3, 10	3bitri 205	1 ⊢ (𝐴 ∈ ℝ* ↔ (𝐴 ∈ ℝ ∨ 𝐴 = +∞ ∨ 𝐴 = -∞))

Syntax hints:   ↔ wb 104   ∨ wo 697   ∨ w3o 961   = wceq 1331   ∈ wcel 1480   ∪ cun 3064  {cpr 3523  ℝcr 7612  +∞cpnf 7790  -∞cmnf 7791  ℝ^*cxr 7792

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 698  ax-5 1423  ax-7 1424  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-8 1482  ax-10 1483  ax-11 1484  ax-i12 1485  ax-bndl 1486  ax-4 1487  ax-13 1491  ax-14 1492  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-ext 2119  ax-sep 4041  ax-pow 4093  ax-un 4350  ax-cnex 7704

This theorem depends on definitions:  df-bi 116  df-3or 963  df-tru 1334  df-nf 1437  df-sb 1736  df-clab 2124  df-cleq 2130  df-clel 2133  df-nfc 2268  df-rex 2420  df-v 2683  df-un 3070  df-in 3072  df-ss 3079  df-pw 3507  df-sn 3528  df-pr 3529  df-uni 3732  df-pnf 7795  df-mnf 7796  df-xr 7797

This theorem is referenced by:  xrnemnf  9557  xrnepnf  9558  xrltnr  9559  xrltnsym  9572  xrlttr  9574  xrltso  9575  xrlttri3  9576  nltpnft  9590  npnflt  9591  ngtmnft  9593  nmnfgt  9594  xrrebnd  9595  xnegcl  9608  xnegneg  9609  xltnegi  9611  xrpnfdc  9618  xrmnfdc  9619  xnegid  9635  xaddcom  9637  xaddid1  9638  xnegdi  9644  xleadd1a  9649  xltadd1  9652  xlt2add  9656  xsubge0  9657  xposdif  9658  xleaddadd  9663  qbtwnxr  10028  xrmaxiflemcl  11007  xrmaxifle  11008  xrmaxiflemab  11009  xrmaxiflemlub  11010  xrmaxltsup  11020  xrmaxadd  11023  xrbdtri  11038  isxmet2d  12506  blssioo  12703