Metamath Proof Explorer


Theorem ovolval4lem2

Description: The value of the Lebesgue outer measure for subsets of the reals. Similar to ovolval3 , but here f is may represent unordered interval bounds. (Contributed by Glauco Siliprandi, 3-Mar-2021)

Ref Expression
Hypotheses ovolval4lem2.a φ A
ovolval4lem2.m M = y * | f 2 A ran . f y = sum^ vol . f
ovolval4lem2.g G = n 1 st f n if 1 st f n 2 nd f n 2 nd f n 1 st f n
Assertion ovolval4lem2 φ vol * A = sup M * <

Proof

Step Hyp Ref Expression
1 ovolval4lem2.a φ A
2 ovolval4lem2.m M = y * | f 2 A ran . f y = sum^ vol . f
3 ovolval4lem2.g G = n 1 st f n if 1 st f n 2 nd f n 2 nd f n 1 st f n
4 iftrue 1 st f n 2 nd f n if 1 st f n 2 nd f n 2 nd f n 1 st f n = 2 nd f n
5 4 opeq2d 1 st f n 2 nd f n 1 st f n if 1 st f n 2 nd f n 2 nd f n 1 st f n = 1 st f n 2 nd f n
6 5 adantl f 2 n 1 st f n 2 nd f n 1 st f n if 1 st f n 2 nd f n 2 nd f n 1 st f n = 1 st f n 2 nd f n
7 df-br 1 st f n 2 nd f n 1 st f n 2 nd f n
8 7 biimpi 1 st f n 2 nd f n 1 st f n 2 nd f n
9 8 adantl f 2 n 1 st f n 2 nd f n 1 st f n 2 nd f n
10 6 9 eqeltrd f 2 n 1 st f n 2 nd f n 1 st f n if 1 st f n 2 nd f n 2 nd f n 1 st f n
11 iffalse ¬ 1 st f n 2 nd f n if 1 st f n 2 nd f n 2 nd f n 1 st f n = 1 st f n
12 11 opeq2d ¬ 1 st f n 2 nd f n 1 st f n if 1 st f n 2 nd f n 2 nd f n 1 st f n = 1 st f n 1 st f n
13 12 adantl f 2 n ¬ 1 st f n 2 nd f n 1 st f n if 1 st f n 2 nd f n 2 nd f n 1 st f n = 1 st f n 1 st f n
14 elmapi f 2 f : 2
15 14 ffvelrnda f 2 n f n 2
16 xp1st f n 2 1 st f n
17 15 16 syl f 2 n 1 st f n
18 17 leidd f 2 n 1 st f n 1 st f n
19 df-br 1 st f n 1 st f n 1 st f n 1 st f n
20 18 19 sylib f 2 n 1 st f n 1 st f n
21 20 adantr f 2 n ¬ 1 st f n 2 nd f n 1 st f n 1 st f n
22 13 21 eqeltrd f 2 n ¬ 1 st f n 2 nd f n 1 st f n if 1 st f n 2 nd f n 2 nd f n 1 st f n
23 10 22 pm2.61dan f 2 n 1 st f n if 1 st f n 2 nd f n 2 nd f n 1 st f n
24 xp2nd f n 2 2 nd f n
25 15 24 syl f 2 n 2 nd f n
26 25 17 ifcld f 2 n if 1 st f n 2 nd f n 2 nd f n 1 st f n
27 opelxpi 1 st f n if 1 st f n 2 nd f n 2 nd f n 1 st f n 1 st f n if 1 st f n 2 nd f n 2 nd f n 1 st f n 2
28 17 26 27 syl2anc f 2 n 1 st f n if 1 st f n 2 nd f n 2 nd f n 1 st f n 2
29 23 28 elind f 2 n 1 st f n if 1 st f n 2 nd f n 2 nd f n 1 st f n 2
30 29 3 fmptd f 2 G : 2
31 reex V
32 31 31 xpex 2 V
33 32 inex2 2 V
34 33 a1i f 2 2 V
35 nnex V
36 35 a1i f 2 V
37 34 36 elmapd f 2 G 2 G : 2
38 30 37 mpbird f 2 G 2
39 38 adantr f 2 A ran . f y = sum^ vol . f G 2
40 simpr f 2 A ran . f A ran . f
41 rexpssxrxp 2 * × *
42 41 a1i f 2 2 * × *
43 14 42 fssd f 2 f : * × *
44 2fveq3 k = n 1 st f k = 1 st f n
45 2fveq3 k = n 2 nd f k = 2 nd f n
46 44 45 breq12d k = n 1 st f k 2 nd f k 1 st f n 2 nd f n
47 46 cbvrabv k | 1 st f k 2 nd f k = n | 1 st f n 2 nd f n
48 43 3 47 ovolval4lem1 f 2 ran . f = ran . G vol . f = vol . G
49 48 simpld f 2 ran . f = ran . G
50 49 adantr f 2 A ran . f ran . f = ran . G
51 40 50 sseqtrd f 2 A ran . f A ran . G
52 51 adantrr f 2 A ran . f y = sum^ vol . f A ran . G
53 simpr f 2 y = sum^ vol . f y = sum^ vol . f
54 48 simprd f 2 vol . f = vol . G
55 coass vol . f = vol . f
56 55 a1i f 2 vol . f = vol . f
57 coass vol . G = vol . G
58 57 a1i f 2 vol . G = vol . G
59 54 56 58 3eqtr4d f 2 vol . f = vol . G
60 59 fveq2d f 2 sum^ vol . f = sum^ vol . G
61 60 adantr f 2 y = sum^ vol . f sum^ vol . f = sum^ vol . G
62 53 61 eqtrd f 2 y = sum^ vol . f y = sum^ vol . G
63 62 adantrl f 2 A ran . f y = sum^ vol . f y = sum^ vol . G
64 52 63 jca f 2 A ran . f y = sum^ vol . f A ran . G y = sum^ vol . G
65 coeq2 g = G . g = . G
66 65 rneqd g = G ran . g = ran . G
67 66 unieqd g = G ran . g = ran . G
68 67 sseq2d g = G A ran . g A ran . G
69 coeq2 g = G vol . g = vol . G
70 69 fveq2d g = G sum^ vol . g = sum^ vol . G
71 70 eqeq2d g = G y = sum^ vol . g y = sum^ vol . G
72 68 71 anbi12d g = G A ran . g y = sum^ vol . g A ran . G y = sum^ vol . G
73 72 rspcev G 2 A ran . G y = sum^ vol . G g 2 A ran . g y = sum^ vol . g
74 39 64 73 syl2anc f 2 A ran . f y = sum^ vol . f g 2 A ran . g y = sum^ vol . g
75 74 rexlimiva f 2 A ran . f y = sum^ vol . f g 2 A ran . g y = sum^ vol . g
76 inss2 2 2
77 mapss 2 V 2 2 2 2
78 32 76 77 mp2an 2 2
79 78 sseli g 2 g 2
80 79 adantr g 2 A ran . g y = sum^ vol . g g 2
81 simpr g 2 A ran . g y = sum^ vol . g A ran . g y = sum^ vol . g
82 coeq2 f = g . f = . g
83 82 rneqd f = g ran . f = ran . g
84 83 unieqd f = g ran . f = ran . g
85 84 sseq2d f = g A ran . f A ran . g
86 coeq2 f = g vol . f = vol . g
87 86 fveq2d f = g sum^ vol . f = sum^ vol . g
88 87 eqeq2d f = g y = sum^ vol . f y = sum^ vol . g
89 85 88 anbi12d f = g A ran . f y = sum^ vol . f A ran . g y = sum^ vol . g
90 89 rspcev g 2 A ran . g y = sum^ vol . g f 2 A ran . f y = sum^ vol . f
91 80 81 90 syl2anc g 2 A ran . g y = sum^ vol . g f 2 A ran . f y = sum^ vol . f
92 91 rexlimiva g 2 A ran . g y = sum^ vol . g f 2 A ran . f y = sum^ vol . f
93 75 92 impbii f 2 A ran . f y = sum^ vol . f g 2 A ran . g y = sum^ vol . g
94 93 rabbii y * | f 2 A ran . f y = sum^ vol . f = y * | g 2 A ran . g y = sum^ vol . g
95 2 94 eqtri M = y * | g 2 A ran . g y = sum^ vol . g
96 1 95 ovolval3 φ vol * A = sup M * <