Metamath Proof Explorer

Theorem vonvolmbl2

Description: A subset X of the space of 1-dimensional Real numbers is Lebesgue measurable if and only if its projection Y on the Real numbers is Lebesgue measure. (Contributed by Glauco Siliprandi, 3-Mar-2021)

		Ref	Expression
	Hypotheses	vonvolmbl2.f	$⊢ \underline{Ⅎ} f Y$
		vonvolmbl2.a	$⊢ φ \to A \in V$
		vonvolmbl2.x	$⊢ φ \to X \subseteq ℝ^{\{A\}}$
		vonvolmbl2.y	$⊢ Y = ⋃_{f \in X} ran f$
	Assertion	vonvolmbl2	$⊢ φ \to (X \in dom voln (\{A\}) \leftrightarrow Y \in dom vol)$

Proof

Step	Hyp	Ref	Expression
1		vonvolmbl2.f	$⊢ \underline{Ⅎ} f Y$
2		vonvolmbl2.a	$⊢ φ \to A \in V$
3		vonvolmbl2.x	$⊢ φ \to X \subseteq ℝ^{\{A\}}$
4		vonvolmbl2.y	$⊢ Y = ⋃_{f \in X} ran f$
5	1 2 3 4	ssmapsn	$⊢ φ \to X = Y^{\{A\}}$
6	5	eleq1d	$⊢ φ \to (X \in dom voln (\{A\}) \leftrightarrow Y^{\{A\}} \in dom voln (\{A\}))$
7	3	adantr	$⊢ (φ \land f \in X) \to X \subseteq ℝ^{\{A\}}$
8		simpr	$⊢ (φ \land f \in X) \to f \in X$
9	7 8	sseldd	$⊢ (φ \land f \in X) \to f \in (ℝ^{\{A\}})$
10		elmapi	$⊢ f \in (ℝ^{\{A\}}) \to f : \{A\} ⟶ ℝ$
11		frn	$⊢ f : \{A\} ⟶ ℝ \to ran f \subseteq ℝ$
12	9 10 11	3syl	$⊢ (φ \land f \in X) \to ran f \subseteq ℝ$
13	12	ralrimiva	$⊢ φ \to \forall f \in X ran f \subseteq ℝ$
14		iunss	$⊢ ⋃_{f \in X} ran f \subseteq ℝ \leftrightarrow \forall f \in X ran f \subseteq ℝ$
15	13 14	sylibr	$⊢ φ \to ⋃_{f \in X} ran f \subseteq ℝ$
16	4 15	eqsstrid	$⊢ φ \to Y \subseteq ℝ$
17	2 16	vonvolmbl	$⊢ φ \to (Y^{\{A\}} \in dom voln (\{A\}) \leftrightarrow Y \in dom vol)$
18	6 17	bitrd	$⊢ φ \to (X \in dom voln (\{A\}) \leftrightarrow Y \in dom vol)$