Description: A Borel measurable function is Lebesgue measurable. Proposition 121D (a) of Fremlin1 p. 36 . (Contributed by Glauco Siliprandi, 26-Jun-2021)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | bormflebmf.x | |- ( ph -> X e. Fin ) |
|
| bormflebmf.b | |- B = ( SalGen ` ( TopOpen ` ( RR^ ` X ) ) ) |
||
| bormflebmf.l | |- L = dom ( voln ` X ) |
||
| bormflebmf.f | |- ( ph -> F e. ( SMblFn ` B ) ) |
||
| Assertion | bormflebmf | |- ( ph -> F e. ( SMblFn ` L ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | bormflebmf.x | |- ( ph -> X e. Fin ) |
|
| 2 | bormflebmf.b | |- B = ( SalGen ` ( TopOpen ` ( RR^ ` X ) ) ) |
|
| 3 | bormflebmf.l | |- L = dom ( voln ` X ) |
|
| 4 | bormflebmf.f | |- ( ph -> F e. ( SMblFn ` B ) ) |
|
| 5 | fvexd | |- ( ph -> ( TopOpen ` ( RR^ ` X ) ) e. _V ) |
|
| 6 | 5 2 | salgencld | |- ( ph -> B e. SAlg ) |
| 7 | 1 3 | dmovnsal | |- ( ph -> L e. SAlg ) |
| 8 | 1 3 2 | borelmbl | |- ( ph -> B C_ L ) |
| 9 | 6 7 8 4 | smfsssmf | |- ( ph -> F e. ( SMblFn ` L ) ) |