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

Metamath Proof Explorer

Theorem icomnfinre

Description: A left-closed, right-open, interval of extended reals, intersected with the Reals. (Contributed by Glauco Siliprandi, 26-Jun-2021)

Ref Expression
Hypothesis icomnfinre.1 ⊢ ( 𝜑 → 𝐴 ∈ ℝ* )
Assertion icomnfinre ( 𝜑 → ( ( -∞ [,) 𝐴 ) ∩ ℝ ) = ( -∞ (,) 𝐴 ) )

Proof

Step Hyp Ref Expression
1 icomnfinre.1 ⊢ ( 𝜑 → 𝐴 ∈ ℝ* )
2 mnfxr ⊢ -∞ ∈ ℝ*
3 2 a1i ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( -∞ [,) 𝐴 ) ∩ ℝ ) ) → -∞ ∈ ℝ* )
4 1 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( -∞ [,) 𝐴 ) ∩ ℝ ) ) → 𝐴 ∈ ℝ* )
5 elinel2 ⊢ ( 𝑥 ∈ ( ( -∞ [,) 𝐴 ) ∩ ℝ ) → 𝑥 ∈ ℝ )
6 5 adantl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( -∞ [,) 𝐴 ) ∩ ℝ ) ) → 𝑥 ∈ ℝ )
7 6 mnfltd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( -∞ [,) 𝐴 ) ∩ ℝ ) ) → -∞ < 𝑥 )
8 elinel1 ⊢ ( 𝑥 ∈ ( ( -∞ [,) 𝐴 ) ∩ ℝ ) → 𝑥 ∈ ( -∞ [,) 𝐴 ) )
9 8 adantl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( -∞ [,) 𝐴 ) ∩ ℝ ) ) → 𝑥 ∈ ( -∞ [,) 𝐴 ) )
10 3 4 9 icoltubd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( -∞ [,) 𝐴 ) ∩ ℝ ) ) → 𝑥 < 𝐴 )
11 3 4 6 7 10 eliood ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( -∞ [,) 𝐴 ) ∩ ℝ ) ) → 𝑥 ∈ ( -∞ (,) 𝐴 ) )
12 11 ssd ⊢ ( 𝜑 → ( ( -∞ [,) 𝐴 ) ∩ ℝ ) ⊆ ( -∞ (,) 𝐴 ) )
13 ioossico ⊢ ( -∞ (,) 𝐴 ) ⊆ ( -∞ [,) 𝐴 )
14 ioossre ⊢ ( -∞ (,) 𝐴 ) ⊆ ℝ
15 13 14 ssini ⊢ ( -∞ (,) 𝐴 ) ⊆ ( ( -∞ [,) 𝐴 ) ∩ ℝ )
16 15 a1i ⊢ ( 𝜑 → ( -∞ (,) 𝐴 ) ⊆ ( ( -∞ [,) 𝐴 ) ∩ ℝ ) )
17 12 16 eqssd ⊢ ( 𝜑 → ( ( -∞ [,) 𝐴 ) ∩ ℝ ) = ( -∞ (,) 𝐴 ) )