Description: A measurable function to a Borel Set is measurable. (Contributed by Thierry Arnoux, 24-Jan-2017) Remove hypotheses. (Revised by SN, 13-Jan-2025)
| Ref | Expression | ||
|---|---|---|---|
| Hypothesis | mbfmbfm.1 | |- ( ph -> F e. ( dom M MblFnM ( sigaGen ` J ) ) ) |
|
| Assertion | mbfmbfm | |- ( ph -> F e. U. ran MblFnM ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | mbfmbfm.1 | |- ( ph -> F e. ( dom M MblFnM ( sigaGen ` J ) ) ) |
|
| 2 | 1 | isanmbfm | |- ( ph -> F e. U. ran MblFnM ) |