This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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