Mathbox for Brendan Leahy < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  mblfinlem2 Structured version   Unicode version

Theorem mblfinlem2 26284
 Description: Lemma for ismblfin 26287, effectively one direction of the same fact for open sets, made necessary by Viaclovsky's slightly different defintion of outer measure. Note that unlike the main theorem, this holds for sets of infinite measure. (Contributed by Brendan Leahy, 21-Feb-2018.) (Revised by Brendan Leahy, 13-Jul-2018.)
Assertion
Ref Expression
mblfinlem2
Distinct variable groups:   ,   ,

Proof of Theorem mblfinlem2
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 retop 18833 . . . 4
2 0cld 17140 . . . 4
31, 2ax-mp 5 . . 3
4 simpl3 963 . . . . 5
5 fveq2 5763 . . . . . 6
65adantl 454 . . . . 5
74, 6breqtrd 4267 . . . 4
8 0ss 3644 . . . 4
97, 8jctil 525 . . 3
10 sseq1 3358 . . . . 5
11 fveq2 5763 . . . . . 6
1211breq2d 4255 . . . . 5
1310, 12anbi12d 693 . . . 4
1413rspcev 3061 . . 3
153, 9, 14sylancr 646 . 2
16 mblfinlem1 26283 . . . 4
18 simpl3 963 . . . . . . . . 9
19 f1ofo 5716 . . . . . . . . . . . . . 14
20 rnco2 5412 . . . . . . . . . . . . . . . 16
21 forn 5691 . . . . . . . . . . . . . . . . 17
2221imaeq2d 5238 . . . . . . . . . . . . . . . 16
2320, 22syl5eq 2487 . . . . . . . . . . . . . . 15
2423unieqd 4055 . . . . . . . . . . . . . 14
2519, 24syl 16 . . . . . . . . . . . . 13
2625adantl 454 . . . . . . . . . . . 12
27 oveq1 6124 . . . . . . . . . . . . . . . 16
28 oveq1 6124 . . . . . . . . . . . . . . . . 17
2928oveq1d 6132 . . . . . . . . . . . . . . . 16
3027, 29opeq12d 4021 . . . . . . . . . . . . . . 15
31 oveq2 6125 . . . . . . . . . . . . . . . . 17
3231oveq2d 6133 . . . . . . . . . . . . . . . 16
3331oveq2d 6133 . . . . . . . . . . . . . . . 16
3432, 33opeq12d 4021 . . . . . . . . . . . . . . 15
3530, 34cbvmpt2v 6188 . . . . . . . . . . . . . 14
36 fveq2 5763 . . . . . . . . . . . . . . . . . 18
3736sseq1d 3364 . . . . . . . . . . . . . . . . 17
38 eqeq1 2449 . . . . . . . . . . . . . . . . 17
3937, 38imbi12d 313 . . . . . . . . . . . . . . . 16
4039ralbidv 2732 . . . . . . . . . . . . . . 15
4140cbvrabv 2964 . . . . . . . . . . . . . 14
42 ssrab2 3417 . . . . . . . . . . . . . . 15
4342a1i 11 . . . . . . . . . . . . . 14
4435, 41, 43dyadmbllem 19529 . . . . . . . . . . . . 13
4544adantr 453 . . . . . . . . . . . 12
46 opnmbllem0 26282 . . . . . . . . . . . . . 14
47463ad2ant1 979 . . . . . . . . . . . . 13
4847adantr 453 . . . . . . . . . . . 12
4926, 45, 483eqtr2d 2481 . . . . . . . . . . 11
5049fveq2d 5767 . . . . . . . . . 10
51 f1of 5709 . . . . . . . . . . . . 13
52 ssrab2 3417 . . . . . . . . . . . . . 14
5335dyadf 19521 . . . . . . . . . . . . . . . 16
54 frn 5632 . . . . . . . . . . . . . . . 16
5553, 54ax-mp 5 . . . . . . . . . . . . . . 15
5642, 55sstri 3346 . . . . . . . . . . . . . 14
5752, 56sstri 3346 . . . . . . . . . . . . 13
58 fss 5634 . . . . . . . . . . . . 13
5951, 57, 58sylancl 645 . . . . . . . . . . . 12
6052, 42sstri 3346 . . . . . . . . . . . . . . . . . . . 20
61 ffvelrn 5904 . . . . . . . . . . . . . . . . . . . 20
6260, 61sseldi 3335 . . . . . . . . . . . . . . . . . . 19
6362adantrr 699 . . . . . . . . . . . . . . . . . 18
64 ffvelrn 5904 . . . . . . . . . . . . . . . . . . . 20
6560, 64sseldi 3335 . . . . . . . . . . . . . . . . . . 19
6665adantrl 698 . . . . . . . . . . . . . . . . . 18
6735dyaddisj 19526 . . . . . . . . . . . . . . . . . 18
6863, 66, 67syl2anc 644 . . . . . . . . . . . . . . . . 17
6951, 68sylan 459 . . . . . . . . . . . . . . . 16
70 df-3or 938 . . . . . . . . . . . . . . . 16
7169, 70sylib 190 . . . . . . . . . . . . . . 15
72 elrabi 3099 . . . . . . . . . . . . . . . . . . . . . 22
73 fveq2 5763 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
7473sseq1d 3364 . . . . . . . . . . . . . . . . . . . . . . . . . 26
75 eqeq1 2449 . . . . . . . . . . . . . . . . . . . . . . . . . 26
7674, 75imbi12d 313 . . . . . . . . . . . . . . . . . . . . . . . . 25
7776ralbidv 2732 . . . . . . . . . . . . . . . . . . . . . . . 24
7877elrab 3101 . . . . . . . . . . . . . . . . . . . . . . 23
7978simprbi 452 . . . . . . . . . . . . . . . . . . . . . 22
80 fveq2 5763 . . . . . . . . . . . . . . . . . . . . . . . . 25
8180sseq2d 3365 . . . . . . . . . . . . . . . . . . . . . . . 24
82 eqeq2 2452 . . . . . . . . . . . . . . . . . . . . . . . 24
8381, 82imbi12d 313 . . . . . . . . . . . . . . . . . . . . . . 23
8483rspcva 3059 . . . . . . . . . . . . . . . . . . . . . 22
8572, 79, 84syl2anr 466 . . . . . . . . . . . . . . . . . . . . 21
86 elrabi 3099 . . . . . . . . . . . . . . . . . . . . . . 23
87 fveq2 5763 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
8887sseq1d 3364 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
89 eqeq1 2449 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
9088, 89imbi12d 313 . . . . . . . . . . . . . . . . . . . . . . . . . 26
9190ralbidv 2732 . . . . . . . . . . . . . . . . . . . . . . . . 25
9291elrab 3101 . . . . . . . . . . . . . . . . . . . . . . . 24
9392simprbi 452 . . . . . . . . . . . . . . . . . . . . . . 23
94 fveq2 5763 . . . . . . . . . . . . . . . . . . . . . . . . . 26
9594sseq2d 3365 . . . . . . . . . . . . . . . . . . . . . . . . 25
96 eqeq2 2452 . . . . . . . . . . . . . . . . . . . . . . . . 25
9795, 96imbi12d 313 . . . . . . . . . . . . . . . . . . . . . . . 24
9897rspcva 3059 . . . . . . . . . . . . . . . . . . . . . . 23
9986, 93, 98syl2an 465 . . . . . . . . . . . . . . . . . . . . . 22
100 eqcom 2445 . . . . . . . . . . . . . . . . . . . . . 22
10199, 100syl6ib 219 . . . . . . . . . . . . . . . . . . . . 21
10285, 101jaod 371 . . . . . . . . . . . . . . . . . . . 20
10361, 64, 102syl2an 465 . . . . . . . . . . . . . . . . . . 19
104103anandis 805 . . . . . . . . . . . . . . . . . 18
10551, 104sylan 459 . . . . . . . . . . . . . . . . 17
106 f1of1 5708 . . . . . . . . . . . . . . . . . 18
107 f1veqaeq 6041 . . . . . . . . . . . . . . . . . 18
108106, 107sylan 459 . . . . . . . . . . . . . . . . 17
109105, 108syld 43 . . . . . . . . . . . . . . . 16
110109orim1d 814 . . . . . . . . . . . . . . 15
11171, 110mpd 15 . . . . . . . . . . . . . 14
112111ralrimivva 2805 . . . . . . . . . . . . 13
113 eqeq1 2449 . . . . . . . . . . . . . . . . 17
114 fveq2 5763 . . . . . . . . . . . . . . . . . . . 20
115114fveq2d 5767 . . . . . . . . . . . . . . . . . . 19
116115ineq1d 3530 . . . . . . . . . . . . . . . . . 18
117116eqeq1d 2451 . . . . . . . . . . . . . . . . 17
118113, 117orbi12d 692 . . . . . . . . . . . . . . . 16
119118ralbidv 2732 . . . . . . . . . . . . . . 15
120119cbvralv 2941 . . . . . . . . . . . . . 14
121 eqeq2 2452 . . . . . . . . . . . . . . . . 17
122 fveq2 5763 . . . . . . . . . . . . . . . . . . . 20
123122fveq2d 5767 . . . . . . . . . . . . . . . . . . 19
124123ineq2d 3531 . . . . . . . . . . . . . . . . . 18
125124eqeq1d 2451 . . . . . . . . . . . . . . . . 17
126121, 125orbi12d 692 . . . . . . . . . . . . . . . 16
127126cbvralv 2941 . . . . . . . . . . . . . . 15
128127ralbii 2736 . . . . . . . . . . . . . 14
129123disjor 4227 . . . . . . . . . . . . . 14 Disj
130120, 128, 1293bitr4ri 271 . . . . . . . . . . . . 13 Disj
131112, 130sylibr 205 . . . . . . . . . . . 12 Disj
132 eqid 2443 . . . . . . . . . . . 12
13359, 131, 132uniiccvol 19510 . . . . . . . . . . 11
134133adantl 454 . . . . . . . . . 10
13550, 134eqtr3d 2477 . . . . . . . . 9
13618, 135breqtrd 4267 . . . . . . . 8
137 absf 12179 . . . . . . . . . . . 12
138 subf 9345 . . . . . . . . . . . 12
139 fco 5635 . . . . . . . . . . . 12
140137, 138, 139mp2an 655 . . . . . . . . . . 11
141 zre 10324 . . . . . . . . . . . . . . . . . . 19
142 2re 10107 . . . . . . . . . . . . . . . . . . . . 21
143 reexpcl 11436 . . . . . . . . . . . . . . . . . . . . 21
144142, 143mpan 653 . . . . . . . . . . . . . . . . . . . 20
145 nn0z 10342 . . . . . . . . . . . . . . . . . . . . 21
146 2cn 10108 . . . . . . . . . . . . . . . . . . . . . 22
147 2ne0 10121 . . . . . . . . . . . . . . . . . . . . . 22
148 expne0i 11450 . . . . . . . . . . . . . . . . . . . . . 22
149146, 147, 148mp3an12 1270 . . . . . . . . . . . . . . . . . . . . 21
150145, 149syl 16 . . . . . . . . . . . . . . . . . . . 20
151144, 150jca 520 . . . . . . . . . . . . . . . . . . 19
152 redivcl 9771 . . . . . . . . . . . . . . . . . . . . 21
153 peano2re 9277 . . . . . . . . . . . . . . . . . . . . . 22
154 redivcl 9771 . . . . . . . . . . . . . . . . . . . . . 22
155153, 154syl3an1 1218 . . . . . . . . . . . . . . . . . . . . 21
156 opelxpi 4945 . . . . . . . . . . . . . . . . . . . . 21
157152, 155, 156syl2anc 644 . . . . . . . . . . . . . . . . . . . 20
1581573expb 1155 . . . . . . . . . . . . . . . . . . 19
159141, 151, 158syl2an 465 . . . . . . . . . . . . . . . . . 18
160159rgen2 2809 . . . . . . . . . . . . . . . . 17
161 eqid 2443 . . . . . . . . . . . . . . . . . 18