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	$⊢ φ \to A \in ℝ^{*}$
	Assertion	icomnfinre	$⊢ φ \to [−∞, A) \cap ℝ = (−∞, A)$

Step	Hyp	Ref	Expression
1		icomnfinre.1	$⊢ φ \to A \in ℝ^{*}$
2		mnfxr	$⊢ −∞ \in ℝ^{*}$
3	2	a1i	$⊢ (φ \land x \in ([−∞, A) \cap ℝ)) \to −∞ \in ℝ^{*}$
4	1	adantr	$⊢ (φ \land x \in ([−∞, A) \cap ℝ)) \to A \in ℝ^{*}$
5		elinel2	$⊢ x \in ([−∞, A) \cap ℝ) \to x \in ℝ$
6	5	adantl	$⊢ (φ \land x \in ([−∞, A) \cap ℝ)) \to x \in ℝ$
7	6	mnfltd	$⊢ (φ \land x \in ([−∞, A) \cap ℝ)) \to −∞ < x$
8		elinel1	$⊢ x \in ([−∞, A) \cap ℝ) \to x \in [−∞, A)$
9	8	adantl	$⊢ (φ \land x \in ([−∞, A) \cap ℝ)) \to x \in [−∞, A)$
10	3 4 9	icoltubd	$⊢ (φ \land x \in ([−∞, A) \cap ℝ)) \to x < A$
11	3 4 6 7 10	eliood	$⊢ (φ \land x \in ([−∞, A) \cap ℝ)) \to x \in (−∞, A)$
12	11	ssd	$⊢ φ \to [−∞, A) \cap ℝ \subseteq (−∞, A)$
13		ioossico	$⊢ (−∞, A) \subseteq [−∞, A)$
14		ioossre	$⊢ (−∞, A) \subseteq ℝ$
15	13 14	ssini	$⊢ (−∞, A) \subseteq [−∞, A) \cap ℝ$
16	15	a1i	$⊢ φ \to (−∞, A) \subseteq [−∞, A) \cap ℝ$
17	12 16	eqssd	$⊢ φ \to [−∞, A) \cap ℝ = (−∞, A)$

Metamath Proof Explorer