volicorescl

Description: The Lebesgue measure of a left-closed, right-open interval with real bounds, is real. (Contributed by Glauco Siliprandi, 11-Oct-2020)

		Ref	Expression
	Assertion	volicorescl	$⊢ A \in ran ({[.) ↾}_{ℝ^{2}}) \to vol (A) \in ℝ$

Proof

Step	Hyp	Ref	Expression
1		df-ico	$⊢ [.) = (x \in ℝ^{}, y \in ℝ^{} ⟼ \{z \in ℝ^{*} \| (x \leq z \land z < y)\})$
2	1	reseq1i	$⊢ {[.) ↾}_{ℝ^{2}} = {(x \in ℝ^{}, y \in ℝ^{} ⟼ \{z \in ℝ^{*} \| (x \leq z \land z < y)\}) ↾}_{ℝ^{2}}$
3		ressxr	$⊢ ℝ \subseteq ℝ^{*}$
4		resmpo	$⊢ (ℝ \subseteq ℝ^{} \land ℝ \subseteq ℝ^{}) \to {(x \in ℝ^{}, y \in ℝ^{} ⟼ \{z \in ℝ^{} \| (x \leq z \land z < y)\}) ↾}_{ℝ^{2}} = (x \in ℝ, y \in ℝ ⟼ \{z \in ℝ^{} \| (x \leq z \land z < y)\})$
5	3 3 4	mp2an	$⊢ {(x \in ℝ^{}, y \in ℝ^{} ⟼ \{z \in ℝ^{} \| (x \leq z \land z < y)\}) ↾}_{ℝ^{2}} = (x \in ℝ, y \in ℝ ⟼ \{z \in ℝ^{} \| (x \leq z \land z < y)\})$
6	2 5	eqtri	$⊢ {[.) ↾}_{ℝ^{2}} = (x \in ℝ, y \in ℝ ⟼ \{z \in ℝ^{*} \| (x \leq z \land z < y)\})$
7	6	rneqi	$⊢ ran ({[.) ↾}_{ℝ^{2}}) = ran (x \in ℝ, y \in ℝ ⟼ \{z \in ℝ^{*} \| (x \leq z \land z < y)\})$
8	7	eleq2i	$⊢ A \in ran ({[.) ↾}_{ℝ^{2}}) \leftrightarrow A \in ran (x \in ℝ, y \in ℝ ⟼ \{z \in ℝ^{*} \| (x \leq z \land z < y)\})$
9	8	biimpi	$⊢ A \in ran ({[.) ↾}_{ℝ^{2}}) \to A \in ran (x \in ℝ, y \in ℝ ⟼ \{z \in ℝ^{*} \| (x \leq z \land z < y)\})$
10		eqid	$⊢ (x \in ℝ, y \in ℝ ⟼ \{z \in ℝ^{} \| (x \leq z \land z < y)\}) = (x \in ℝ, y \in ℝ ⟼ \{z \in ℝ^{} \| (x \leq z \land z < y)\})$
11		xrex	$⊢ ℝ^{*} \in V$
12	11	rabex	$⊢ \{z \in ℝ^{*} \| (x \leq z \land z < y)\} \in V$
13	10 12	elrnmpo	$⊢ A \in ran (x \in ℝ, y \in ℝ ⟼ \{z \in ℝ^{} \| (x \leq z \land z < y)\}) \leftrightarrow \exists x \in ℝ \exists y \in ℝ A = \{z \in ℝ^{} \| (x \leq z \land z < y)\}$
14	9 13	sylib	$⊢ A \in ran ({[.) ↾}_{ℝ^{2}}) \to \exists x \in ℝ \exists y \in ℝ A = \{z \in ℝ^{*} \| (x \leq z \land z < y)\}$
15		simpr	$⊢ ((x \in ℝ \land y \in ℝ) \land A = \{z \in ℝ^{} \| (x \leq z \land z < y)\}) \to A = \{z \in ℝ^{} \| (x \leq z \land z < y)\}$
16	3	sseli	$⊢ x \in ℝ \to x \in ℝ^{*}$
17	16	adantr	$⊢ (x \in ℝ \land y \in ℝ) \to x \in ℝ^{*}$
18	3	sseli	$⊢ y \in ℝ \to y \in ℝ^{*}$
19	18	adantl	$⊢ (x \in ℝ \land y \in ℝ) \to y \in ℝ^{*}$
20		icoval	$⊢ (x \in ℝ^{} \land y \in ℝ^{}) \to [x, y) = \{z \in ℝ^{*} \| (x \leq z \land z < y)\}$
21	17 19 20	syl2anc	$⊢ (x \in ℝ \land y \in ℝ) \to [x, y) = \{z \in ℝ^{*} \| (x \leq z \land z < y)\}$
22	21	eqcomd	$⊢ (x \in ℝ \land y \in ℝ) \to \{z \in ℝ^{*} \| (x \leq z \land z < y)\} = [x, y)$
23	22	adantr	$⊢ ((x \in ℝ \land y \in ℝ) \land A = \{z \in ℝ^{} \| (x \leq z \land z < y)\}) \to \{z \in ℝ^{} \| (x \leq z \land z < y)\} = [x, y)$
24	15 23	eqtrd	$⊢ ((x \in ℝ \land y \in ℝ) \land A = \{z \in ℝ^{*} \| (x \leq z \land z < y)\}) \to A = [x, y)$
25	24	ex	$⊢ (x \in ℝ \land y \in ℝ) \to (A = \{z \in ℝ^{*} \| (x \leq z \land z < y)\} \to A = [x, y))$
26	25	adantll	$⊢ ((A \in ran ({[.) ↾}_{ℝ^{2}}) \land x \in ℝ) \land y \in ℝ) \to (A = \{z \in ℝ^{*} \| (x \leq z \land z < y)\} \to A = [x, y))$
27	26	reximdva	$⊢ (A \in ran ({[.) ↾}_{ℝ^{2}}) \land x \in ℝ) \to (\exists y \in ℝ A = \{z \in ℝ^{*} \| (x \leq z \land z < y)\} \to \exists y \in ℝ A = [x, y))$
28	27	reximdva	$⊢ A \in ran ({[.) ↾}_{ℝ^{2}}) \to (\exists x \in ℝ \exists y \in ℝ A = \{z \in ℝ^{*} \| (x \leq z \land z < y)\} \to \exists x \in ℝ \exists y \in ℝ A = [x, y))$
29	14 28	mpd	$⊢ A \in ran ({[.) ↾}_{ℝ^{2}}) \to \exists x \in ℝ \exists y \in ℝ A = [x, y)$
30		fveq2	$⊢ A = [x, y) \to vol (A) = vol ([x, y))$
31	30	adantl	$⊢ ((x \in ℝ \land y \in ℝ) \land A = [x, y)) \to vol (A) = vol ([x, y))$
32		volicorecl	$⊢ (x \in ℝ \land y \in ℝ) \to vol ([x, y)) \in ℝ$
33	32	adantr	$⊢ ((x \in ℝ \land y \in ℝ) \land A = [x, y)) \to vol ([x, y)) \in ℝ$
34	31 33	eqeltrd	$⊢ ((x \in ℝ \land y \in ℝ) \land A = [x, y)) \to vol (A) \in ℝ$
35	34	ex	$⊢ (x \in ℝ \land y \in ℝ) \to (A = [x, y) \to vol (A) \in ℝ)$
36	35	a1i	$⊢ A \in ran ({[.) ↾}_{ℝ^{2}}) \to ((x \in ℝ \land y \in ℝ) \to (A = [x, y) \to vol (A) \in ℝ))$
37	36	rexlimdvv	$⊢ A \in ran ({[.) ↾}_{ℝ^{2}}) \to (\exists x \in ℝ \exists y \in ℝ A = [x, y) \to vol (A) \in ℝ)$
38	29 37	mpd	$⊢ A \in ran ({[.) ↾}_{ℝ^{2}}) \to vol (A) \in ℝ$
39	38	2a1d	$⊢ A \in ran ({[.) ↾}_{ℝ^{2}}) \to ((x \in ℝ \land y \in ℝ) \to (A = [x, y) \to vol (A) \in ℝ))$
40	39	rexlimdvv	$⊢ A \in ran ({[.) ↾}_{ℝ^{2}}) \to (\exists x \in ℝ \exists y \in ℝ A = [x, y) \to vol (A) \in ℝ)$
41	29 40	mpd	$⊢ A \in ran ({[.) ↾}_{ℝ^{2}}) \to vol (A) \in ℝ$

Metamath Proof Explorer

Theorem volicorescl

Proof