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 
|- ( ph -> F : NN --> ( <_ i^i ( RR X. RR ) ) )
uniioombl.2 
|- ( ph -> Disj_ x e. NN ( (,) ` ( F ` x ) ) )
uniioombl.3 
|- S = seq 1 ( + , ( ( abs o. - ) o. F ) )
Assertion uniioombl 
|- ( ph -> U. ran ( (,) o. F ) e. dom vol )

Proof

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