Metamath Proof Explorer

Theorem elmbfmvol2

Description: Measurable functions with respect to the Lebesgue measure. We only have the inclusion, since MblFn includes complex-valued functions. (Contributed by Thierry Arnoux, 26-Jan-2017)

Ref Expression
Assertion elmbfmvol2 ⊢ F ∈ dom ⁡ vol MblFn μ 𝔅 ℝ → F ∈ MblFn

Proof

Step Hyp Ref Expression
1 retopbas ⊢ ran ⁡ . ∈ TopBases
2 bastg ⊢ ran ⁡ . ∈ TopBases → ran ⁡ . ⊆ topGen ⁡ ran ⁡ .
3 1 2 ax-mp ⊢ ran ⁡ . ⊆ topGen ⁡ ran ⁡ .
4 retop ⊢ topGen ⁡ ran ⁡ . ∈ Top
5 sssigagen ⊢ topGen ⁡ ran ⁡ . ∈ Top → topGen ⁡ ran ⁡ . ⊆ 𝛔 ⁡ topGen ⁡ ran ⁡ .
6 4 5 ax-mp ⊢ topGen ⁡ ran ⁡ . ⊆ 𝛔 ⁡ topGen ⁡ ran ⁡ .
7 3 6 sstri ⊢ ran ⁡ . ⊆ 𝛔 ⁡ topGen ⁡ ran ⁡ .
8 df-brsiga ⊢ 𝔅 ℝ = 𝛔 ⁡ topGen ⁡ ran ⁡ .
9 7 8 sseqtrri ⊢ ran ⁡ . ⊆ 𝔅 ℝ
10 eqid ⊢ vol = vol
11 dmvlsiga ⊢ dom ⁡ vol ∈ sigAlgebra ⁡ ℝ
12 elrnsiga ⊢ dom ⁡ vol ∈ sigAlgebra ⁡ ℝ → dom ⁡ vol ∈ ⋃ ran ⁡ sigAlgebra
13 11 12 mp1i ⊢ vol = vol → dom ⁡ vol ∈ ⋃ ran ⁡ sigAlgebra
14 brsigarn ⊢ 𝔅 ℝ ∈ sigAlgebra ⁡ ℝ
15 elrnsiga ⊢ 𝔅 ℝ ∈ sigAlgebra ⁡ ℝ → 𝔅 ℝ ∈ ⋃ ran ⁡ sigAlgebra
16 14 15 mp1i ⊢ vol = vol → 𝔅 ℝ ∈ ⋃ ran ⁡ sigAlgebra
17 13 16 ismbfm ⊢ vol = vol → F ∈ dom ⁡ vol MblFn μ 𝔅 ℝ ↔ F ∈ ⋃ 𝔅 ℝ ⋃ dom ⁡ vol ∧ ∀ x ∈ 𝔅 ℝ F -1 x ∈ dom ⁡ vol
18 10 17 ax-mp ⊢ F ∈ dom ⁡ vol MblFn μ 𝔅 ℝ ↔ F ∈ ⋃ 𝔅 ℝ ⋃ dom ⁡ vol ∧ ∀ x ∈ 𝔅 ℝ F -1 x ∈ dom ⁡ vol
19 18 simprbi ⊢ F ∈ dom ⁡ vol MblFn μ 𝔅 ℝ → ∀ x ∈ 𝔅 ℝ F -1 x ∈ dom ⁡ vol
20 ssralv ⊢ ran ⁡ . ⊆ 𝔅 ℝ → ∀ x ∈ 𝔅 ℝ F -1 x ∈ dom ⁡ vol → ∀ x ∈ ran ⁡ . F -1 x ∈ dom ⁡ vol
21 9 19 20 mpsyl ⊢ F ∈ dom ⁡ vol MblFn μ 𝔅 ℝ → ∀ x ∈ ran ⁡ . F -1 x ∈ dom ⁡ vol
22 18 simplbi ⊢ F ∈ dom ⁡ vol MblFn μ 𝔅 ℝ → F ∈ ⋃ 𝔅 ℝ ⋃ dom ⁡ vol
23 elmapi ⊢ F ∈ ℝ ℝ → F : ℝ ⟶ ℝ
24 unibrsiga ⊢ ⋃ 𝔅 ℝ = ℝ
25 unidmvol ⊢ ⋃ dom ⁡ vol = ℝ
26 24 25 oveq12i ⊢ ⋃ 𝔅 ℝ ⋃ dom ⁡ vol = ℝ ℝ
27 23 26 eleq2s ⊢ F ∈ ⋃ 𝔅 ℝ ⋃ dom ⁡ vol → F : ℝ ⟶ ℝ
28 ismbf ⊢ F : ℝ ⟶ ℝ → F ∈ MblFn ↔ ∀ x ∈ ran ⁡ . F -1 x ∈ dom ⁡ vol
29 22 27 28 3syl ⊢ F ∈ dom ⁡ vol MblFn μ 𝔅 ℝ → F ∈ MblFn ↔ ∀ x ∈ ran ⁡ . F -1 x ∈ dom ⁡ vol
30 21 29 mpbird ⊢ F ∈ dom ⁡ vol MblFn μ 𝔅 ℝ → F ∈ MblFn