Description: A measurable function to a Borel Set is measurable. (Contributed by Thierry Arnoux, 24-Jan-2017)
Ref | Expression | ||
---|---|---|---|
Hypotheses | mbfmbfm.1 | |
|
mbfmbfm.2 | |
||
mbfmbfm.3 | |
||
Assertion | mbfmbfm | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | mbfmbfm.1 | |
|
2 | mbfmbfm.2 | |
|
3 | mbfmbfm.3 | |
|
4 | measbasedom | |
|
5 | 4 | biimpi | |
6 | measbase | |
|
7 | 1 5 6 | 3syl | |
8 | 2 | sgsiga | |
9 | 7 8 3 | isanmbfm | |