Metamath Proof Explorer

Theorem ovnovol

Description: The 1-dimensional Lebesgue outer measure agrees with the Lebesgue outer measure on subsets of Real numbers. (Contributed by Glauco Siliprandi, 3-Mar-2021)

		Ref	Expression
	Hypotheses	ovnovol.a	$⊢ φ \to A \in V$
		ovnovol.b	$⊢ φ \to B \subseteq ℝ$
	Assertion	ovnovol	$⊢ φ \to voln* (\{A\}) (B^{\{A\}}) = {vol}^{*} (B)$

Proof

Step	Hyp	Ref	Expression
1		ovnovol.a	$⊢ φ \to A \in V$
2		ovnovol.b	$⊢ φ \to B \subseteq ℝ$
3		eqid	$⊢ \{z \in ℝ^{} \| \exists i \in ({({ℝ^{2}}^{\{A\}})}^{ℕ}) (B^{\{A\}} \subseteq ⋃_{j \in ℕ} \underset{k \in \{A\}}{⨉} ([.) \circ i (j)) (k) \land z = sum^((j \in ℕ ⟼ \prod_{k \in \{A\}} vol (([.) \circ i (j)) (k)))))\} = \{z \in ℝ^{} \| \exists i \in ({({ℝ^{2}}^{\{A\}})}^{ℕ}) (B^{\{A\}} \subseteq ⋃_{j \in ℕ} \underset{k \in \{A\}}{⨉} ([.) \circ i (j)) (k) \land z = sum^((j \in ℕ ⟼ \prod_{k \in \{A\}} vol (([.) \circ i (j)) (k)))))\}$
4		eqeq1	$⊢ w = z \to (w = sum^((vol \circ [.)) \circ f) \leftrightarrow z = sum^((vol \circ [.)) \circ f))$
5	4	anbi2d	$⊢ w = z \to ((B \subseteq ⋃ ran ([.) \circ f) \land w = sum^((vol \circ [.)) \circ f)) \leftrightarrow (B \subseteq ⋃ ran ([.) \circ f) \land z = sum^((vol \circ [.)) \circ f)))$
6	5	rexbidv	$⊢ w = z \to (\exists f \in ({ℝ^{2}}^{ℕ}) (B \subseteq ⋃ ran ([.) \circ f) \land w = sum^((vol \circ [.)) \circ f)) \leftrightarrow \exists f \in ({ℝ^{2}}^{ℕ}) (B \subseteq ⋃ ran ([.) \circ f) \land z = sum^((vol \circ [.)) \circ f)))$
7	6	cbvrabv	$⊢ \{w \in ℝ^{} \| \exists f \in ({ℝ^{2}}^{ℕ}) (B \subseteq ⋃ ran ([.) \circ f) \land w = sum^((vol \circ [.)) \circ f))\} = \{z \in ℝ^{} \| \exists f \in ({ℝ^{2}}^{ℕ}) (B \subseteq ⋃ ran ([.) \circ f) \land z = sum^((vol \circ [.)) \circ f))\}$
8	1 2 3 7	ovnovollem3	$⊢ φ \to voln* (\{A\}) (B^{\{A\}}) = {vol}^{*} (B)$