icoresmbl

Description: A closed-below, open-above real interval is measurable, when the bounds are real. (Contributed by Glauco Siliprandi, 11-Oct-2020)

		Ref	Expression
	Assertion	icoresmbl	$⊢ ran ({[.) ↾}_{ℝ^{2}}) \subseteq dom vol$

Step	Hyp	Ref	Expression
1		elicores	$⊢ x \in ran ({[.) ↾}_{ℝ^{2}}) \leftrightarrow \exists y \in ℝ \exists z \in ℝ x = [y, z)$
2	1	biimpi	$⊢ x \in ran ({[.) ↾}_{ℝ^{2}}) \to \exists y \in ℝ \exists z \in ℝ x = [y, z)$
3		simpr	$⊢ ((y \in ℝ \land z \in ℝ) \land x = [y, z)) \to x = [y, z)$
4		simpl	$⊢ (y \in ℝ \land z \in ℝ) \to y \in ℝ$
5		rexr	$⊢ z \in ℝ \to z \in ℝ^{*}$
6	5	adantl	$⊢ (y \in ℝ \land z \in ℝ) \to z \in ℝ^{*}$
7		icombl	$⊢ (y \in ℝ \land z \in ℝ^{*}) \to [y, z) \in dom vol$
8	4 6 7	syl2anc	$⊢ (y \in ℝ \land z \in ℝ) \to [y, z) \in dom vol$
9	8	adantr	$⊢ ((y \in ℝ \land z \in ℝ) \land x = [y, z)) \to [y, z) \in dom vol$
10	3 9	eqeltrd	$⊢ ((y \in ℝ \land z \in ℝ) \land x = [y, z)) \to x \in dom vol$
11	10	rexlimdva2	$⊢ y \in ℝ \to (\exists z \in ℝ x = [y, z) \to x \in dom vol)$
12	11	rexlimiv	$⊢ \exists y \in ℝ \exists z \in ℝ x = [y, z) \to x \in dom vol$
13	12	a1i	$⊢ x \in ran ({[.) ↾}_{ℝ^{2}}) \to (\exists y \in ℝ \exists z \in ℝ x = [y, z) \to x \in dom vol)$
14	2 13	mpd	$⊢ x \in ran ({[.) ↾}_{ℝ^{2}}) \to x \in dom vol$
15	14	rgen	$⊢ \forall x \in ran ({[.) ↾}_{ℝ^{2}}) x \in dom vol$
16		dfss3	$⊢ ran ({[.) ↾}_{ℝ^{2}}) \subseteq dom vol \leftrightarrow \forall x \in ran ({[.) ↾}_{ℝ^{2}}) x \in dom vol$
17	15 16	mpbir	$⊢ ran ({[.) ↾}_{ℝ^{2}}) \subseteq dom vol$

Metamath Proof Explorer