Metamath Proof Explorer


Theorem uniioombl

Description: A disjoint union of open intervals is measurable. (This proof does not use countable choice, unlike iunmbl .) Lemma 565Ca of Fremlin5 p. 214. (Contributed by Mario Carneiro, 26-Mar-2015)

Ref Expression
Hypotheses uniioombl.1 φ F : 2
uniioombl.2 φ Disj x . F x
uniioombl.3 S = seq 1 + abs F
Assertion uniioombl φ ran . F dom vol

Proof

Step Hyp Ref Expression
1 uniioombl.1 φ F : 2
2 uniioombl.2 φ Disj x . F x
3 uniioombl.3 S = seq 1 + abs F
4 ioof . : * × * 𝒫
5 inss2 2 2
6 rexpssxrxp 2 * × *
7 5 6 sstri 2 * × *
8 fss F : 2 2 * × * F : * × *
9 1 7 8 sylancl φ F : * × *
10 fco . : * × * 𝒫 F : * × * . F : 𝒫
11 4 9 10 sylancr φ . F : 𝒫
12 11 frnd φ ran . F 𝒫
13 sspwuni ran . F 𝒫 ran . F
14 12 13 sylib φ ran . F
15 elpwi z 𝒫 z
16 15 ad2antrl φ z 𝒫 vol * z z
17 simprr φ z 𝒫 vol * z vol * z
18 rphalfcl r + r 2 +
19 18 rphalfcld r + r 2 2 +
20 eqid seq 1 + abs f = seq 1 + abs f
21 20 ovolgelb z vol * z r 2 2 + f 2 z ran . f sup ran seq 1 + abs f * < vol * z + r 2 2
22 16 17 19 21 syl2an3an φ z 𝒫 vol * z r + f 2 z ran . f sup ran seq 1 + abs f * < vol * z + r 2 2
23 1 ad3antrrr φ z 𝒫 vol * z r + f 2 z ran . f sup ran seq 1 + abs f * < vol * z + r 2 2 F : 2
24 2 ad3antrrr φ z 𝒫 vol * z r + f 2 z ran . f sup ran seq 1 + abs f * < vol * z + r 2 2 Disj x . F x
25 eqid ran . F = ran . F
26 17 adantr φ z 𝒫 vol * z r + vol * z
27 26 adantr φ z 𝒫 vol * z r + f 2 z ran . f sup ran seq 1 + abs f * < vol * z + r 2 2 vol * z
28 18 adantl φ z 𝒫 vol * z r + r 2 +
29 28 adantr φ z 𝒫 vol * z r + f 2 z ran . f sup ran seq 1 + abs f * < vol * z + r 2 2 r 2 +
30 29 rphalfcld φ z 𝒫 vol * z r + f 2 z ran . f sup ran seq 1 + abs f * < vol * z + r 2 2 r 2 2 +
31 elmapi f 2 f : 2
32 31 ad2antrl φ z 𝒫 vol * z r + f 2 z ran . f sup ran seq 1 + abs f * < vol * z + r 2 2 f : 2
33 simprrl φ z 𝒫 vol * z r + f 2 z ran . f sup ran seq 1 + abs f * < vol * z + r 2 2 z ran . f
34 simprrr φ z 𝒫 vol * z r + f 2 z ran . f sup ran seq 1 + abs f * < vol * z + r 2 2 sup ran seq 1 + abs f * < vol * z + r 2 2
35 23 24 3 25 27 30 32 33 20 34 uniioombllem6 φ z 𝒫 vol * z r + f 2 z ran . f sup ran seq 1 + abs f * < vol * z + r 2 2 vol * z ran . F + vol * z ran . F vol * z + 4 r 2 2
36 22 35 rexlimddv φ z 𝒫 vol * z r + vol * z ran . F + vol * z ran . F vol * z + 4 r 2 2
37 rpcn r + r
38 37 adantl φ z 𝒫 vol * z r + r
39 2cnd φ z 𝒫 vol * z r + 2
40 2ne0 2 0
41 40 a1i φ z 𝒫 vol * z r + 2 0
42 38 39 39 41 41 divdiv1d φ z 𝒫 vol * z r + r 2 2 = r 2 2
43 2t2e4 2 2 = 4
44 43 oveq2i r 2 2 = r 4
45 42 44 eqtrdi φ z 𝒫 vol * z r + r 2 2 = r 4
46 45 oveq2d φ z 𝒫 vol * z r + 4 r 2 2 = 4 r 4
47 4cn 4
48 47 a1i φ z 𝒫 vol * z r + 4
49 4ne0 4 0
50 49 a1i φ z 𝒫 vol * z r + 4 0
51 38 48 50 divcan2d φ z 𝒫 vol * z r + 4 r 4 = r
52 46 51 eqtrd φ z 𝒫 vol * z r + 4 r 2 2 = r
53 52 oveq2d φ z 𝒫 vol * z r + vol * z + 4 r 2 2 = vol * z + r
54 36 53 breqtrd φ z 𝒫 vol * z r + vol * z ran . F + vol * z ran . F vol * z + r
55 54 ralrimiva φ z 𝒫 vol * z r + vol * z ran . F + vol * z ran . F vol * z + r
56 inss1 z ran . F z
57 56 a1i φ z 𝒫 vol * z z ran . F z
58 ovolsscl z ran . F z z vol * z vol * z ran . F
59 57 16 17 58 syl3anc φ z 𝒫 vol * z vol * z ran . F
60 difssd φ z 𝒫 vol * z z ran . F z
61 ovolsscl z ran . F z z vol * z vol * z ran . F
62 60 16 17 61 syl3anc φ z 𝒫 vol * z vol * z ran . F
63 59 62 readdcld φ z 𝒫 vol * z vol * z ran . F + vol * z ran . F
64 alrple vol * z ran . F + vol * z ran . F vol * z vol * z ran . F + vol * z ran . F vol * z r + vol * z ran . F + vol * z ran . F vol * z + r
65 63 17 64 syl2anc φ z 𝒫 vol * z vol * z ran . F + vol * z ran . F vol * z r + vol * z ran . F + vol * z ran . F vol * z + r
66 55 65 mpbird φ z 𝒫 vol * z vol * z ran . F + vol * z ran . F vol * z
67 66 expr φ z 𝒫 vol * z vol * z ran . F + vol * z ran . F vol * z
68 67 ralrimiva φ z 𝒫 vol * z vol * z ran . F + vol * z ran . F vol * z
69 ismbl2 ran . F dom vol ran . F z 𝒫 vol * z vol * z ran . F + vol * z ran . F vol * z
70 14 68 69 sylanbrc φ ran . F dom vol