Metamath Proof Explorer


Theorem mbfsup

Description: The supremum of a sequence of measurable, real-valued functions is measurable. Note that in this and related theorems, B ( n , x ) is a function of both n and x , since it is an n -indexed sequence of functions on x . (Contributed by Mario Carneiro, 14-Aug-2014) (Revised by Mario Carneiro, 7-Sep-2014)

Ref Expression
Hypotheses mbfsup.1 Z = M
mbfsup.2 G = x A sup ran n Z B <
mbfsup.3 φ M
mbfsup.4 φ n Z x A B MblFn
mbfsup.5 φ n Z x A B
mbfsup.6 φ x A y n Z B y
Assertion mbfsup φ G MblFn

Proof

Step Hyp Ref Expression
1 mbfsup.1 Z = M
2 mbfsup.2 G = x A sup ran n Z B <
3 mbfsup.3 φ M
4 mbfsup.4 φ n Z x A B MblFn
5 mbfsup.5 φ n Z x A B
6 mbfsup.6 φ x A y n Z B y
7 5 anassrs φ n Z x A B
8 7 an32s φ x A n Z B
9 8 fmpttd φ x A n Z B : Z
10 9 frnd φ x A ran n Z B
11 uzid M M M
12 3 11 syl φ M M
13 12 1 eleqtrrdi φ M Z
14 13 adantr φ x A M Z
15 eqid n Z B = n Z B
16 15 8 dmmptd φ x A dom n Z B = Z
17 14 16 eleqtrrd φ x A M dom n Z B
18 17 ne0d φ x A dom n Z B
19 dm0rn0 dom n Z B = ran n Z B =
20 19 necon3bii dom n Z B ran n Z B
21 18 20 sylib φ x A ran n Z B
22 9 ffnd φ x A n Z B Fn Z
23 breq1 z = n Z B m z y n Z B m y
24 23 ralrn n Z B Fn Z z ran n Z B z y m Z n Z B m y
25 22 24 syl φ x A z ran n Z B z y m Z n Z B m y
26 nffvmpt1 _ n n Z B m
27 nfcv _ n
28 nfcv _ n y
29 26 27 28 nfbr n n Z B m y
30 nfv m n Z B n y
31 fveq2 m = n n Z B m = n Z B n
32 31 breq1d m = n n Z B m y n Z B n y
33 29 30 32 cbvralw m Z n Z B m y n Z n Z B n y
34 simpr φ x A n Z n Z
35 15 fvmpt2 n Z B n Z B n = B
36 34 8 35 syl2anc φ x A n Z n Z B n = B
37 36 breq1d φ x A n Z n Z B n y B y
38 37 ralbidva φ x A n Z n Z B n y n Z B y
39 33 38 syl5bb φ x A m Z n Z B m y n Z B y
40 25 39 bitrd φ x A z ran n Z B z y n Z B y
41 40 rexbidv φ x A y z ran n Z B z y y n Z B y
42 6 41 mpbird φ x A y z ran n Z B z y
43 10 21 42 suprcld φ x A sup ran n Z B <
44 43 2 fmptd φ G : A
45 simpr φ t x A x A
46 ltso < Or
47 46 supex sup ran n Z B < V
48 2 fvmpt2 x A sup ran n Z B < V G x = sup ran n Z B <
49 45 47 48 sylancl φ t x A G x = sup ran n Z B <
50 49 breq2d φ t x A t < G x t < sup ran n Z B <
51 10 21 42 3jca φ x A ran n Z B ran n Z B y z ran n Z B z y
52 51 adantlr φ t x A ran n Z B ran n Z B y z ran n Z B z y
53 simplr φ t x A t
54 suprlub ran n Z B ran n Z B y z ran n Z B z y t t < sup ran n Z B < z ran n Z B t < z
55 52 53 54 syl2anc φ t x A t < sup ran n Z B < z ran n Z B t < z
56 22 adantlr φ t x A n Z B Fn Z
57 breq2 z = n Z B m t < z t < n Z B m
58 57 rexrn n Z B Fn Z z ran n Z B t < z m Z t < n Z B m
59 56 58 syl φ t x A z ran n Z B t < z m Z t < n Z B m
60 nfcv _ n t
61 nfcv _ n <
62 60 61 26 nfbr n t < n Z B m
63 nfv m t < n Z B n
64 31 breq2d m = n t < n Z B m t < n Z B n
65 62 63 64 cbvrexw m Z t < n Z B m n Z t < n Z B n
66 15 fvmpt2i n Z n Z B n = I B
67 eqid x A B = x A B
68 67 fvmpt2i x A x A B x = I B
69 68 adantl φ x A x A B x = I B
70 69 eqcomd φ x A I B = x A B x
71 66 70 sylan9eqr φ x A n Z n Z B n = x A B x
72 71 breq2d φ x A n Z t < n Z B n t < x A B x
73 72 rexbidva φ x A n Z t < n Z B n n Z t < x A B x
74 73 adantlr φ t x A n Z t < n Z B n n Z t < x A B x
75 65 74 syl5bb φ t x A m Z t < n Z B m n Z t < x A B x
76 59 75 bitrd φ t x A z ran n Z B t < z n Z t < x A B x
77 50 55 76 3bitrd φ t x A t < G x n Z t < x A B x
78 77 ralrimiva φ t x A t < G x n Z t < x A B x
79 nfv z t < G x n Z t < x A B x
80 nfcv _ x t
81 nfcv _ x <
82 nfmpt1 _ x x A sup ran n Z B <
83 2 82 nfcxfr _ x G
84 nfcv _ x z
85 83 84 nffv _ x G z
86 80 81 85 nfbr x t < G z
87 nfcv _ x Z
88 nffvmpt1 _ x x A B z
89 80 81 88 nfbr x t < x A B z
90 87 89 nfrex x n Z t < x A B z
91 86 90 nfbi x t < G z n Z t < x A B z
92 fveq2 x = z G x = G z
93 92 breq2d x = z t < G x t < G z
94 fveq2 x = z x A B x = x A B z
95 94 breq2d x = z t < x A B x t < x A B z
96 95 rexbidv x = z n Z t < x A B x n Z t < x A B z
97 93 96 bibi12d x = z t < G x n Z t < x A B x t < G z n Z t < x A B z
98 79 91 97 cbvralw x A t < G x n Z t < x A B x z A t < G z n Z t < x A B z
99 78 98 sylib φ t z A t < G z n Z t < x A B z
100 99 r19.21bi φ t z A t < G z n Z t < x A B z
101 44 adantr φ t G : A
102 101 ffvelrnda φ t z A G z
103 rexr t t *
104 103 ad2antlr φ t z A t *
105 elioopnf t * G z t +∞ G z t < G z
106 104 105 syl φ t z A G z t +∞ G z t < G z
107 102 106 mpbirand φ t z A G z t +∞ t < G z
108 104 adantr φ t z A n Z t *
109 elioopnf t * x A B z t +∞ x A B z t < x A B z
110 108 109 syl φ t z A n Z x A B z t +∞ x A B z t < x A B z
111 7 fmpttd φ n Z x A B : A
112 111 ffvelrnda φ n Z z A x A B z
113 112 biantrurd φ n Z z A t < x A B z x A B z t < x A B z
114 113 an32s φ z A n Z t < x A B z x A B z t < x A B z
115 114 adantllr φ t z A n Z t < x A B z x A B z t < x A B z
116 110 115 bitr4d φ t z A n Z x A B z t +∞ t < x A B z
117 116 rexbidva φ t z A n Z x A B z t +∞ n Z t < x A B z
118 100 107 117 3bitr4d φ t z A G z t +∞ n Z x A B z t +∞
119 118 pm5.32da φ t z A G z t +∞ z A n Z x A B z t +∞
120 44 ffnd φ G Fn A
121 120 adantr φ t G Fn A
122 elpreima G Fn A z G -1 t +∞ z A G z t +∞
123 121 122 syl φ t z G -1 t +∞ z A G z t +∞
124 eliun z n Z x A B -1 t +∞ n Z z x A B -1 t +∞
125 111 ffnd φ n Z x A B Fn A
126 elpreima x A B Fn A z x A B -1 t +∞ z A x A B z t +∞
127 125 126 syl φ n Z z x A B -1 t +∞ z A x A B z t +∞
128 127 rexbidva φ n Z z x A B -1 t +∞ n Z z A x A B z t +∞
129 128 adantr φ t n Z z x A B -1 t +∞ n Z z A x A B z t +∞
130 r19.42v n Z z A x A B z t +∞ z A n Z x A B z t +∞
131 129 130 bitrdi φ t n Z z x A B -1 t +∞ z A n Z x A B z t +∞
132 124 131 syl5bb φ t z n Z x A B -1 t +∞ z A n Z x A B z t +∞
133 119 123 132 3bitr4d φ t z G -1 t +∞ z n Z x A B -1 t +∞
134 133 eqrdv φ t G -1 t +∞ = n Z x A B -1 t +∞
135 zex V
136 uzssz M
137 ssdomg V M M
138 135 136 137 mp2 M
139 1 138 eqbrtri Z
140 znnen
141 domentr Z Z
142 139 140 141 mp2an Z
143 mbfima x A B MblFn x A B : A x A B -1 t +∞ dom vol
144 4 111 143 syl2anc φ n Z x A B -1 t +∞ dom vol
145 144 ralrimiva φ n Z x A B -1 t +∞ dom vol
146 145 adantr φ t n Z x A B -1 t +∞ dom vol
147 iunmbl2 Z n Z x A B -1 t +∞ dom vol n Z x A B -1 t +∞ dom vol
148 142 146 147 sylancr φ t n Z x A B -1 t +∞ dom vol
149 134 148 eqeltrd φ t G -1 t +∞ dom vol
150 44 149 ismbf3d φ G MblFn