Theorem elxr 9984

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

Assertion

Ref	Expression
elxr	|- ( A e. RR* <-> ( A e. RR \/ A = +oo \/ A = -oo ) )

Proof of Theorem elxr

Step	Hyp	Ref	Expression
1		df-xr 8196	. . 3 |- RR* = ( RR u. { +oo , -oo } )
2	1	eleq2i 2296	. 2 |- ( A e. RR* <-> A e. ( RR u. { +oo , -oo } ) )
3		elun 3345	. 2 |- ( A e. ( RR u. { +oo , -oo } ) <-> ( A e. RR \/ A e. { +oo , -oo } ) )
4		pnfex 8211	. . . . 5 |- +oo e. _V
5		mnfxr 8214	. . . . . 6 |- -oo e. RR*
6	5	elexi 2812	. . . . 5 |- -oo e. _V
7	4, 6	elpr2 3688	. . . 4 |- ( A e. { +oo , -oo } <-> ( A = +oo \/ A = -oo ) )
8	7	orbi2i 767	. . 3 |- ( ( A e. RR \/ A e. { +oo , -oo } ) <-> ( A e. RR \/ ( A = +oo \/ A = -oo ) ) )
9		3orass 1005	. . 3 |- ( ( A e. RR \/ A = +oo \/ A = -oo ) <-> ( A e. RR \/ ( A = +oo \/ A = -oo ) ) )
10	8, 9	bitr4i 187	. 2 |- ( ( A e. RR \/ A e. { +oo , -oo } ) <-> ( A e. RR \/ A = +oo \/ A = -oo ) )
11	2, 3, 10	3bitri 206	1 |- ( A e. RR* <-> ( A e. RR \/ A = +oo \/ A = -oo ) )

Syntax hints:   <-> wb 105   \/ wo 713   \/ w3o 1001   = wceq 1395   e. wcel 2200   u. cun 3195   {cpr 3667   RRcr 8009   +oocpnf 8189   -oocmnf 8190   RR*cxr 8191

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 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-13 2202  ax-14 2203  ax-ext 2211  ax-sep 4202  ax-pow 4258  ax-un 4524  ax-cnex 8101

This theorem depends on definitions:  df-bi 117  df-3or 1003  df-tru 1398  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-rex 2514  df-v 2801  df-un 3201  df-in 3203  df-ss 3210  df-pw 3651  df-sn 3672  df-pr 3673  df-uni 3889  df-pnf 8194  df-mnf 8195  df-xr 8196

This theorem is referenced by:  xrnemnf  9985  xrnepnf  9986  xrltnr  9987  xrltnsym  10001  xrlttr  10003  xrltso  10004  xrlttri3  10005  nltpnft  10022  npnflt  10023  ngtmnft  10025  nmnfgt  10026  xrrebnd  10027  xnegcl  10040  xnegneg  10041  xltnegi  10043  xrpnfdc  10050  xrmnfdc  10051  xnegid  10067  xaddcom  10069  xaddid1  10070  xnegdi  10076  xleadd1a  10081  xltadd1  10084  xlt2add  10088  xsubge0  10089  xposdif  10090  xleaddadd  10095  qbtwnxr  10489  xrmaxiflemcl  11771  xrmaxifle  11772  xrmaxiflemab  11773  xrmaxiflemlub  11774  xrmaxltsup  11784  xrmaxadd  11787  xrbdtri  11802  isxmet2d  15037  blssioo  15242