Metamath Proof Explorer

Theorem uniioovol

Description: A disjoint union of open intervals has volume equal to the sum of the volume of the intervals. (This proof does not use countable choice, unlike voliun .) Lemma 565Ca of Fremlin5 p. 213. (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 uniioovol 
|- ( ph -> ( vol* ` U. ran ( (,) o. F ) ) = sup ( ran S , RR* , < ) )

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 ovolcl 
 |-  ( U. ran ( (,) o. F ) C_ RR -> ( vol* ` U. ran ( (,) o. F ) ) e. RR* )
16 14 15 syl 
 |-  ( ph -> ( vol* ` U. ran ( (,) o. F ) ) e. RR* )
17 eqid 
 |-  ( ( abs o. - ) o. F ) = ( ( abs o. - ) o. F )
18 17 3 ovolsf 
 |-  ( F : NN --> ( <_ i^i ( RR X. RR ) ) -> S : NN --> ( 0 [,) +oo ) )
19 frn 
 |-  ( S : NN --> ( 0 [,) +oo ) -> ran S C_ ( 0 [,) +oo ) )
20 1 18 19 3syl 
 |-  ( ph -> ran S C_ ( 0 [,) +oo ) )
21 icossxr 
 |-  ( 0 [,) +oo ) C_ RR*
22 20 21 sstrdi 
 |-  ( ph -> ran S C_ RR* )
23 supxrcl 
 |-  ( ran S C_ RR* -> sup ( ran S , RR* , < ) e. RR* )
24 22 23 syl 
 |-  ( ph -> sup ( ran S , RR* , < ) e. RR* )
25 ssid 
 |-  U. ran ( (,) o. F ) C_ U. ran ( (,) o. F )
26 3 ovollb 
 |-  ( ( F : NN --> ( <_ i^i ( RR X. RR ) ) /\ U. ran ( (,) o. F ) C_ U. ran ( (,) o. F ) ) -> ( vol* ` U. ran ( (,) o. F ) ) <_ sup ( ran S , RR* , < ) )
27 1 25 26 sylancl 
 |-  ( ph -> ( vol* ` U. ran ( (,) o. F ) ) <_ sup ( ran S , RR* , < ) )
28 3 fveq1i 
 |-  ( S ` n ) = ( seq 1 ( + , ( ( abs o. - ) o. F ) ) ` n )
29 1 adantr 
 |-  ( ( ph /\ n e. NN ) -> F : NN --> ( <_ i^i ( RR X. RR ) ) )
30 elfznn 
 |-  ( x e. ( 1 ... n ) -> x e. NN )
31 17 ovolfsval 
 |-  ( ( F : NN --> ( <_ i^i ( RR X. RR ) ) /\ x e. NN ) -> ( ( ( abs o. - ) o. F ) ` x ) = ( ( 2nd ` ( F ` x ) ) - ( 1st ` ( F ` x ) ) ) )
32 29 30 31 syl2an 
 |-  ( ( ( ph /\ n e. NN ) /\ x e. ( 1 ... n ) ) -> ( ( ( abs o. - ) o. F ) ` x ) = ( ( 2nd ` ( F ` x ) ) - ( 1st ` ( F ` x ) ) ) )
33 fvco3 
 |-  ( ( F : NN --> ( <_ i^i ( RR X. RR ) ) /\ x e. NN ) -> ( ( (,) o. F ) ` x ) = ( (,) ` ( F ` x ) ) )
34 29 30 33 syl2an 
 |-  ( ( ( ph /\ n e. NN ) /\ x e. ( 1 ... n ) ) -> ( ( (,) o. F ) ` x ) = ( (,) ` ( F ` x ) ) )
35 ffvelrn 
 |-  ( ( F : NN --> ( <_ i^i ( RR X. RR ) ) /\ x e. NN ) -> ( F ` x ) e. ( <_ i^i ( RR X. RR ) ) )
36 29 30 35 syl2an 
 |-  ( ( ( ph /\ n e. NN ) /\ x e. ( 1 ... n ) ) -> ( F ` x ) e. ( <_ i^i ( RR X. RR ) ) )
37 36 elin2d 
 |-  ( ( ( ph /\ n e. NN ) /\ x e. ( 1 ... n ) ) -> ( F ` x ) e. ( RR X. RR ) )
38 1st2nd2 
 |-  ( ( F ` x ) e. ( RR X. RR ) -> ( F ` x ) = <. ( 1st ` ( F ` x ) ) , ( 2nd ` ( F ` x ) ) >. )
39 37 38 syl 
 |-  ( ( ( ph /\ n e. NN ) /\ x e. ( 1 ... n ) ) -> ( F ` x ) = <. ( 1st ` ( F ` x ) ) , ( 2nd ` ( F ` x ) ) >. )
40 39 fveq2d 
 |-  ( ( ( ph /\ n e. NN ) /\ x e. ( 1 ... n ) ) -> ( (,) ` ( F ` x ) ) = ( (,) ` <. ( 1st ` ( F ` x ) ) , ( 2nd ` ( F ` x ) ) >. ) )
41 df-ov 
 |-  ( ( 1st ` ( F ` x ) ) (,) ( 2nd ` ( F ` x ) ) ) = ( (,) ` <. ( 1st ` ( F ` x ) ) , ( 2nd ` ( F ` x ) ) >. )
42 40 41 eqtr4di 
 |-  ( ( ( ph /\ n e. NN ) /\ x e. ( 1 ... n ) ) -> ( (,) ` ( F ` x ) ) = ( ( 1st ` ( F ` x ) ) (,) ( 2nd ` ( F ` x ) ) ) )
43 34 42 eqtrd 
 |-  ( ( ( ph /\ n e. NN ) /\ x e. ( 1 ... n ) ) -> ( ( (,) o. F ) ` x ) = ( ( 1st ` ( F ` x ) ) (,) ( 2nd ` ( F ` x ) ) ) )
44 ioombl 
 |-  ( ( 1st ` ( F ` x ) ) (,) ( 2nd ` ( F ` x ) ) ) e. dom vol
45 43 44 eqeltrdi 
 |-  ( ( ( ph /\ n e. NN ) /\ x e. ( 1 ... n ) ) -> ( ( (,) o. F ) ` x ) e. dom vol )
46 mblvol 
 |-  ( ( ( (,) o. F ) ` x ) e. dom vol -> ( vol ` ( ( (,) o. F ) ` x ) ) = ( vol* ` ( ( (,) o. F ) ` x ) ) )
47 45 46 syl 
 |-  ( ( ( ph /\ n e. NN ) /\ x e. ( 1 ... n ) ) -> ( vol ` ( ( (,) o. F ) ` x ) ) = ( vol* ` ( ( (,) o. F ) ` x ) ) )
48 43 fveq2d 
 |-  ( ( ( ph /\ n e. NN ) /\ x e. ( 1 ... n ) ) -> ( vol* ` ( ( (,) o. F ) ` x ) ) = ( vol* ` ( ( 1st ` ( F ` x ) ) (,) ( 2nd ` ( F ` x ) ) ) ) )
49 ovolfcl 
 |-  ( ( F : NN --> ( <_ i^i ( RR X. RR ) ) /\ x e. NN ) -> ( ( 1st ` ( F ` x ) ) e. RR /\ ( 2nd ` ( F ` x ) ) e. RR /\ ( 1st ` ( F ` x ) ) <_ ( 2nd ` ( F ` x ) ) ) )
50 29 30 49 syl2an 
 |-  ( ( ( ph /\ n e. NN ) /\ x e. ( 1 ... n ) ) -> ( ( 1st ` ( F ` x ) ) e. RR /\ ( 2nd ` ( F ` x ) ) e. RR /\ ( 1st ` ( F ` x ) ) <_ ( 2nd ` ( F ` x ) ) ) )
51 ovolioo 
 |-  ( ( ( 1st ` ( F ` x ) ) e. RR /\ ( 2nd ` ( F ` x ) ) e. RR /\ ( 1st ` ( F ` x ) ) <_ ( 2nd ` ( F ` x ) ) ) -> ( vol* ` ( ( 1st ` ( F ` x ) ) (,) ( 2nd ` ( F ` x ) ) ) ) = ( ( 2nd ` ( F ` x ) ) - ( 1st ` ( F ` x ) ) ) )
52 50 51 syl 
 |-  ( ( ( ph /\ n e. NN ) /\ x e. ( 1 ... n ) ) -> ( vol* ` ( ( 1st ` ( F ` x ) ) (,) ( 2nd ` ( F ` x ) ) ) ) = ( ( 2nd ` ( F ` x ) ) - ( 1st ` ( F ` x ) ) ) )
53 47 48 52 3eqtrd 
 |-  ( ( ( ph /\ n e. NN ) /\ x e. ( 1 ... n ) ) -> ( vol ` ( ( (,) o. F ) ` x ) ) = ( ( 2nd ` ( F ` x ) ) - ( 1st ` ( F ` x ) ) ) )
54 32 53 eqtr4d 
 |-  ( ( ( ph /\ n e. NN ) /\ x e. ( 1 ... n ) ) -> ( ( ( abs o. - ) o. F ) ` x ) = ( vol ` ( ( (,) o. F ) ` x ) ) )
55 simpr 
 |-  ( ( ph /\ n e. NN ) -> n e. NN )
56 nnuz 
 |-  NN = ( ZZ>= ` 1 )
57 55 56 eleqtrdi 
 |-  ( ( ph /\ n e. NN ) -> n e. ( ZZ>= ` 1 ) )
58 50 simp2d 
 |-  ( ( ( ph /\ n e. NN ) /\ x e. ( 1 ... n ) ) -> ( 2nd ` ( F ` x ) ) e. RR )
59 50 simp1d 
 |-  ( ( ( ph /\ n e. NN ) /\ x e. ( 1 ... n ) ) -> ( 1st ` ( F ` x ) ) e. RR )
60 58 59 resubcld 
 |-  ( ( ( ph /\ n e. NN ) /\ x e. ( 1 ... n ) ) -> ( ( 2nd ` ( F ` x ) ) - ( 1st ` ( F ` x ) ) ) e. RR )
61 53 60 eqeltrd 
 |-  ( ( ( ph /\ n e. NN ) /\ x e. ( 1 ... n ) ) -> ( vol ` ( ( (,) o. F ) ` x ) ) e. RR )
62 61 recnd 
 |-  ( ( ( ph /\ n e. NN ) /\ x e. ( 1 ... n ) ) -> ( vol ` ( ( (,) o. F ) ` x ) ) e. CC )
63 54 57 62 fsumser 
 |-  ( ( ph /\ n e. NN ) -> sum_ x e. ( 1 ... n ) ( vol ` ( ( (,) o. F ) ` x ) ) = ( seq 1 ( + , ( ( abs o. - ) o. F ) ) ` n ) )
64 28 63 eqtr4id 
 |-  ( ( ph /\ n e. NN ) -> ( S ` n ) = sum_ x e. ( 1 ... n ) ( vol ` ( ( (,) o. F ) ` x ) ) )
65 fzfid 
 |-  ( ( ph /\ n e. NN ) -> ( 1 ... n ) e. Fin )
66 45 61 jca 
 |-  ( ( ( ph /\ n e. NN ) /\ x e. ( 1 ... n ) ) -> ( ( ( (,) o. F ) ` x ) e. dom vol /\ ( vol ` ( ( (,) o. F ) ` x ) ) e. RR ) )
67 66 ralrimiva 
 |-  ( ( ph /\ n e. NN ) -> A. x e. ( 1 ... n ) ( ( ( (,) o. F ) ` x ) e. dom vol /\ ( vol ` ( ( (,) o. F ) ` x ) ) e. RR ) )
68 fz1ssnn 
 |-  ( 1 ... n ) C_ NN
69 1 33 sylan 
 |-  ( ( ph /\ x e. NN ) -> ( ( (,) o. F ) ` x ) = ( (,) ` ( F ` x ) ) )
70 69 disjeq2dv 
 |-  ( ph -> ( Disj_ x e. NN ( ( (,) o. F ) ` x ) <-> Disj_ x e. NN ( (,) ` ( F ` x ) ) ) )
71 2 70 mpbird 
 |-  ( ph -> Disj_ x e. NN ( ( (,) o. F ) ` x ) )
72 71 adantr 
 |-  ( ( ph /\ n e. NN ) -> Disj_ x e. NN ( ( (,) o. F ) ` x ) )
73 disjss1 
 |-  ( ( 1 ... n ) C_ NN -> ( Disj_ x e. NN ( ( (,) o. F ) ` x ) -> Disj_ x e. ( 1 ... n ) ( ( (,) o. F ) ` x ) ) )
74 68 72 73 mpsyl 
 |-  ( ( ph /\ n e. NN ) -> Disj_ x e. ( 1 ... n ) ( ( (,) o. F ) ` x ) )
75 volfiniun 
 |-  ( ( ( 1 ... n ) e. Fin /\ A. x e. ( 1 ... n ) ( ( ( (,) o. F ) ` x ) e. dom vol /\ ( vol ` ( ( (,) o. F ) ` x ) ) e. RR ) /\ Disj_ x e. ( 1 ... n ) ( ( (,) o. F ) ` x ) ) -> ( vol ` U_ x e. ( 1 ... n ) ( ( (,) o. F ) ` x ) ) = sum_ x e. ( 1 ... n ) ( vol ` ( ( (,) o. F ) ` x ) ) )
76 65 67 74 75 syl3anc 
 |-  ( ( ph /\ n e. NN ) -> ( vol ` U_ x e. ( 1 ... n ) ( ( (,) o. F ) ` x ) ) = sum_ x e. ( 1 ... n ) ( vol ` ( ( (,) o. F ) ` x ) ) )
77 45 ralrimiva 
 |-  ( ( ph /\ n e. NN ) -> A. x e. ( 1 ... n ) ( ( (,) o. F ) ` x ) e. dom vol )
78 finiunmbl 
 |-  ( ( ( 1 ... n ) e. Fin /\ A. x e. ( 1 ... n ) ( ( (,) o. F ) ` x ) e. dom vol ) -> U_ x e. ( 1 ... n ) ( ( (,) o. F ) ` x ) e. dom vol )
79 65 77 78 syl2anc 
 |-  ( ( ph /\ n e. NN ) -> U_ x e. ( 1 ... n ) ( ( (,) o. F ) ` x ) e. dom vol )
80 mblvol 
 |-  ( U_ x e. ( 1 ... n ) ( ( (,) o. F ) ` x ) e. dom vol -> ( vol ` U_ x e. ( 1 ... n ) ( ( (,) o. F ) ` x ) ) = ( vol* ` U_ x e. ( 1 ... n ) ( ( (,) o. F ) ` x ) ) )
81 79 80 syl 
 |-  ( ( ph /\ n e. NN ) -> ( vol ` U_ x e. ( 1 ... n ) ( ( (,) o. F ) ` x ) ) = ( vol* ` U_ x e. ( 1 ... n ) ( ( (,) o. F ) ` x ) ) )
82 64 76 81 3eqtr2d 
 |-  ( ( ph /\ n e. NN ) -> ( S ` n ) = ( vol* ` U_ x e. ( 1 ... n ) ( ( (,) o. F ) ` x ) ) )
83 iunss1 
 |-  ( ( 1 ... n ) C_ NN -> U_ x e. ( 1 ... n ) ( ( (,) o. F ) ` x ) C_ U_ x e. NN ( ( (,) o. F ) ` x ) )
84 68 83 mp1i 
 |-  ( ( ph /\ n e. NN ) -> U_ x e. ( 1 ... n ) ( ( (,) o. F ) ` x ) C_ U_ x e. NN ( ( (,) o. F ) ` x ) )
85 11 adantr 
 |-  ( ( ph /\ n e. NN ) -> ( (,) o. F ) : NN --> ~P RR )
86 ffn 
 |-  ( ( (,) o. F ) : NN --> ~P RR -> ( (,) o. F ) Fn NN )
87 fniunfv 
 |-  ( ( (,) o. F ) Fn NN -> U_ x e. NN ( ( (,) o. F ) ` x ) = U. ran ( (,) o. F ) )
88 85 86 87 3syl 
 |-  ( ( ph /\ n e. NN ) -> U_ x e. NN ( ( (,) o. F ) ` x ) = U. ran ( (,) o. F ) )
89 84 88 sseqtrd 
 |-  ( ( ph /\ n e. NN ) -> U_ x e. ( 1 ... n ) ( ( (,) o. F ) ` x ) C_ U. ran ( (,) o. F ) )
90 14 adantr 
 |-  ( ( ph /\ n e. NN ) -> U. ran ( (,) o. F ) C_ RR )
91 ovolss 
 |-  ( ( U_ x e. ( 1 ... n ) ( ( (,) o. F ) ` x ) C_ U. ran ( (,) o. F ) /\ U. ran ( (,) o. F ) C_ RR ) -> ( vol* ` U_ x e. ( 1 ... n ) ( ( (,) o. F ) ` x ) ) <_ ( vol* ` U. ran ( (,) o. F ) ) )
92 89 90 91 syl2anc 
 |-  ( ( ph /\ n e. NN ) -> ( vol* ` U_ x e. ( 1 ... n ) ( ( (,) o. F ) ` x ) ) <_ ( vol* ` U. ran ( (,) o. F ) ) )
93 82 92 eqbrtrd 
 |-  ( ( ph /\ n e. NN ) -> ( S ` n ) <_ ( vol* ` U. ran ( (,) o. F ) ) )
94 93 ralrimiva 
 |-  ( ph -> A. n e. NN ( S ` n ) <_ ( vol* ` U. ran ( (,) o. F ) ) )
95 1 18 syl 
 |-  ( ph -> S : NN --> ( 0 [,) +oo ) )
96 ffn 
 |-  ( S : NN --> ( 0 [,) +oo ) -> S Fn NN )
97 breq1 
 |-  ( y = ( S ` n ) -> ( y <_ ( vol* ` U. ran ( (,) o. F ) ) <-> ( S ` n ) <_ ( vol* ` U. ran ( (,) o. F ) ) ) )
98 97 ralrn 
 |-  ( S Fn NN -> ( A. y e. ran S y <_ ( vol* ` U. ran ( (,) o. F ) ) <-> A. n e. NN ( S ` n ) <_ ( vol* ` U. ran ( (,) o. F ) ) ) )
99 95 96 98 3syl 
 |-  ( ph -> ( A. y e. ran S y <_ ( vol* ` U. ran ( (,) o. F ) ) <-> A. n e. NN ( S ` n ) <_ ( vol* ` U. ran ( (,) o. F ) ) ) )
100 94 99 mpbird 
 |-  ( ph -> A. y e. ran S y <_ ( vol* ` U. ran ( (,) o. F ) ) )
101 supxrleub 
 |-  ( ( ran S C_ RR* /\ ( vol* ` U. ran ( (,) o. F ) ) e. RR* ) -> ( sup ( ran S , RR* , < ) <_ ( vol* ` U. ran ( (,) o. F ) ) <-> A. y e. ran S y <_ ( vol* ` U. ran ( (,) o. F ) ) ) )
102 22 16 101 syl2anc 
 |-  ( ph -> ( sup ( ran S , RR* , < ) <_ ( vol* ` U. ran ( (,) o. F ) ) <-> A. y e. ran S y <_ ( vol* ` U. ran ( (,) o. F ) ) ) )
103 100 102 mpbird 
 |-  ( ph -> sup ( ran S , RR* , < ) <_ ( vol* ` U. ran ( (,) o. F ) ) )
104 16 24 27 103 xrletrid 
 |-  ( ph -> ( vol* ` U. ran ( (,) o. F ) ) = sup ( ran S , RR* , < ) )