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 ∘ (,) ) : ( ℝ^* × ℝ^* ) ⟶ ( 0 [,] +∞ )

Proof

Step	Hyp	Ref	Expression
1		volf	⊢ vol : dom vol ⟶ ( 0 [,] +∞ )
2		ioof	⊢ (,) : ( ℝ^* × ℝ^* ) ⟶ 𝒫 ℝ
3		ffn	⊢ ( (,) : ( ℝ^* × ℝ^* ) ⟶ 𝒫 ℝ → (,) Fn ( ℝ^* × ℝ^* ) )
4	2 3	ax-mp	⊢ (,) Fn ( ℝ^* × ℝ^* )
5		df-ov	⊢ ( ( 1^st ‘ 𝑥 ) (,) ( 2^nd ‘ 𝑥 ) ) = ( (,) ‘ ⟨ ( 1^st ‘ 𝑥 ) , ( 2^nd ‘ 𝑥 ) ⟩ )
6	5	a1i	⊢ ( 𝑥 ∈ ( ℝ^* × ℝ^* ) → ( ( 1^st ‘ 𝑥 ) (,) ( 2^nd ‘ 𝑥 ) ) = ( (,) ‘ ⟨ ( 1^st ‘ 𝑥 ) , ( 2^nd ‘ 𝑥 ) ⟩ ) )
7		1st2nd2	⊢ ( 𝑥 ∈ ( ℝ^* × ℝ^* ) → 𝑥 = ⟨ ( 1^st ‘ 𝑥 ) , ( 2^nd ‘ 𝑥 ) ⟩ )
8	7	eqcomd	⊢ ( 𝑥 ∈ ( ℝ^* × ℝ^* ) → ⟨ ( 1^st ‘ 𝑥 ) , ( 2^nd ‘ 𝑥 ) ⟩ = 𝑥 )
9	8	fveq2d	⊢ ( 𝑥 ∈ ( ℝ^* × ℝ^* ) → ( (,) ‘ ⟨ ( 1^st ‘ 𝑥 ) , ( 2^nd ‘ 𝑥 ) ⟩ ) = ( (,) ‘ 𝑥 ) )
10	6 9	eqtr2d	⊢ ( 𝑥 ∈ ( ℝ^* × ℝ^* ) → ( (,) ‘ 𝑥 ) = ( ( 1^st ‘ 𝑥 ) (,) ( 2^nd ‘ 𝑥 ) ) )
11		ioombl	⊢ ( ( 1^st ‘ 𝑥 ) (,) ( 2^nd ‘ 𝑥 ) ) ∈ dom vol
12	10 11	eqeltrdi	⊢ ( 𝑥 ∈ ( ℝ^* × ℝ^* ) → ( (,) ‘ 𝑥 ) ∈ dom vol )
13	12	rgen	⊢ ∀ 𝑥 ∈ ( ℝ^* × ℝ^* ) ( (,) ‘ 𝑥 ) ∈ dom vol
14	4 13	pm3.2i	⊢ ( (,) Fn ( ℝ^* × ℝ^* ) ∧ ∀ 𝑥 ∈ ( ℝ^* × ℝ^* ) ( (,) ‘ 𝑥 ) ∈ dom vol )
15		ffnfv	⊢ ( (,) : ( ℝ^* × ℝ^* ) ⟶ dom vol ↔ ( (,) Fn ( ℝ^* × ℝ^* ) ∧ ∀ 𝑥 ∈ ( ℝ^* × ℝ^* ) ( (,) ‘ 𝑥 ) ∈ dom vol ) )
16	14 15	mpbir	⊢ (,) : ( ℝ^* × ℝ^* ) ⟶ dom vol
17		fco	⊢ ( ( vol : dom vol ⟶ ( 0 [,] +∞ ) ∧ (,) : ( ℝ^* × ℝ^* ) ⟶ dom vol ) → ( vol ∘ (,) ) : ( ℝ^* × ℝ^* ) ⟶ ( 0 [,] +∞ ) )
18	1 16 17	mp2an	⊢ ( vol ∘ (,) ) : ( ℝ^* × ℝ^* ) ⟶ ( 0 [,] +∞ )