vonvol2

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

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

Proof

Step	Hyp	Ref	Expression
1		vonvol2.f	$⊢ \underline{Ⅎ} f Y$
2		vonvol2.a	$⊢ φ \to A \in V$
3		vonvol2.x	$⊢ φ \to X \in dom voln (\{A\})$
4		vonvol2.y	$⊢ Y = ⋃_{f \in X} ran f$
5		snfi	$⊢ \{A\} \in Fin$
6	5	a1i	$⊢ φ \to \{A\} \in Fin$
7	6 3	vonmblss2	$⊢ φ \to X \subseteq ℝ^{\{A\}}$
8	1 2 7 4	ssmapsn	$⊢ φ \to X = Y^{\{A\}}$
9	8	eqcomd	$⊢ φ \to Y^{\{A\}} = X$
10	9 3	eqeltrd	$⊢ φ \to Y^{\{A\}} \in dom voln (\{A\})$
11	7	adantr	$⊢ (φ \land f \in X) \to X \subseteq ℝ^{\{A\}}$
12		simpr	$⊢ (φ \land f \in X) \to f \in X$
13	11 12	sseldd	$⊢ (φ \land f \in X) \to f \in (ℝ^{\{A\}})$
14		elmapi	$⊢ f \in (ℝ^{\{A\}}) \to f : \{A\} ⟶ ℝ$
15		frn	$⊢ f : \{A\} ⟶ ℝ \to ran f \subseteq ℝ$
16	13 14 15	3syl	$⊢ (φ \land f \in X) \to ran f \subseteq ℝ$
17	16	ralrimiva	$⊢ φ \to \forall f \in X ran f \subseteq ℝ$
18		iunss	$⊢ ⋃_{f \in X} ran f \subseteq ℝ \leftrightarrow \forall f \in X ran f \subseteq ℝ$
19	17 18	sylibr	$⊢ φ \to ⋃_{f \in X} ran f \subseteq ℝ$
20	4 19	eqsstrid	$⊢ φ \to Y \subseteq ℝ$
21	2 20	vonvolmbl	$⊢ φ \to (Y^{\{A\}} \in dom voln (\{A\}) \leftrightarrow Y \in dom vol)$
22	10 21	mpbid	$⊢ φ \to Y \in dom vol$
23	2 22	vonvol	$⊢ φ \to voln (\{A\}) (Y^{\{A\}}) = vol (Y)$
24	9	eqcomd	$⊢ φ \to X = Y^{\{A\}}$
25	24	fveq2d	$⊢ φ \to voln (\{A\}) (X) = voln (\{A\}) (Y^{\{A\}})$
26		eqidd	$⊢ φ \to vol (Y) = vol (Y)$
27	23 25 26	3eqtr4d	$⊢ φ \to voln (\{A\}) (X) = vol (Y)$

Metamath Proof Explorer

Theorem vonvol2

Proof