ovolval5

Description: The value of the Lebesgue outer measure for subsets of the reals, using covers of left-closed right-open intervals are used, instead of open intervals. (Contributed by Glauco Siliprandi, 3-Mar-2021)

	Ref	Expression
Hypotheses	ovolval5.a	$⊢ φ \to A \subseteq ℝ$
	ovolval5.m	$⊢ M = \{y \in ℝ^{*} \| \exists f \in ({ℝ^{2}}^{ℕ}) (A \subseteq ⋃ ran ([.) \circ f) \land y = sum^((vol \circ [.)) \circ f))\}$
Assertion	ovolval5	$⊢ φ \to {vol}^{} (A) = inf (M ℝ^{} <)$

Proof

Step	Hyp	Ref	Expression
1		ovolval5.a	$⊢ φ \to A \subseteq ℝ$
2		ovolval5.m	$⊢ M = \{y \in ℝ^{*} \| \exists f \in ({ℝ^{2}}^{ℕ}) (A \subseteq ⋃ ran ([.) \circ f) \land y = sum^((vol \circ [.)) \circ f))\}$
3		eqeq1	$⊢ x = y \to (x = sum^((vol \circ (.)) \circ g) \leftrightarrow y = sum^((vol \circ (.)) \circ g))$
4	3	anbi2d	$⊢ x = y \to ((A \subseteq ⋃ ran ((.) \circ g) \land x = sum^((vol \circ (.)) \circ g)) \leftrightarrow (A \subseteq ⋃ ran ((.) \circ g) \land y = sum^((vol \circ (.)) \circ g)))$
5	4	rexbidv	$⊢ x = y \to (\exists g \in ({ℝ^{2}}^{ℕ}) (A \subseteq ⋃ ran ((.) \circ g) \land x = sum^((vol \circ (.)) \circ g)) \leftrightarrow \exists g \in ({ℝ^{2}}^{ℕ}) (A \subseteq ⋃ ran ((.) \circ g) \land y = sum^((vol \circ (.)) \circ g)))$
6		coeq2	$⊢ g = f \to (.) \circ g = (.) \circ f$
7	6	rneqd	$⊢ g = f \to ran ((.) \circ g) = ran ((.) \circ f)$
8	7	unieqd	$⊢ g = f \to ⋃ ran ((.) \circ g) = ⋃ ran ((.) \circ f)$
9	8	sseq2d	$⊢ g = f \to (A \subseteq ⋃ ran ((.) \circ g) \leftrightarrow A \subseteq ⋃ ran ((.) \circ f))$
10		coeq2	$⊢ g = f \to (vol \circ (.)) \circ g = (vol \circ (.)) \circ f$
11	10	fveq2d	$⊢ g = f \to sum^((vol \circ (.)) \circ g) = sum^((vol \circ (.)) \circ f)$
12	11	eqeq2d	$⊢ g = f \to (y = sum^((vol \circ (.)) \circ g) \leftrightarrow y = sum^((vol \circ (.)) \circ f))$
13	9 12	anbi12d	$⊢ g = f \to ((A \subseteq ⋃ ran ((.) \circ g) \land y = sum^((vol \circ (.)) \circ g)) \leftrightarrow (A \subseteq ⋃ ran ((.) \circ f) \land y = sum^((vol \circ (.)) \circ f)))$
14	13	cbvrexvw	$⊢ \exists g \in ({ℝ^{2}}^{ℕ}) (A \subseteq ⋃ ran ((.) \circ g) \land y = sum^((vol \circ (.)) \circ g)) \leftrightarrow \exists f \in ({ℝ^{2}}^{ℕ}) (A \subseteq ⋃ ran ((.) \circ f) \land y = sum^((vol \circ (.)) \circ f))$
15	14	a1i	$⊢ x = y \to (\exists g \in ({ℝ^{2}}^{ℕ}) (A \subseteq ⋃ ran ((.) \circ g) \land y = sum^((vol \circ (.)) \circ g)) \leftrightarrow \exists f \in ({ℝ^{2}}^{ℕ}) (A \subseteq ⋃ ran ((.) \circ f) \land y = sum^((vol \circ (.)) \circ f)))$
16	5 15	bitrd	$⊢ x = y \to (\exists g \in ({ℝ^{2}}^{ℕ}) (A \subseteq ⋃ ran ((.) \circ g) \land x = sum^((vol \circ (.)) \circ g)) \leftrightarrow \exists f \in ({ℝ^{2}}^{ℕ}) (A \subseteq ⋃ ran ((.) \circ f) \land y = sum^((vol \circ (.)) \circ f)))$
17	16	cbvrabv	$⊢ \{x \in ℝ^{} \| \exists g \in ({ℝ^{2}}^{ℕ}) (A \subseteq ⋃ ran ((.) \circ g) \land x = sum^((vol \circ (.)) \circ g))\} = \{y \in ℝ^{} \| \exists f \in ({ℝ^{2}}^{ℕ}) (A \subseteq ⋃ ran ((.) \circ f) \land y = sum^((vol \circ (.)) \circ f))\}$
18	1 17	ovolval4	$⊢ φ \to {vol}^{} (A) = inf (\{x \in ℝ^{} \| \exists g \in ({ℝ^{2}}^{ℕ}) (A \subseteq ⋃ ran ((.) \circ g) \land x = sum^((vol \circ (.)) \circ g))\} ℝ^{*} <)$
19	11	eqeq2d	$⊢ g = f \to (x = sum^((vol \circ (.)) \circ g) \leftrightarrow x = sum^((vol \circ (.)) \circ f))$
20	9 19	anbi12d	$⊢ g = f \to ((A \subseteq ⋃ ran ((.) \circ g) \land x = sum^((vol \circ (.)) \circ g)) \leftrightarrow (A \subseteq ⋃ ran ((.) \circ f) \land x = sum^((vol \circ (.)) \circ f)))$
21	20	cbvrexvw	$⊢ \exists g \in ({ℝ^{2}}^{ℕ}) (A \subseteq ⋃ ran ((.) \circ g) \land x = sum^((vol \circ (.)) \circ g)) \leftrightarrow \exists f \in ({ℝ^{2}}^{ℕ}) (A \subseteq ⋃ ran ((.) \circ f) \land x = sum^((vol \circ (.)) \circ f))$
22	21	a1i	$⊢ x = z \to (\exists g \in ({ℝ^{2}}^{ℕ}) (A \subseteq ⋃ ran ((.) \circ g) \land x = sum^((vol \circ (.)) \circ g)) \leftrightarrow \exists f \in ({ℝ^{2}}^{ℕ}) (A \subseteq ⋃ ran ((.) \circ f) \land x = sum^((vol \circ (.)) \circ f)))$
23		eqeq1	$⊢ x = z \to (x = sum^((vol \circ (.)) \circ f) \leftrightarrow z = sum^((vol \circ (.)) \circ f))$
24	23	anbi2d	$⊢ x = z \to ((A \subseteq ⋃ ran ((.) \circ f) \land x = sum^((vol \circ (.)) \circ f)) \leftrightarrow (A \subseteq ⋃ ran ((.) \circ f) \land z = sum^((vol \circ (.)) \circ f)))$
25	24	rexbidv	$⊢ x = z \to (\exists f \in ({ℝ^{2}}^{ℕ}) (A \subseteq ⋃ ran ((.) \circ f) \land x = sum^((vol \circ (.)) \circ f)) \leftrightarrow \exists f \in ({ℝ^{2}}^{ℕ}) (A \subseteq ⋃ ran ((.) \circ f) \land z = sum^((vol \circ (.)) \circ f)))$
26	22 25	bitrd	$⊢ x = z \to (\exists g \in ({ℝ^{2}}^{ℕ}) (A \subseteq ⋃ ran ((.) \circ g) \land x = sum^((vol \circ (.)) \circ g)) \leftrightarrow \exists f \in ({ℝ^{2}}^{ℕ}) (A \subseteq ⋃ ran ((.) \circ f) \land z = sum^((vol \circ (.)) \circ f)))$
27	26	cbvrabv	$⊢ \{x \in ℝ^{} \| \exists g \in ({ℝ^{2}}^{ℕ}) (A \subseteq ⋃ ran ((.) \circ g) \land x = sum^((vol \circ (.)) \circ g))\} = \{z \in ℝ^{} \| \exists f \in ({ℝ^{2}}^{ℕ}) (A \subseteq ⋃ ran ((.) \circ f) \land z = sum^((vol \circ (.)) \circ f))\}$
28	2 27	ovolval5lem3	$⊢ inf (\{x \in ℝ^{} \| \exists g \in ({ℝ^{2}}^{ℕ}) (A \subseteq ⋃ ran ((.) \circ g) \land x = sum^((vol \circ (.)) \circ g))\} ℝ^{} <) = inf (M ℝ^{*} <)$
29	28	a1i	$⊢ φ \to inf (\{x \in ℝ^{} \| \exists g \in ({ℝ^{2}}^{ℕ}) (A \subseteq ⋃ ran ((.) \circ g) \land x = sum^((vol \circ (.)) \circ g))\} ℝ^{} <) = inf (M ℝ^{*} <)$
30	18 29	eqtrd	$⊢ φ \to {vol}^{} (A) = inf (M ℝ^{} <)$

Metamath Proof Explorer

Theorem ovolval5

Proof