Metamath Proof Explorer


Theorem ismbfd

Description: Deduction to prove measurability of a real function. The third hypothesis is not necessary, but the proof of this requires countable choice, so we derive this separately as ismbf3d . (Contributed by Mario Carneiro, 18-Jun-2014)

Ref Expression
Hypotheses ismbfd.1 φF:A
ismbfd.2 φx*F-1x+∞domvol
ismbfd.3 φx*F-1−∞xdomvol
Assertion ismbfd φFMblFn

Proof

Step Hyp Ref Expression
1 ismbfd.1 φF:A
2 ismbfd.2 φx*F-1x+∞domvol
3 ismbfd.3 φx*F-1−∞xdomvol
4 ioof .:*×*𝒫
5 ffn .:*×*𝒫.Fn*×*
6 ovelrn .Fn*×*zran.x*y*z=xy
7 4 5 6 mp2b zran.x*y*z=xy
8 simprl φx*y*x*
9 pnfxr +∞*
10 9 a1i φx*y*+∞*
11 mnfxr −∞*
12 11 a1i φx*y*−∞*
13 simprr φx*y*y*
14 iooin x*+∞*−∞*y*x+∞−∞y=ifx−∞−∞xif+∞y+∞y
15 8 10 12 13 14 syl22anc φx*y*x+∞−∞y=ifx−∞−∞xif+∞y+∞y
16 ifcl −∞*x*ifx−∞−∞x*
17 11 8 16 sylancr φx*y*ifx−∞−∞x*
18 mnfle x*−∞x
19 xrleid x*xx
20 breq1 −∞=ifx−∞−∞x−∞xifx−∞−∞xx
21 breq1 x=ifx−∞−∞xxxifx−∞−∞xx
22 20 21 ifboth −∞xxxifx−∞−∞xx
23 18 19 22 syl2anc x*ifx−∞−∞xx
24 23 ad2antrl φx*y*ifx−∞−∞xx
25 xrmax1 x*−∞*xifx−∞−∞x
26 8 11 25 sylancl φx*y*xifx−∞−∞x
27 17 8 24 26 xrletrid φx*y*ifx−∞−∞x=x
28 ifcl +∞*y*if+∞y+∞y*
29 9 13 28 sylancr φx*y*if+∞y+∞y*
30 xrmin2 +∞*y*if+∞y+∞yy
31 9 13 30 sylancr φx*y*if+∞y+∞yy
32 pnfge y*y+∞
33 xrleid y*yy
34 breq2 +∞=if+∞y+∞yy+∞yif+∞y+∞y
35 breq2 y=if+∞y+∞yyyyif+∞y+∞y
36 34 35 ifboth y+∞yyyif+∞y+∞y
37 32 33 36 syl2anc y*yif+∞y+∞y
38 37 ad2antll φx*y*yif+∞y+∞y
39 29 13 31 38 xrletrid φx*y*if+∞y+∞y=y
40 27 39 oveq12d φx*y*ifx−∞−∞xif+∞y+∞y=xy
41 15 40 eqtrd φx*y*x+∞−∞y=xy
42 41 imaeq2d φx*y*F-1x+∞−∞y=F-1xy
43 1 adantr φx*y*F:A
44 43 ffund φx*y*FunF
45 inpreima FunFF-1x+∞−∞y=F-1x+∞F-1−∞y
46 44 45 syl φx*y*F-1x+∞−∞y=F-1x+∞F-1−∞y
47 42 46 eqtr3d φx*y*F-1xy=F-1x+∞F-1−∞y
48 2 adantrr φx*y*F-1x+∞domvol
49 3 ralrimiva φx*F-1−∞xdomvol
50 oveq2 x=y−∞x=−∞y
51 50 imaeq2d x=yF-1−∞x=F-1−∞y
52 51 eleq1d x=yF-1−∞xdomvolF-1−∞ydomvol
53 52 rspccva x*F-1−∞xdomvoly*F-1−∞ydomvol
54 49 53 sylan φy*F-1−∞ydomvol
55 54 adantrl φx*y*F-1−∞ydomvol
56 inmbl F-1x+∞domvolF-1−∞ydomvolF-1x+∞F-1−∞ydomvol
57 48 55 56 syl2anc φx*y*F-1x+∞F-1−∞ydomvol
58 47 57 eqeltrd φx*y*F-1xydomvol
59 imaeq2 z=xyF-1z=F-1xy
60 59 eleq1d z=xyF-1zdomvolF-1xydomvol
61 58 60 syl5ibrcom φx*y*z=xyF-1zdomvol
62 61 rexlimdvva φx*y*z=xyF-1zdomvol
63 7 62 syl5bi φzran.F-1zdomvol
64 63 ralrimiv φzran.F-1zdomvol
65 ismbf F:AFMblFnzran.F-1zdomvol
66 1 65 syl φFMblFnzran.F-1zdomvol
67 64 66 mpbird φFMblFn