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

Theorem mblfinlem 26143
 Description: Lemma for ismblfin 26146, 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.)
Assertion
Ref Expression
mblfinlem
Distinct variable groups:   ,   ,

Proof of Theorem mblfinlem
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 retop 18748 . . . 4
2 0cld 17057 . . . 4
31, 2ax-mp 8 . . 3
4 simpl3 962 . . . . 5
5 fveq2 5687 . . . . . 6
65adantl 453 . . . . 5
74, 6breqtrd 4196 . . . 4
8 0ss 3616 . . . 4
97, 8jctil 524 . . 3
10 sseq1 3329 . . . . 5
11 fveq2 5687 . . . . . 6
1211breq2d 4184 . . . . 5
1310, 12anbi12d 692 . . . 4
1413rspcev 3012 . . 3
153, 9, 14sylancr 645 . 2
16 peano2re 9195 . . . . . . . . . . . . . . . 16
17 ltp1 9804 . . . . . . . . . . . . . . . 16
18 breq2 4176 . . . . . . . . . . . . . . . . 17
1918rspcev 3012 . . . . . . . . . . . . . . . 16
2016, 17, 19syl2anc 643 . . . . . . . . . . . . . . 15
2120rgen 2731 . . . . . . . . . . . . . 14
22 ltnle 9111 . . . . . . . . . . . . . . . . . 18
2322rexbidva 2683 . . . . . . . . . . . . . . . . 17
24 rexnal 2677 . . . . . . . . . . . . . . . . 17
2523, 24syl6bb 253 . . . . . . . . . . . . . . . 16
2625ralbiia 2698 . . . . . . . . . . . . . . 15
27 ralnex 2676 . . . . . . . . . . . . . . 15
2826, 27bitri 241 . . . . . . . . . . . . . 14
2921, 28mpbi 200 . . . . . . . . . . . . 13
30 raleq 2864 . . . . . . . . . . . . . 14
3130rexbidv 2687 . . . . . . . . . . . . 13
3229, 31mtbiri 295 . . . . . . . . . . . 12
33 ssrab2 3388 . . . . . . . . . . . . . . . . 17
34 ssrab2 3388 . . . . . . . . . . . . . . . . . 18
35 zre 10242 . . . . . . . . . . . . . . . . . . . . . 22
36 2re 10025 . . . . . . . . . . . . . . . . . . . . . . . 24
37 reexpcl 11353 . . . . . . . . . . . . . . . . . . . . . . . 24
3836, 37mpan 652 . . . . . . . . . . . . . . . . . . . . . . 23
39 nn0z 10260 . . . . . . . . . . . . . . . . . . . . . . . 24
40 2cn 10026 . . . . . . . . . . . . . . . . . . . . . . . . 25
41 2ne0 10039 . . . . . . . . . . . . . . . . . . . . . . . . 25
42 expne0i 11367 . . . . . . . . . . . . . . . . . . . . . . . . 25
4340, 41, 42mp3an12 1269 . . . . . . . . . . . . . . . . . . . . . . . 24
4439, 43syl 16 . . . . . . . . . . . . . . . . . . . . . . 23
4538, 44jca 519 . . . . . . . . . . . . . . . . . . . . . 22
46 redivcl 9689 . . . . . . . . . . . . . . . . . . . . . . . 24
47 peano2re 9195 . . . . . . . . . . . . . . . . . . . . . . . . 25
48 redivcl 9689 . . . . . . . . . . . . . . . . . . . . . . . . 25
4947, 48syl3an1 1217 . . . . . . . . . . . . . . . . . . . . . . . 24
50 opelxpi 4869 . . . . . . . . . . . . . . . . . . . . . . . 24
5146, 49, 50syl2anc 643 . . . . . . . . . . . . . . . . . . . . . . 23
52513expb 1154 . . . . . . . . . . . . . . . . . . . . . 22
5335, 45, 52syl2an 464 . . . . . . . . . . . . . . . . . . . . 21
5453rgen2 2762 . . . . . . . . . . . . . . . . . . . 20
55 eqid 2404 . . . . . . . . . . . . . . . . . . . . 21
5655fmpt2 6377 . . . . . . . . . . . . . . . . . . . 20
5754, 56mpbi 200 . . . . . . . . . . . . . . . . . . 19
58 frn 5556 . . . . . . . . . . . . . . . . . . 19
5957, 58ax-mp 8 . . . . . . . . . . . . . . . . . 18
6034, 59sstri 3317 . . . . . . . . . . . . . . . . 17
6133, 60sstri 3317 . . . . . . . . . . . . . . . 16
62 rnss 5057 . . . . . . . . . . . . . . . . 17
63 rnxpid 5261 . . . . . . . . . . . . . . . . 17
6462, 63syl6sseq 3354 . . . . . . . . . . . . . . . 16
6561, 64ax-mp 8 . . . . . . . . . . . . . . 15
66 rnfi 7350 . . . . . . . . . . . . . . 15
67 fimaxre2 9912 . . . . . . . . . . . . . . 15
6865, 66, 67sylancr 645 . . . . . . . . . . . . . 14
6968adantl 453 . . . . . . . . . . . . 13
70 eluni2 3979 . . . . . . . . . . . . . . . . . . . 20
71 iccf 10959 . . . . . . . . . . . . . . . . . . . . . 22
72 ffn 5550 . . . . . . . . . . . . . . . . . . . . . 22
7371, 72ax-mp 8 . . . . . . . . . . . . . . . . . . . . 21
74 ressxr 9085 . . . . . . . . . . . . . . . . . . . . . . 23
75 xpss12 4940 . . . . . . . . . . . . . . . . . . . . . . 23
7674, 74, 75mp2an 654 . . . . . . . . . . . . . . . . . . . . . 22
7761, 76sstri 3317 . . . . . . . . . . . . . . . . . . . . 21
78 eleq2 2465 . . . . . . . . . . . . . . . . . . . . . 22
7978rexima 5936 . . . . . . . . . . . . . . . . . . . . 21
8073, 77, 79mp2an 654 . . . . . . . . . . . . . . . . . . . 20
8170, 80bitri 241 . . . . . . . . . . . . . . . . . . 19
8261sseli 3304 . . . . . . . . . . . . . . . . . . . . . . . 24
83 1st2nd2 6345 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
8483fveq2d 5691 . . . . . . . . . . . . . . . . . . . . . . . . . 26
85 df-ov 6043 . . . . . . . . . . . . . . . . . . . . . . . . . 26
8684, 85syl6eqr 2454 . . . . . . . . . . . . . . . . . . . . . . . . 25
8786eleq2d 2471 . . . . . . . . . . . . . . . . . . . . . . . 24
8882, 87syl 16 . . . . . . . . . . . . . . . . . . . . . . 23
8988biimpd 199 . . . . . . . . . . . . . . . . . . . . . 22
9089imdistani 672 . . . . . . . . . . . . . . . . . . . . 21
91 iccssxr 10949 . . . . . . . . . . . . . . . . . . . . . . . 24
9291sseli 3304 . . . . . . . . . . . . . . . . . . . . . . 23
9392ad2antll 710 . . . . . . . . . . . . . . . . . . . . . 22
94 xp2nd 6336 . . . . . . . . . . . . . . . . . . . . . . . . 25
9594rexrd 9090 . . . . . . . . . . . . . . . . . . . . . . . 24
9682, 95syl 16 . . . . . . . . . . . . . . . . . . . . . . 23
9796ad2antrl 709 . . . . . . . . . . . . . . . . . . . . . 22
98 simpllr 736 . . . . . . . . . . . . . . . . . . . . . . 23
9998rexrd 9090 . . . . . . . . . . . . . . . . . . . . . 22
100 xp1st 6335 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
101100rexrd 9090 . . . . . . . . . . . . . . . . . . . . . . . . . 26
102101, 95jca 519 . . . . . . . . . . . . . . . . . . . . . . . . 25
10382, 102syl 16 . . . . . . . . . . . . . . . . . . . . . . . 24
104 iccleub 10923 . . . . . . . . . . . . . . . . . . . . . . . . 25
1051043expa 1153 . . . . . . . . . . . . . . . . . . . . . . . 24
106103, 105sylan 458 . . . . . . . . . . . . . . . . . . . . . . 23
107106adantl 453 . . . . . . . . . . . . . . . . . . . . . 22
108 xpss 4941 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
10961, 108sstri 3317 . . . . . . . . . . . . . . . . . . . . . . . . . 26
110 df-rel 4844 . . . . . . . . . . . . . . . . . . . . . . . . . 26
111109, 110mpbir 201 . . . . . . . . . . . . . . . . . . . . . . . . 25
112 2ndrn 6354 . . . . . . . . . . . . . . . . . . . . . . . . 25
113111, 112mpan 652 . . . . . . . . . . . . . . . . . . . . . . . 24
114 breq1 4175 . . . . . . . . . . . . . . . . . . . . . . . . 25
115114rspccva 3011 . . . . . . . . . . . . . . . . . . . . . . . 24
116113, 115sylan2 461 . . . . . . . . . . . . . . . . . . . . . . 23
117116ad2ant2lr 729 . . . . . . . . . . . . . . . . . . . . . 22
11893, 97, 99, 107, 117xrletrd 10708 . . . . . . . . . . . . . . . . . . . . 21
11990, 118sylan2 461 . . . . . . . . . . . . . . . . . . . 20
120119rexlimdvaa 2791 . . . . . . . . . . . . . . . . . . 19
12181, 120syl5bi 209 . . . . . . . . . . . . . . . . . 18
122121ralrimiv 2748 . . . . . . . . . . . . . . . . 17
123 raleq 2864 . . . . . . . . . . . . . . . . . 18
124123ad2antrr 707 . . . . . . . . . . . . . . . . 17
125122, 124mpbid 202 . . . . . . . . . . . . . . . 16
126125ex 424 . . . . . . . . . . . . . . 15
127126reximdva 2778 . . . . . . . . . . . . . 14
128127adantr 452 . . . . . . . . . . . . 13
12969, 128mpd 15 . . . . . . . . . . . 12
13032, 129nsyl 115 . . . . . . . . . . 11
131130adantl 453 . . . . . . . . . 10
132 uniretop 18749 . . . . . . . . . . . . . 14
133 retopcon 18813 . . . . . . . . . . . . . . 15
134133a1i 11 . . . . . . . . . . . . . 14
135 simpll 731 . . . . . . . . . . . . . 14
136 simplr 732 . . . . . . . . . . . . . 14
137 simprl 733 . . . . . . . . . . . . . . 15