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	⊢ ( 𝜑 → ( ( -∞ [,) 𝐴 ) ∩ ℝ ) = ( -∞ (,) 𝐴 ) )