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 φ F MblFn
mbfmax.3 φ G : A
mbfmax.4 φ G MblFn
mbfmax.5 H = x A if F x G x G x F x
Assertion mbfmax φ H MblFn

Proof

Step Hyp Ref Expression
1 mbfmax.1 φ F : A
2 mbfmax.2 φ F MblFn
3 mbfmax.3 φ G : A
4 mbfmax.4 φ G MblFn
5 mbfmax.5 H = x A if F x G x G x F x
6 3 ffvelrnda φ x A G x
7 1 ffvelrnda φ x A F x
8 6 7 ifcld φ x A if F x G x G x F x
9 8 5 fmptd φ H : A
10 1 adantr φ y * F : A
11 10 ffvelrnda φ y * z A F z
12 11 rexrd φ y * z A F z *
13 3 adantr φ y * G : A
14 13 ffvelrnda φ y * z A G z
15 14 rexrd φ y * z A G z *
16 simplr φ y * z A y *
17 xrmaxle F z * G z * y * if F z G z G z F z y F z y G z y
18 12 15 16 17 syl3anc φ y * z A if F z G z G z F z y F z y G z y
19 18 notbid φ y * z A ¬ if F z G z G z F z y ¬ F z y G z y
20 ianor ¬ F z y G z y ¬ F z y ¬ G z y
21 19 20 bitrdi φ y * z A ¬ if F z G z G z F z y ¬ F z y ¬ G z y
22 pnfxr +∞ *
23 elioo2 y * +∞ * if F z G z G z F z y +∞ if F z G z G z F z y < if F z G z G z F z if F z G z G z F z < +∞
24 16 22 23 sylancl φ y * z A if F z G z G z F z y +∞ if F z G z G z F z y < if F z G z G z F z if F z G z G z F z < +∞
25 3anan12 if F z G z G z F z y < if F z G z G z F z if F z G z G z F z < +∞ y < if F z G z G z F z if F z G z G z F z if F z G z G z F z < +∞
26 24 25 bitrdi φ y * z A if F z G z G z F z y +∞ y < if F z G z G z F z if F z G z G z F z if F z G z G z F z < +∞
27 fveq2 x = z F x = F z
28 fveq2 x = z G x = G z
29 27 28 breq12d x = z F x G x F z G z
30 29 28 27 ifbieq12d x = z if F x G x G x F x = if F z G z G z F z
31 fvex G z V
32 fvex F z V
33 31 32 ifex if F z G z G z F z V
34 30 5 33 fvmpt z A H z = if F z G z G z F z
35 34 adantl φ y * z A H z = if F z G z G z F z
36 35 eleq1d φ y * z A H z y +∞ if F z G z G z F z y +∞
37 14 11 ifcld φ y * z A if F z G z G z F z
38 ltpnf if F z G z G z F z if F z G z G z F z < +∞
39 37 38 jccir φ y * z A if F z G z G z F z if F z G z G z F z < +∞
40 39 biantrud φ y * z A y < if F z G z G z F z y < if F z G z G z F z if F z G z G z F z if F z G z G z F z < +∞
41 26 36 40 3bitr4d φ y * z A H z y +∞ y < if F z G z G z F z
42 37 rexrd φ y * z A if F z G z G z F z *
43 xrltnle y * if F z G z G z F z * y < if F z G z G z F z ¬ if F z G z G z F z y
44 16 42 43 syl2anc φ y * z A y < if F z G z G z F z ¬ if F z G z G z F z y
45 41 44 bitrd φ y * z A H z y +∞ ¬ if F z G z G z F z y
46 elioo2 y * +∞ * F z y +∞ F z y < F z F z < +∞
47 16 22 46 sylancl φ y * z A F z y +∞ F z y < F z F z < +∞
48 3anan12 F z y < F z F z < +∞ y < F z F z F z < +∞
49 47 48 bitrdi φ y * z A F z y +∞ y < F z F z F z < +∞
50 ltpnf F z F z < +∞
51 11 50 jccir φ y * z A F z F z < +∞
52 51 biantrud φ y * z A y < F z y < F z F z F z < +∞
53 xrltnle y * F z * y < F z ¬ F z y
54 16 12 53 syl2anc φ y * z A y < F z ¬ F z y
55 49 52 54 3bitr2d φ y * z A F z y +∞ ¬ F z y
56 elioo2 y * +∞ * G z y +∞ G z y < G z G z < +∞
57 16 22 56 sylancl φ y * z A G z y +∞ G z y < G z G z < +∞
58 3anan12 G z y < G z G z < +∞ y < G z G z G z < +∞
59 57 58 bitrdi φ y * z A G z y +∞ y < G z G z G z < +∞
60 ltpnf G z G z < +∞
61 14 60 jccir φ y * z A G z G z < +∞
62 61 biantrud φ y * z A y < G z y < G z G z G z < +∞
63 xrltnle y * G z * y < G z ¬ G z y
64 16 15 63 syl2anc φ y * z A y < G z ¬ G z y
65 59 62 64 3bitr2d φ y * z A G z y +∞ ¬ G z y
66 55 65 orbi12d φ y * z A F z y +∞ G z y +∞ ¬ F z y ¬ G z y
67 21 45 66 3bitr4d φ y * z A H z y +∞ F z y +∞ G z y +∞
68 67 pm5.32da φ y * z A H z y +∞ z A F z y +∞ G z y +∞
69 andi z A F z y +∞ G z y +∞ z A F z y +∞ z A G z y +∞
70 68 69 bitrdi φ y * z A H z y +∞ z A F z y +∞ z A G z y +∞
71 9 ffnd φ H Fn A
72 71 adantr φ y * H Fn A
73 elpreima H Fn A z H -1 y +∞ z A H z y +∞
74 72 73 syl φ y * z H -1 y +∞ z A H z y +∞
75 10 ffnd φ y * F Fn A
76 elpreima F Fn A z F -1 y +∞ z A F z y +∞
77 75 76 syl φ y * z F -1 y +∞ z A F z y +∞
78 13 ffnd φ y * G Fn A
79 elpreima G Fn A z G -1 y +∞ z A G z y +∞
80 78 79 syl φ y * z G -1 y +∞ z A G z y +∞
81 77 80 orbi12d φ y * z F -1 y +∞ z G -1 y +∞ z A F z y +∞ z A G z y +∞
82 70 74 81 3bitr4d φ y * z H -1 y +∞ z F -1 y +∞ z G -1 y +∞
83 elun z F -1 y +∞ G -1 y +∞ z F -1 y +∞ z G -1 y +∞
84 82 83 bitr4di φ y * z H -1 y +∞ z F -1 y +∞ G -1 y +∞
85 84 eqrdv φ y * H -1 y +∞ = F -1 y +∞ G -1 y +∞
86 mbfima F MblFn F : A F -1 y +∞ dom vol
87 2 1 86 syl2anc φ F -1 y +∞ dom vol
88 mbfima G MblFn G : A G -1 y +∞ dom vol
89 4 3 88 syl2anc φ G -1 y +∞ dom vol
90 unmbl F -1 y +∞ dom vol G -1 y +∞ dom vol F -1 y +∞ G -1 y +∞ dom vol
91 87 89 90 syl2anc φ F -1 y +∞ G -1 y +∞ dom vol
92 91 adantr φ y * F -1 y +∞ G -1 y +∞ dom vol
93 85 92 eqeltrd φ y * H -1 y +∞ dom vol
94 xrmaxlt F z * G z * y * if F z G z G z F z < y F z < y G z < y
95 12 15 16 94 syl3anc φ y * z A if F z G z G z F z < y F z < y G z < y
96 mnfxr −∞ *
97 elioo2 −∞ * y * if F z G z G z F z −∞ y if F z G z G z F z −∞ < if F z G z G z F z if F z G z G z F z < y
98 96 16 97 sylancr φ y * z A if F z G z G z F z −∞ y if F z G z G z F z −∞ < if F z G z G z F z if F z G z G z F z < y
99 df-3an if F z G z G z F z −∞ < if F z G z G z F z if F z G z G z F z < y if F z G z G z F z −∞ < if F z G z G z F z if F z G z G z F z < y
100 98 99 bitrdi φ y * z A if F z G z G z F z −∞ y if F z G z G z F z −∞ < if F z G z G z F z if F z G z G z F z < y
101 35 eleq1d φ y * z A H z −∞ y if F z G z G z F z −∞ y
102 mnflt if F z G z G z F z −∞ < if F z G z G z F z
103 37 102 jccir φ y * z A if F z G z G z F z −∞ < if F z G z G z F z
104 103 biantrurd φ y * z A if F z G z G z F z < y if F z G z G z F z −∞ < if F z G z G z F z if F z G z G z F z < y
105 100 101 104 3bitr4d φ y * z A H z −∞ y if F z G z G z F z < y
106 mnflt F z −∞ < F z
107 11 106 jccir φ y * z A F z −∞ < F z
108 elioo2 −∞ * y * F z −∞ y F z −∞ < F z F z < y
109 96 16 108 sylancr φ y * z A F z −∞ y F z −∞ < F z F z < y
110 df-3an F z −∞ < F z F z < y F z −∞ < F z F z < y
111 109 110 bitrdi φ y * z A F z −∞ y F z −∞ < F z F z < y
112 107 111 mpbirand φ y * z A F z −∞ y F z < y
113 mnflt G z −∞ < G z
114 14 113 jccir φ y * z A G z −∞ < G z
115 elioo2 −∞ * y * G z −∞ y G z −∞ < G z G z < y
116 96 16 115 sylancr φ y * z A G z −∞ y G z −∞ < G z G z < y
117 df-3an G z −∞ < G z G z < y G z −∞ < G z G z < y
118 116 117 bitrdi φ y * z A G z −∞ y G z −∞ < G z G z < y
119 114 118 mpbirand φ y * z A G z −∞ y G z < y
120 112 119 anbi12d φ y * z A F z −∞ y G z −∞ y F z < y G z < y
121 95 105 120 3bitr4d φ y * z A H z −∞ y F z −∞ y G z −∞ y
122 121 pm5.32da φ y * z A H z −∞ y z A F z −∞ y G z −∞ y
123 anandi z A F z −∞ y G z −∞ y z A F z −∞ y z A G z −∞ y
124 122 123 bitrdi φ y * z A H z −∞ y z A F z −∞ y z A G z −∞ y
125 elpreima H Fn A z H -1 −∞ y z A H z −∞ y
126 72 125 syl φ y * z H -1 −∞ y z A H z −∞ y
127 elpreima F Fn A z F -1 −∞ y z A F z −∞ y
128 75 127 syl φ y * z F -1 −∞ y z A F z −∞ y
129 elpreima G Fn A z G -1 −∞ y z A G z −∞ y
130 78 129 syl φ y * z G -1 −∞ y z A G z −∞ y
131 128 130 anbi12d φ y * z F -1 −∞ y z G -1 −∞ y z A F z −∞ y z A G z −∞ y
132 124 126 131 3bitr4d φ y * z H -1 −∞ y z F -1 −∞ y z G -1 −∞ y
133 elin z F -1 −∞ y G -1 −∞ y z F -1 −∞ y z G -1 −∞ y
134 132 133 bitr4di φ y * z H -1 −∞ y z F -1 −∞ y G -1 −∞ y
135 134 eqrdv φ y * H -1 −∞ y = F -1 −∞ y G -1 −∞ y
136 mbfima F MblFn F : A F -1 −∞ y dom vol
137 2 1 136 syl2anc φ F -1 −∞ y dom vol
138 mbfima G MblFn G : A G -1 −∞ y dom vol
139 4 3 138 syl2anc φ G -1 −∞ y dom vol
140 inmbl F -1 −∞ y dom vol G -1 −∞ y dom vol F -1 −∞ y G -1 −∞ y dom vol
141 137 139 140 syl2anc φ F -1 −∞ y G -1 −∞ y dom vol
142 141 adantr φ y * F -1 −∞ y G -1 −∞ y dom vol
143 135 142 eqeltrd φ y * H -1 −∞ y dom vol
144 9 93 143 ismbfd φ H MblFn