Metamath Proof Explorer


Theorem sibfmbl

Description: A simple function is measurable. (Contributed by Thierry Arnoux, 19-Feb-2018)

Ref Expression
Hypotheses sitgval.b B = Base W
sitgval.j J = TopOpen W
sitgval.s S = 𝛔 J
sitgval.0 0 ˙ = 0 W
sitgval.x · ˙ = W
sitgval.h H = ℝHom Scalar W
sitgval.1 φ W V
sitgval.2 φ M ran measures
sibfmbl.1 φ F M W
Assertion sibfmbl φ F dom M MblFn μ S

Proof

Step Hyp Ref Expression
1 sitgval.b B = Base W
2 sitgval.j J = TopOpen W
3 sitgval.s S = 𝛔 J
4 sitgval.0 0 ˙ = 0 W
5 sitgval.x · ˙ = W
6 sitgval.h H = ℝHom Scalar W
7 sitgval.1 φ W V
8 sitgval.2 φ M ran measures
9 sibfmbl.1 φ F M W
10 1 2 3 4 5 6 7 8 issibf φ F M W F dom M MblFn μ S ran F Fin x ran F 0 ˙ M F -1 x 0 +∞
11 9 10 mpbid φ F dom M MblFn μ S ran F Fin x ran F 0 ˙ M F -1 x 0 +∞
12 11 simp1d φ F dom M MblFn μ S