Metamath Proof Explorer

Theorem volioof

Description: The function that assigns the Lebesgue measure to open intervals. (Contributed by Glauco Siliprandi, 3-Mar-2021)

		Ref	Expression
	Assertion	volioof	$⊢ (vol \circ (.)) : ℝ^{} \times ℝ^{} ⟶ [0, +∞]$

Proof

Step	Hyp	Ref	Expression
1		volf	$⊢ vol : dom vol ⟶ [0, +∞]$
2		ioof	$⊢ (.) : ℝ^{} \times ℝ^{} ⟶ 𝒫 ℝ$
3		ffn	$⊢ (.) : ℝ^{} \times ℝ^{} ⟶ 𝒫 ℝ \to (.) Fn (ℝ^{} \times ℝ^{})$
4	2 3	ax-mp	$⊢ (.) Fn (ℝ^{} \times ℝ^{})$
5		df-ov	$⊢ (1^{st} (x), 2^{nd} (x)) = (.) (⟨1^{st} (x), 2^{nd} (x)⟩)$
6	5	a1i	$⊢ x \in (ℝ^{} \times ℝ^{}) \to (1^{st} (x), 2^{nd} (x)) = (.) (⟨1^{st} (x), 2^{nd} (x)⟩)$
7		1st2nd2	$⊢ x \in (ℝ^{} \times ℝ^{}) \to x = ⟨1^{st} (x), 2^{nd} (x)⟩$
8	7	eqcomd	$⊢ x \in (ℝ^{} \times ℝ^{}) \to ⟨1^{st} (x), 2^{nd} (x)⟩ = x$
9	8	fveq2d	$⊢ x \in (ℝ^{} \times ℝ^{}) \to (.) (⟨1^{st} (x), 2^{nd} (x)⟩) = (.) (x)$
10	6 9	eqtr2d	$⊢ x \in (ℝ^{} \times ℝ^{}) \to (.) (x) = (1^{st} (x), 2^{nd} (x))$
11		ioombl	$⊢ (1^{st} (x), 2^{nd} (x)) \in dom vol$
12	10 11	eqeltrdi	$⊢ x \in (ℝ^{} \times ℝ^{}) \to (.) (x) \in dom vol$
13	12	rgen	$⊢ \forall x \in (ℝ^{} \times ℝ^{}) (.) (x) \in dom vol$
14	4 13	pm3.2i	$⊢ ((.) Fn (ℝ^{} \times ℝ^{}) \land \forall x \in (ℝ^{} \times ℝ^{}) (.) (x) \in dom vol)$
15		ffnfv	$⊢ (.) : ℝ^{} \times ℝ^{} ⟶ dom vol \leftrightarrow ((.) Fn (ℝ^{} \times ℝ^{}) \land \forall x \in (ℝ^{} \times ℝ^{}) (.) (x) \in dom vol)$
16	14 15	mpbir	$⊢ (.) : ℝ^{} \times ℝ^{} ⟶ dom vol$
17		fco	$⊢ (vol : dom vol ⟶ [0, +∞] \land (.) : ℝ^{} \times ℝ^{} ⟶ dom vol) \to (vol \circ (.)) : ℝ^{} \times ℝ^{} ⟶ [0, +∞]$
18	1 16 17	mp2an	$⊢ (vol \circ (.)) : ℝ^{} \times ℝ^{} ⟶ [0, +∞]$