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 ⁡ x 2 nd ⁡ x = . ⁡ 1 st ⁡ x 2 nd ⁡ x
6 5 a1i ⊢ x ∈ ℝ * × ℝ * → 1 st ⁡ x 2 nd ⁡ x = . ⁡ 1 st ⁡ x 2 nd ⁡ x
7 1st2nd2 ⊢ x ∈ ℝ * × ℝ * → x = 1 st ⁡ x 2 nd ⁡ x
8 7 eqcomd ⊢ x ∈ ℝ * × ℝ * → 1 st ⁡ x 2 nd ⁡ x = x
9 8 fveq2d ⊢ x ∈ ℝ * × ℝ * → . ⁡ 1 st ⁡ x 2 nd ⁡ x = . ⁡ x
10 6 9 eqtr2d ⊢ x ∈ ℝ * × ℝ * → . ⁡ x = 1 st ⁡ x 2 nd ⁡ x
11 ioombl ⊢ 1 st ⁡ x 2 nd ⁡ x ∈ dom ⁡ vol
12 10 11 eqeltrdi ⊢ x ∈ ℝ * × ℝ * → . ⁡ x ∈ dom ⁡ vol
13 12 rgen ⊢ ∀ x ∈ ℝ * × ℝ * . ⁡ x ∈ dom ⁡ vol
14 4 13 pm3.2i ⊢ . Fn ℝ * × ℝ * ∧ ∀ x ∈ ℝ * × ℝ * . ⁡ x ∈ dom ⁡ vol
15 ffnfv ⊢ . : ℝ * × ℝ * ⟶ dom ⁡ vol ↔ . Fn ℝ * × ℝ * ∧ ∀ x ∈ ℝ * × ℝ * . ⁡ x ∈ 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 +∞