Metamath Proof Explorer


Theorem mbfmax

Description: The maximum of two functions is measurable. (Contributed by Mario Carneiro, 18-Jun-2014)

Ref Expression
Hypotheses mbfmax.1 φF:A
mbfmax.2 φFMblFn
mbfmax.3 φG:A
mbfmax.4 φGMblFn
mbfmax.5 H=xAifFxGxGxFx
Assertion mbfmax φHMblFn

Proof

Step Hyp Ref Expression
1 mbfmax.1 φF:A
2 mbfmax.2 φFMblFn
3 mbfmax.3 φG:A
4 mbfmax.4 φGMblFn
5 mbfmax.5 H=xAifFxGxGxFx
6 3 ffvelrnda φxAGx
7 1 ffvelrnda φxAFx
8 6 7 ifcld φxAifFxGxGxFx
9 8 5 fmptd φH:A
10 1 adantr φy*F:A
11 10 ffvelrnda φy*zAFz
12 11 rexrd φy*zAFz*
13 3 adantr φy*G:A
14 13 ffvelrnda φy*zAGz
15 14 rexrd φy*zAGz*
16 simplr φy*zAy*
17 xrmaxle Fz*Gz*y*ifFzGzGzFzyFzyGzy
18 12 15 16 17 syl3anc φy*zAifFzGzGzFzyFzyGzy
19 18 notbid φy*zA¬ifFzGzGzFzy¬FzyGzy
20 ianor ¬FzyGzy¬Fzy¬Gzy
21 19 20 bitrdi φy*zA¬ifFzGzGzFzy¬Fzy¬Gzy
22 pnfxr +∞*
23 elioo2 y*+∞*ifFzGzGzFzy+∞ifFzGzGzFzy<ifFzGzGzFzifFzGzGzFz<+∞
24 16 22 23 sylancl φy*zAifFzGzGzFzy+∞ifFzGzGzFzy<ifFzGzGzFzifFzGzGzFz<+∞
25 3anan12 ifFzGzGzFzy<ifFzGzGzFzifFzGzGzFz<+∞y<ifFzGzGzFzifFzGzGzFzifFzGzGzFz<+∞
26 24 25 bitrdi φy*zAifFzGzGzFzy+∞y<ifFzGzGzFzifFzGzGzFzifFzGzGzFz<+∞
27 fveq2 x=zFx=Fz
28 fveq2 x=zGx=Gz
29 27 28 breq12d x=zFxGxFzGz
30 29 28 27 ifbieq12d x=zifFxGxGxFx=ifFzGzGzFz
31 fvex GzV
32 fvex FzV
33 31 32 ifex ifFzGzGzFzV
34 30 5 33 fvmpt zAHz=ifFzGzGzFz
35 34 adantl φy*zAHz=ifFzGzGzFz
36 35 eleq1d φy*zAHzy+∞ifFzGzGzFzy+∞
37 14 11 ifcld φy*zAifFzGzGzFz
38 ltpnf ifFzGzGzFzifFzGzGzFz<+∞
39 37 38 jccir φy*zAifFzGzGzFzifFzGzGzFz<+∞
40 39 biantrud φy*zAy<ifFzGzGzFzy<ifFzGzGzFzifFzGzGzFzifFzGzGzFz<+∞
41 26 36 40 3bitr4d φy*zAHzy+∞y<ifFzGzGzFz
42 37 rexrd φy*zAifFzGzGzFz*
43 xrltnle y*ifFzGzGzFz*y<ifFzGzGzFz¬ifFzGzGzFzy
44 16 42 43 syl2anc φy*zAy<ifFzGzGzFz¬ifFzGzGzFzy
45 41 44 bitrd φy*zAHzy+∞¬ifFzGzGzFzy
46 elioo2 y*+∞*Fzy+∞Fzy<FzFz<+∞
47 16 22 46 sylancl φy*zAFzy+∞Fzy<FzFz<+∞
48 3anan12 Fzy<FzFz<+∞y<FzFzFz<+∞
49 47 48 bitrdi φy*zAFzy+∞y<FzFzFz<+∞
50 ltpnf FzFz<+∞
51 11 50 jccir φy*zAFzFz<+∞
52 51 biantrud φy*zAy<Fzy<FzFzFz<+∞
53 xrltnle y*Fz*y<Fz¬Fzy
54 16 12 53 syl2anc φy*zAy<Fz¬Fzy
55 49 52 54 3bitr2d φy*zAFzy+∞¬Fzy
56 elioo2 y*+∞*Gzy+∞Gzy<GzGz<+∞
57 16 22 56 sylancl φy*zAGzy+∞Gzy<GzGz<+∞
58 3anan12 Gzy<GzGz<+∞y<GzGzGz<+∞
59 57 58 bitrdi φy*zAGzy+∞y<GzGzGz<+∞
60 ltpnf GzGz<+∞
61 14 60 jccir φy*zAGzGz<+∞
62 61 biantrud φy*zAy<Gzy<GzGzGz<+∞
63 xrltnle y*Gz*y<Gz¬Gzy
64 16 15 63 syl2anc φy*zAy<Gz¬Gzy
65 59 62 64 3bitr2d φy*zAGzy+∞¬Gzy
66 55 65 orbi12d φy*zAFzy+∞Gzy+∞¬Fzy¬Gzy
67 21 45 66 3bitr4d φy*zAHzy+∞Fzy+∞Gzy+∞
68 67 pm5.32da φy*zAHzy+∞zAFzy+∞Gzy+∞
69 andi zAFzy+∞Gzy+∞zAFzy+∞zAGzy+∞
70 68 69 bitrdi φy*zAHzy+∞zAFzy+∞zAGzy+∞
71 9 ffnd φHFnA
72 71 adantr φy*HFnA
73 elpreima HFnAzH-1y+∞zAHzy+∞
74 72 73 syl φy*zH-1y+∞zAHzy+∞
75 10 ffnd φy*FFnA
76 elpreima FFnAzF-1y+∞zAFzy+∞
77 75 76 syl φy*zF-1y+∞zAFzy+∞
78 13 ffnd φy*GFnA
79 elpreima GFnAzG-1y+∞zAGzy+∞
80 78 79 syl φy*zG-1y+∞zAGzy+∞
81 77 80 orbi12d φy*zF-1y+∞zG-1y+∞zAFzy+∞zAGzy+∞
82 70 74 81 3bitr4d φy*zH-1y+∞zF-1y+∞zG-1y+∞
83 elun zF-1y+∞G-1y+∞zF-1y+∞zG-1y+∞
84 82 83 bitr4di φy*zH-1y+∞zF-1y+∞G-1y+∞
85 84 eqrdv φy*H-1y+∞=F-1y+∞G-1y+∞
86 mbfima FMblFnF:AF-1y+∞domvol
87 2 1 86 syl2anc φF-1y+∞domvol
88 mbfima GMblFnG:AG-1y+∞domvol
89 4 3 88 syl2anc φG-1y+∞domvol
90 unmbl F-1y+∞domvolG-1y+∞domvolF-1y+∞G-1y+∞domvol
91 87 89 90 syl2anc φF-1y+∞G-1y+∞domvol
92 91 adantr φy*F-1y+∞G-1y+∞domvol
93 85 92 eqeltrd φy*H-1y+∞domvol
94 xrmaxlt Fz*Gz*y*ifFzGzGzFz<yFz<yGz<y
95 12 15 16 94 syl3anc φy*zAifFzGzGzFz<yFz<yGz<y
96 mnfxr −∞*
97 elioo2 −∞*y*ifFzGzGzFz−∞yifFzGzGzFz−∞<ifFzGzGzFzifFzGzGzFz<y
98 96 16 97 sylancr φy*zAifFzGzGzFz−∞yifFzGzGzFz−∞<ifFzGzGzFzifFzGzGzFz<y
99 df-3an ifFzGzGzFz−∞<ifFzGzGzFzifFzGzGzFz<yifFzGzGzFz−∞<ifFzGzGzFzifFzGzGzFz<y
100 98 99 bitrdi φy*zAifFzGzGzFz−∞yifFzGzGzFz−∞<ifFzGzGzFzifFzGzGzFz<y
101 35 eleq1d φy*zAHz−∞yifFzGzGzFz−∞y
102 mnflt ifFzGzGzFz−∞<ifFzGzGzFz
103 37 102 jccir φy*zAifFzGzGzFz−∞<ifFzGzGzFz
104 103 biantrurd φy*zAifFzGzGzFz<yifFzGzGzFz−∞<ifFzGzGzFzifFzGzGzFz<y
105 100 101 104 3bitr4d φy*zAHz−∞yifFzGzGzFz<y
106 mnflt Fz−∞<Fz
107 11 106 jccir φy*zAFz−∞<Fz
108 elioo2 −∞*y*Fz−∞yFz−∞<FzFz<y
109 96 16 108 sylancr φy*zAFz−∞yFz−∞<FzFz<y
110 df-3an Fz−∞<FzFz<yFz−∞<FzFz<y
111 109 110 bitrdi φy*zAFz−∞yFz−∞<FzFz<y
112 107 111 mpbirand φy*zAFz−∞yFz<y
113 mnflt Gz−∞<Gz
114 14 113 jccir φy*zAGz−∞<Gz
115 elioo2 −∞*y*Gz−∞yGz−∞<GzGz<y
116 96 16 115 sylancr φy*zAGz−∞yGz−∞<GzGz<y
117 df-3an Gz−∞<GzGz<yGz−∞<GzGz<y
118 116 117 bitrdi φy*zAGz−∞yGz−∞<GzGz<y
119 114 118 mpbirand φy*zAGz−∞yGz<y
120 112 119 anbi12d φy*zAFz−∞yGz−∞yFz<yGz<y
121 95 105 120 3bitr4d φy*zAHz−∞yFz−∞yGz−∞y
122 121 pm5.32da φy*zAHz−∞yzAFz−∞yGz−∞y
123 anandi zAFz−∞yGz−∞yzAFz−∞yzAGz−∞y
124 122 123 bitrdi φy*zAHz−∞yzAFz−∞yzAGz−∞y
125 elpreima HFnAzH-1−∞yzAHz−∞y
126 72 125 syl φy*zH-1−∞yzAHz−∞y
127 elpreima FFnAzF-1−∞yzAFz−∞y
128 75 127 syl φy*zF-1−∞yzAFz−∞y
129 elpreima GFnAzG-1−∞yzAGz−∞y
130 78 129 syl φy*zG-1−∞yzAGz−∞y
131 128 130 anbi12d φy*zF-1−∞yzG-1−∞yzAFz−∞yzAGz−∞y
132 124 126 131 3bitr4d φy*zH-1−∞yzF-1−∞yzG-1−∞y
133 elin zF-1−∞yG-1−∞yzF-1−∞yzG-1−∞y
134 132 133 bitr4di φy*zH-1−∞yzF-1−∞yG-1−∞y
135 134 eqrdv φy*H-1−∞y=F-1−∞yG-1−∞y
136 mbfima FMblFnF:AF-1−∞ydomvol
137 2 1 136 syl2anc φF-1−∞ydomvol
138 mbfima GMblFnG:AG-1−∞ydomvol
139 4 3 138 syl2anc φG-1−∞ydomvol
140 inmbl F-1−∞ydomvolG-1−∞ydomvolF-1−∞yG-1−∞ydomvol
141 137 139 140 syl2anc φF-1−∞yG-1−∞ydomvol
142 141 adantr φy*F-1−∞yG-1−∞ydomvol
143 135 142 eqeltrd φy*H-1−∞ydomvol
144 9 93 143 ismbfd φHMblFn