Theorem elxr

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

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

Proof

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