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 )