Theorem elxr 9968

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 8181	. . 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 8196	. . . . 5 |- +oo e. _V
5		mnfxr 8199	. . . . . 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 7994   +oocpnf 8174   -oocmnf 8175   RR*cxr 8176

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 4201  ax-pow 4257  ax-un 4523  ax-cnex 8086

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 3888  df-pnf 8179  df-mnf 8180  df-xr 8181

This theorem is referenced by:  xrnemnf  9969  xrnepnf  9970  xrltnr  9971  xrltnsym  9985  xrlttr  9987  xrltso  9988  xrlttri3  9989  nltpnft  10006  npnflt  10007  ngtmnft  10009  nmnfgt  10010  xrrebnd  10011  xnegcl  10024  xnegneg  10025  xltnegi  10027  xrpnfdc  10034  xrmnfdc  10035  xnegid  10051  xaddcom  10053  xaddid1  10054  xnegdi  10060  xleadd1a  10065  xltadd1  10068  xlt2add  10072  xsubge0  10073  xposdif  10074  xleaddadd  10079  qbtwnxr  10472  xrmaxiflemcl  11751  xrmaxifle  11752  xrmaxiflemab  11753  xrmaxiflemlub  11754  xrmaxltsup  11764  xrmaxadd  11767  xrbdtri  11782  isxmet2d  15016  blssioo  15221