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 ( 𝐹 ∈ ( dom vol MblFnM 𝔅ℝ ) → 𝐹 ∈ 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 (,) ) ⊆ ( sigaGen ‘ ( topGen ‘ ran (,) ) ) )
6 4 5 ax-mp ⊢ ( topGen ‘ ran (,) ) ⊆ ( sigaGen ‘ ( topGen ‘ ran (,) ) )
7 3 6 sstri ⊢ ran (,) ⊆ ( sigaGen ‘ ( topGen ‘ ran (,) ) )
8 df-brsiga ⊢ 𝔅ℝ = ( sigaGen ‘ ( 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 → ( 𝐹 ∈ ( dom vol MblFnM 𝔅ℝ ) ↔ ( 𝐹 ∈ ( ∪ 𝔅ℝ ↑m ∪ dom vol ) ∧ ∀ 𝑥 ∈ 𝔅ℝ ( ◡ 𝐹 “ 𝑥 ) ∈ dom vol ) ) )
18 10 17 ax-mp ⊢ ( 𝐹 ∈ ( dom vol MblFnM 𝔅ℝ ) ↔ ( 𝐹 ∈ ( ∪ 𝔅ℝ ↑m ∪ dom vol ) ∧ ∀ 𝑥 ∈ 𝔅ℝ ( ◡ 𝐹 “ 𝑥 ) ∈ dom vol ) )
19 18 simprbi ⊢ ( 𝐹 ∈ ( dom vol MblFnM 𝔅ℝ ) → ∀ 𝑥 ∈ 𝔅ℝ ( ◡ 𝐹 “ 𝑥 ) ∈ dom vol )
20 ssralv ⊢ ( ran (,) ⊆ 𝔅ℝ → ( ∀ 𝑥 ∈ 𝔅ℝ ( ◡ 𝐹 “ 𝑥 ) ∈ dom vol → ∀ 𝑥 ∈ ran (,) ( ◡ 𝐹 “ 𝑥 ) ∈ dom vol ) )
21 9 19 20 mpsyl ⊢ ( 𝐹 ∈ ( dom vol MblFnM 𝔅ℝ ) → ∀ 𝑥 ∈ ran (,) ( ◡ 𝐹 “ 𝑥 ) ∈ dom vol )
22 18 simplbi ⊢ ( 𝐹 ∈ ( dom vol MblFnM 𝔅ℝ ) → 𝐹 ∈ ( ∪ 𝔅ℝ ↑m ∪ dom vol ) )
23 elmapi ⊢ ( 𝐹 ∈ ( ℝ ↑m ℝ ) → 𝐹 : ℝ ⟶ ℝ )
24 unibrsiga ⊢ ∪ 𝔅ℝ = ℝ
25 unidmvol ⊢ ∪ dom vol = ℝ
26 24 25 oveq12i ⊢ ( ∪ 𝔅ℝ ↑m ∪ dom vol ) = ( ℝ ↑m ℝ )
27 23 26 eleq2s ⊢ ( 𝐹 ∈ ( ∪ 𝔅ℝ ↑m ∪ dom vol ) → 𝐹 : ℝ ⟶ ℝ )
28 ismbf ⊢ ( 𝐹 : ℝ ⟶ ℝ → ( 𝐹 ∈ MblFn ↔ ∀ 𝑥 ∈ ran (,) ( ◡ 𝐹 “ 𝑥 ) ∈ dom vol ) )
29 22 27 28 3syl ⊢ ( 𝐹 ∈ ( dom vol MblFnM 𝔅ℝ ) → ( 𝐹 ∈ MblFn ↔ ∀ 𝑥 ∈ ran (,) ( ◡ 𝐹 “ 𝑥 ) ∈ dom vol ) )
30 21 29 mpbird ⊢ ( 𝐹 ∈ ( dom vol MblFnM 𝔅ℝ ) → 𝐹 ∈ MblFn )