Metamath Proof Explorer


Theorem ismbf

Description: The predicate " F is a measurable function". A function is measurable iff the preimages of all open intervals are measurable sets in the sense of ismbl . (Contributed by Mario Carneiro, 17-Jun-2014)

Ref Expression
Assertion ismbf F : A F MblFn x ran . F -1 x dom vol

Proof

Step Hyp Ref Expression
1 mbfdm F MblFn dom F dom vol
2 fdm F : A dom F = A
3 2 eleq1d F : A dom F dom vol A dom vol
4 1 3 syl5ib F : A F MblFn A dom vol
5 ioomax −∞ +∞ =
6 ioorebas −∞ +∞ ran .
7 5 6 eqeltrri ran .
8 imaeq2 x = F -1 x = F -1
9 8 eleq1d x = F -1 x dom vol F -1 dom vol
10 9 rspcv ran . x ran . F -1 x dom vol F -1 dom vol
11 7 10 ax-mp x ran . F -1 x dom vol F -1 dom vol
12 fimacnv F : A F -1 = A
13 12 eleq1d F : A F -1 dom vol A dom vol
14 11 13 syl5ib F : A x ran . F -1 x dom vol A dom vol
15 ffvelrn F : A x A F x
16 15 adantlr F : A A dom vol x A F x
17 16 rered F : A A dom vol x A F x = F x
18 17 mpteq2dva F : A A dom vol x A F x = x A F x
19 16 recnd F : A A dom vol x A F x
20 simpl F : A A dom vol F : A
21 20 feqmptd F : A A dom vol F = x A F x
22 ref :
23 22 a1i F : A A dom vol :
24 23 feqmptd F : A A dom vol = y y
25 fveq2 y = F x y = F x
26 19 21 24 25 fmptco F : A A dom vol F = x A F x
27 18 26 21 3eqtr4rd F : A A dom vol F = F
28 27 cnveqd F : A A dom vol F -1 = F -1
29 28 imaeq1d F : A A dom vol F -1 x = F -1 x
30 29 eleq1d F : A A dom vol F -1 x dom vol F -1 x dom vol
31 imf :
32 31 a1i F : A A dom vol :
33 32 feqmptd F : A A dom vol = y y
34 fveq2 y = F x y = F x
35 19 21 33 34 fmptco F : A A dom vol F = x A F x
36 16 reim0d F : A A dom vol x A F x = 0
37 36 mpteq2dva F : A A dom vol x A F x = x A 0
38 35 37 eqtrd F : A A dom vol F = x A 0
39 fconstmpt A × 0 = x A 0
40 38 39 syl6eqr F : A A dom vol F = A × 0
41 40 cnveqd F : A A dom vol F -1 = A × 0 -1
42 41 imaeq1d F : A A dom vol F -1 x = A × 0 -1 x
43 simpr F : A A dom vol A dom vol
44 0re 0
45 mbfconstlem A dom vol 0 A × 0 -1 x dom vol
46 43 44 45 sylancl F : A A dom vol A × 0 -1 x dom vol
47 42 46 eqeltrd F : A A dom vol F -1 x dom vol
48 47 biantrud F : A A dom vol F -1 x dom vol F -1 x dom vol F -1 x dom vol
49 30 48 bitrd F : A A dom vol F -1 x dom vol F -1 x dom vol F -1 x dom vol
50 49 ralbidv F : A A dom vol x ran . F -1 x dom vol x ran . F -1 x dom vol F -1 x dom vol
51 ax-resscn
52 fss F : A F : A
53 51 52 mpan2 F : A F : A
54 mblss A dom vol A
55 cnex V
56 reex V
57 elpm2r V V F : A A F 𝑝𝑚
58 55 56 57 mpanl12 F : A A F 𝑝𝑚
59 53 54 58 syl2an F : A A dom vol F 𝑝𝑚
60 59 biantrurd F : A A dom vol x ran . F -1 x dom vol F -1 x dom vol F 𝑝𝑚 x ran . F -1 x dom vol F -1 x dom vol
61 50 60 bitrd F : A A dom vol x ran . F -1 x dom vol F 𝑝𝑚 x ran . F -1 x dom vol F -1 x dom vol
62 ismbf1 F MblFn F 𝑝𝑚 x ran . F -1 x dom vol F -1 x dom vol
63 61 62 syl6rbbr F : A A dom vol F MblFn x ran . F -1 x dom vol
64 63 ex F : A A dom vol F MblFn x ran . F -1 x dom vol
65 4 14 64 pm5.21ndd F : A F MblFn x ran . F -1 x dom vol