Metamath Proof Explorer


Theorem ovolfioo

Description: Unpack the interval covering property of the outer measure definition. (Contributed by Mario Carneiro, 16-Mar-2014)

Ref Expression
Assertion ovolfioo A F : 2 A ran . F z A n 1 st F n < z z < 2 nd F n

Proof

Step Hyp Ref Expression
1 ioof . : * × * 𝒫
2 inss2 2 2
3 rexpssxrxp 2 * × *
4 2 3 sstri 2 * × *
5 fss F : 2 2 * × * F : * × *
6 4 5 mpan2 F : 2 F : * × *
7 fco . : * × * 𝒫 F : * × * . F : 𝒫
8 1 6 7 sylancr F : 2 . F : 𝒫
9 ffn . F : 𝒫 . F Fn
10 fniunfv . F Fn n . F n = ran . F
11 8 9 10 3syl F : 2 n . F n = ran . F
12 11 sseq2d F : 2 A n . F n A ran . F
13 12 adantl A F : 2 A n . F n A ran . F
14 dfss3 A n . F n z A z n . F n
15 ssel2 A z A z
16 eliun z n . F n n z . F n
17 rexr z z *
18 17 ad2antrr z F : 2 n z *
19 fvco3 F : 2 n . F n = . F n
20 ffvelrn F : 2 n F n 2
21 20 elin2d F : 2 n F n 2
22 1st2nd2 F n 2 F n = 1 st F n 2 nd F n
23 21 22 syl F : 2 n F n = 1 st F n 2 nd F n
24 23 fveq2d F : 2 n . F n = . 1 st F n 2 nd F n
25 df-ov 1 st F n 2 nd F n = . 1 st F n 2 nd F n
26 24 25 eqtr4di F : 2 n . F n = 1 st F n 2 nd F n
27 19 26 eqtrd F : 2 n . F n = 1 st F n 2 nd F n
28 27 eleq2d F : 2 n z . F n z 1 st F n 2 nd F n
29 ovolfcl F : 2 n 1 st F n 2 nd F n 1 st F n 2 nd F n
30 rexr 1 st F n 1 st F n *
31 rexr 2 nd F n 2 nd F n *
32 elioo1 1 st F n * 2 nd F n * z 1 st F n 2 nd F n z * 1 st F n < z z < 2 nd F n
33 30 31 32 syl2an 1 st F n 2 nd F n z 1 st F n 2 nd F n z * 1 st F n < z z < 2 nd F n
34 3anass z * 1 st F n < z z < 2 nd F n z * 1 st F n < z z < 2 nd F n
35 33 34 bitrdi 1 st F n 2 nd F n z 1 st F n 2 nd F n z * 1 st F n < z z < 2 nd F n
36 35 3adant3 1 st F n 2 nd F n 1 st F n 2 nd F n z 1 st F n 2 nd F n z * 1 st F n < z z < 2 nd F n
37 29 36 syl F : 2 n z 1 st F n 2 nd F n z * 1 st F n < z z < 2 nd F n
38 28 37 bitrd F : 2 n z . F n z * 1 st F n < z z < 2 nd F n
39 38 adantll z F : 2 n z . F n z * 1 st F n < z z < 2 nd F n
40 18 39 mpbirand z F : 2 n z . F n 1 st F n < z z < 2 nd F n
41 40 rexbidva z F : 2 n z . F n n 1 st F n < z z < 2 nd F n
42 16 41 syl5bb z F : 2 z n . F n n 1 st F n < z z < 2 nd F n
43 15 42 sylan A z A F : 2 z n . F n n 1 st F n < z z < 2 nd F n
44 43 an32s A F : 2 z A z n . F n n 1 st F n < z z < 2 nd F n
45 44 ralbidva A F : 2 z A z n . F n z A n 1 st F n < z z < 2 nd F n
46 14 45 syl5bb A F : 2 A n . F n z A n 1 st F n < z z < 2 nd F n
47 13 46 bitr3d A F : 2 A ran . F z A n 1 st F n < z z < 2 nd F n