Metamath Proof Explorer


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 ( 𝐴 ∈ ℝ* ↔ ( 𝐴 ∈ ℝ ∨ 𝐴 = +∞ ∨ 𝐴 = -∞ ) )