Metamath Proof Explorer


Theorem mbfima

Description: Definitional property of a measurable function: the preimage of an open right-unbounded interval is measurable. (Contributed by Mario Carneiro, 17-Jun-2014)

Ref Expression
Assertion mbfima F MblFn F : A F -1 B C dom vol

Proof

Step Hyp Ref Expression
1 ismbf F : A F MblFn x ran . F -1 x dom vol
2 1 biimpac F MblFn F : A x ran . F -1 x dom vol
3 ioof . : * × * 𝒫
4 ffn . : * × * 𝒫 . Fn * × *
5 3 4 ax-mp . Fn * × *
6 fnovrn . Fn * × * B * C * B C ran .
7 5 6 mp3an1 B * C * B C ran .
8 imaeq2 x = B C F -1 x = F -1 B C
9 8 eleq1d x = B C F -1 x dom vol F -1 B C dom vol
10 9 rspccva x ran . F -1 x dom vol B C ran . F -1 B C dom vol
11 2 7 10 syl2an F MblFn F : A B * C * F -1 B C dom vol
12 ndmioo ¬ B * C * B C =
13 12 imaeq2d ¬ B * C * F -1 B C = F -1
14 ima0 F -1 =
15 13 14 syl6eq ¬ B * C * F -1 B C =
16 0mbl dom vol
17 15 16 eqeltrdi ¬ B * C * F -1 B C dom vol
18 17 adantl F MblFn F : A ¬ B * C * F -1 B C dom vol
19 11 18 pm2.61dan F MblFn F : A F -1 B C dom vol