Theorem elxr

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

	Ref	Expression
Assertion	elxr	⊢ ( 𝐴 ∈ ℝ* ↔ ( 𝐴 ∈ ℝ ∨ 𝐴 = +∞ ∨ 𝐴 = -∞ ) )

Proof

Step	Hyp	Ref	Expression
1		df-xr	⊢ ℝ* = ( ℝ ∪ { +∞ , -∞ } )
2	1	eleq2i	⊢ ( 𝐴 ∈ ℝ* ↔ 𝐴 ∈ ( ℝ ∪ { +∞ , -∞ } ) )
3		elun	⊢ ( 𝐴 ∈ ( ℝ ∪ { +∞ , -∞ } ) ↔ ( 𝐴 ∈ ℝ ∨ 𝐴 ∈ { +∞ , -∞ } ) )
4		pnfex	⊢ +∞ ∈ V
5		mnfxr	⊢ -∞ ∈ ℝ*
6	5	elexi	⊢ -∞ ∈ V
7	4 6	elpr2	⊢ ( 𝐴 ∈ { +∞ , -∞ } ↔ ( 𝐴 = +∞ ∨ 𝐴 = -∞ ) )
8	7	orbi2i	⊢ ( ( 𝐴 ∈ ℝ ∨ 𝐴 ∈ { +∞ , -∞ } ) ↔ ( 𝐴 ∈ ℝ ∨ ( 𝐴 = +∞ ∨ 𝐴 = -∞ ) ) )
9		3orass	⊢ ( ( 𝐴 ∈ ℝ ∨ 𝐴 = +∞ ∨ 𝐴 = -∞ ) ↔ ( 𝐴 ∈ ℝ ∨ ( 𝐴 = +∞ ∨ 𝐴 = -∞ ) ) )
10	8 9	bitr4i	⊢ ( ( 𝐴 ∈ ℝ ∨ 𝐴 ∈ { +∞ , -∞ } ) ↔ ( 𝐴 ∈ ℝ ∨ 𝐴 = +∞ ∨ 𝐴 = -∞ ) )
11	2 3 10	3bitri	⊢ ( 𝐴 ∈ ℝ* ↔ ( 𝐴 ∈ ℝ ∨ 𝐴 = +∞ ∨ 𝐴 = -∞ ) )