MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  uniioovol Unicode version

Theorem uniioovol 18882
Description: An 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 18859.) Lemma 565Ca of [Fremlin5] p. 213. (Contributed by Mario Carneiro, 26-Mar-2015.)
Hypotheses
Ref Expression
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
Ref Expression
uniioovol  |-  ( ph  ->  ( vol * `  U. ran  ( (,)  o.  F ) )  =  sup ( ran  S ,  RR* ,  <  )
)
Distinct variable groups:    x, F    ph, x
Allowed substitution hint:    S( x)

Proof of Theorem uniioovol
StepHypRef Expression
1 uniioombl.1 . . 3  |-  ( ph  ->  F : NN --> (  <_  i^i  ( RR  X.  RR ) ) )
2 ssid 3158 . . 3  |-  U. ran  ( (,)  o.  F ) 
C_  U. ran  ( (,) 
o.  F )
3 uniioombl.3 . . . 4  |-  S  =  seq  1 (  +  ,  ( ( abs 
o.  -  )  o.  F ) )
43ovollb 18786 . . 3  |-  ( ( 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* ,  <  )
)
51, 2, 4sylancl 646 . 2  |-  ( ph  ->  ( vol * `  U. ran  ( (,)  o.  F ) )  <_  sup ( ran  S ,  RR* ,  <  ) )
61adantr 453 . . . . . . . . . . 11  |-  ( (
ph  /\  n  e.  NN )  ->  F : NN
--> (  <_  i^i  ( RR  X.  RR ) ) )
7 elfznn 10771 . . . . . . . . . . 11  |-  ( x  e.  ( 1 ... n )  ->  x  e.  NN )
8 eqid 2256 . . . . . . . . . . . 12  |-  ( ( abs  o.  -  )  o.  F )  =  ( ( abs  o.  -  )  o.  F )
98ovolfsval 18778 . . . . . . . . . . 11  |-  ( ( F : NN --> (  <_  i^i  ( RR  X.  RR ) )  /\  x  e.  NN )  ->  (
( ( abs  o.  -  )  o.  F
) `  x )  =  ( ( 2nd `  ( F `  x
) )  -  ( 1st `  ( F `  x ) ) ) )
106, 7, 9syl2an 465 . . . . . . . . . 10  |-  ( ( ( ph  /\  n  e.  NN )  /\  x  e.  ( 1 ... n
) )  ->  (
( ( abs  o.  -  )  o.  F
) `  x )  =  ( ( 2nd `  ( F `  x
) )  -  ( 1st `  ( F `  x ) ) ) )
11 fvco3 5516 . . . . . . . . . . . . . . 15  |-  ( ( F : NN --> (  <_  i^i  ( RR  X.  RR ) )  /\  x  e.  NN )  ->  (
( (,)  o.  F
) `  x )  =  ( (,) `  ( F `  x )
) )
126, 7, 11syl2an 465 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  n  e.  NN )  /\  x  e.  ( 1 ... n
) )  ->  (
( (,)  o.  F
) `  x )  =  ( (,) `  ( F `  x )
) )
13 inss2 3351 . . . . . . . . . . . . . . . . . 18  |-  (  <_  i^i  ( RR  X.  RR ) )  C_  ( RR  X.  RR )
14 ffvelrn 5583 . . . . . . . . . . . . . . . . . . 19  |-  ( ( F : NN --> (  <_  i^i  ( RR  X.  RR ) )  /\  x  e.  NN )  ->  ( F `  x )  e.  (  <_  i^i  ( RR  X.  RR ) ) )
156, 7, 14syl2an 465 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  n  e.  NN )  /\  x  e.  ( 1 ... n
) )  ->  ( F `  x )  e.  (  <_  i^i  ( RR  X.  RR ) ) )
1613, 15sseldi 3139 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  n  e.  NN )  /\  x  e.  ( 1 ... n
) )  ->  ( F `  x )  e.  ( RR  X.  RR ) )
17 1st2nd2 6079 . . . . . . . . . . . . . . . . 17  |-  ( ( F `  x )  e.  ( RR  X.  RR )  ->  ( F `
 x )  = 
<. ( 1st `  ( F `  x )
) ,  ( 2nd `  ( F `  x
) ) >. )
1816, 17syl 17 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  n  e.  NN )  /\  x  e.  ( 1 ... n
) )  ->  ( F `  x )  =  <. ( 1st `  ( F `  x )
) ,  ( 2nd `  ( F `  x
) ) >. )
1918fveq2d 5448 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  n  e.  NN )  /\  x  e.  ( 1 ... n
) )  ->  ( (,) `  ( F `  x ) )  =  ( (,) `  <. ( 1st `  ( F `
 x ) ) ,  ( 2nd `  ( F `  x )
) >. ) )
20 df-ov 5781 . . . . . . . . . . . . . . 15  |-  ( ( 1st `  ( F `
 x ) ) (,) ( 2nd `  ( F `  x )
) )  =  ( (,) `  <. ( 1st `  ( F `  x ) ) ,  ( 2nd `  ( F `  x )
) >. )
2119, 20syl6eqr 2306 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  n  e.  NN )  /\  x  e.  ( 1 ... n
) )  ->  ( (,) `  ( F `  x ) )  =  ( ( 1st `  ( F `  x )
) (,) ( 2nd `  ( F `  x
) ) ) )
2212, 21eqtrd 2288 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  n  e.  NN )  /\  x  e.  ( 1 ... n
) )  ->  (
( (,)  o.  F
) `  x )  =  ( ( 1st `  ( F `  x
) ) (,) ( 2nd `  ( F `  x ) ) ) )
23 ioombl 18870 . . . . . . . . . . . . 13  |-  ( ( 1st `  ( F `
 x ) ) (,) ( 2nd `  ( F `  x )
) )  e.  dom  vol
2422, 23syl6eqel 2344 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  n  e.  NN )  /\  x  e.  ( 1 ... n
) )  ->  (
( (,)  o.  F
) `  x )  e.  dom  vol )
25 mblvol 18837 . . . . . . . . . . . 12  |-  ( ( ( (,)  o.  F
) `  x )  e.  dom  vol  ->  ( vol `  ( ( (,)  o.  F ) `  x
) )  =  ( vol * `  (
( (,)  o.  F
) `  x )
) )
2624, 25syl 17 . . . . . . . . . . 11  |-  ( ( ( ph  /\  n  e.  NN )  /\  x  e.  ( 1 ... n
) )  ->  ( vol `  ( ( (,) 
o.  F ) `  x ) )  =  ( vol * `  ( ( (,)  o.  F ) `  x
) ) )
2722fveq2d 5448 . . . . . . . . . . 11  |-  ( ( ( ph  /\  n  e.  NN )  /\  x  e.  ( 1 ... n
) )  ->  ( vol * `  ( ( (,)  o.  F ) `
 x ) )  =  ( vol * `  ( ( 1st `  ( F `  x )
) (,) ( 2nd `  ( F `  x
) ) ) ) )
28 ovolfcl 18774 . . . . . . . . . . . . 13  |-  ( ( 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 )
) ) )
296, 7, 28syl2an 465 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  n  e.  NN )  /\  x  e.  ( 1 ... n
) )  ->  (
( 1st `  ( F `  x )
)  e.  RR  /\  ( 2nd `  ( F `
 x ) )  e.  RR  /\  ( 1st `  ( F `  x ) )  <_ 
( 2nd `  ( F `  x )
) ) )
30 ovolioo 18873 . . . . . . . . . . . 12  |-  ( ( ( 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
) ) ) )
3129, 30syl 17 . . . . . . . . . . 11  |-  ( ( ( ph  /\  n  e.  NN )  /\  x  e.  ( 1 ... n
) )  ->  ( vol * `  ( ( 1st `  ( F `
 x ) ) (,) ( 2nd `  ( F `  x )
) ) )  =  ( ( 2nd `  ( F `  x )
)  -  ( 1st `  ( F `  x
) ) ) )
3226, 27, 313eqtrd 2292 . . . . . . . . . 10  |-  ( ( ( ph  /\  n  e.  NN )  /\  x  e.  ( 1 ... n
) )  ->  ( vol `  ( ( (,) 
o.  F ) `  x ) )  =  ( ( 2nd `  ( F `  x )
)  -  ( 1st `  ( F `  x
) ) ) )
3310, 32eqtr4d 2291 . . . . . . . . 9  |-  ( ( ( ph  /\  n  e.  NN )  /\  x  e.  ( 1 ... n
) )  ->  (
( ( abs  o.  -  )  o.  F
) `  x )  =  ( vol `  (
( (,)  o.  F
) `  x )
) )
34 simpr 449 . . . . . . . . . 10  |-  ( (
ph  /\  n  e.  NN )  ->  n  e.  NN )
35 nnuz 10216 . . . . . . . . . 10  |-  NN  =  ( ZZ>= `  1 )
3634, 35syl6eleq 2346 . . . . . . . . 9  |-  ( (
ph  /\  n  e.  NN )  ->  n  e.  ( ZZ>= `  1 )
)
3729simp2d 973 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  n  e.  NN )  /\  x  e.  ( 1 ... n
) )  ->  ( 2nd `  ( F `  x ) )  e.  RR )
3829simp1d 972 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  n  e.  NN )  /\  x  e.  ( 1 ... n
) )  ->  ( 1st `  ( F `  x ) )  e.  RR )
3937, 38resubcld 9165 . . . . . . . . . . 11  |-  ( ( ( ph  /\  n  e.  NN )  /\  x  e.  ( 1 ... n
) )  ->  (
( 2nd `  ( F `  x )
)  -  ( 1st `  ( F `  x
) ) )  e.  RR )
4032, 39eqeltrd 2330 . . . . . . . . . 10  |-  ( ( ( ph  /\  n  e.  NN )  /\  x  e.  ( 1 ... n
) )  ->  ( vol `  ( ( (,) 
o.  F ) `  x ) )  e.  RR )
4140recnd 8815 . . . . . . . . 9  |-  ( ( ( ph  /\  n  e.  NN )  /\  x  e.  ( 1 ... n
) )  ->  ( vol `  ( ( (,) 
o.  F ) `  x ) )  e.  CC )
4233, 36, 41fsumser 12154 . . . . . . . 8  |-  ( (
ph  /\  n  e.  NN )  ->  sum_ x  e.  ( 1 ... n
) ( vol `  (
( (,)  o.  F
) `  x )
)  =  (  seq  1 (  +  , 
( ( abs  o.  -  )  o.  F
) ) `  n
) )
433fveq1i 5445 . . . . . . . 8  |-  ( S `
 n )  =  (  seq  1 (  +  ,  ( ( abs  o.  -  )  o.  F ) ) `  n )
4442, 43syl6reqr 2307 . . . . . . 7  |-  ( (
ph  /\  n  e.  NN )  ->  ( S `
 n )  = 
sum_ x  e.  (
1 ... n ) ( vol `  ( ( (,)  o.  F ) `
 x ) ) )
45 fzfid 10987 . . . . . . . 8  |-  ( (
ph  /\  n  e.  NN )  ->  ( 1 ... n )  e. 
Fin )
4624, 40jca 520 . . . . . . . . 9  |-  ( ( ( ph  /\  n  e.  NN )  /\  x  e.  ( 1 ... n
) )  ->  (
( ( (,)  o.  F ) `  x
)  e.  dom  vol  /\  ( vol `  (
( (,)  o.  F
) `  x )
)  e.  RR ) )
4746ralrimiva 2599 . . . . . . . 8  |-  ( (
ph  /\  n  e.  NN )  ->  A. x  e.  ( 1 ... n
) ( ( ( (,)  o.  F ) `
 x )  e. 
dom  vol  /\  ( vol `  ( ( (,)  o.  F ) `  x
) )  e.  RR ) )
487ssriv 3145 . . . . . . . . 9  |-  ( 1 ... n )  C_  NN
49 uniioombl.2 . . . . . . . . . . 11  |-  ( ph  -> Disj  x  e.  NN ( (,) `  ( F `  x ) ) )
501, 11sylan 459 . . . . . . . . . . . 12  |-  ( (
ph  /\  x  e.  NN )  ->  ( ( (,)  o.  F ) `
 x )  =  ( (,) `  ( F `  x )
) )
5150disjeq2dv 3958 . . . . . . . . . . 11  |-  ( ph  ->  (Disj  x  e.  NN ( ( (,)  o.  F ) `  x
)  <-> Disj  x  e.  NN ( (,) `  ( F `
 x ) ) ) )
5249, 51mpbird 225 . . . . . . . . . 10  |-  ( ph  -> Disj  x  e.  NN (
( (,)  o.  F
) `  x )
)
5352adantr 453 . . . . . . . . 9  |-  ( (
ph  /\  n  e.  NN )  -> Disj  x  e.  NN ( ( (,)  o.  F ) `  x
) )
54 disjss1 3959 . . . . . . . . 9  |-  ( ( 1 ... n ) 
C_  NN  ->  (Disj  x  e.  NN ( ( (,) 
o.  F ) `  x )  -> Disj  x  e.  ( 1 ... n
) ( ( (,) 
o.  F ) `  x ) ) )
5548, 53, 54mpsyl 61 . . . . . . . 8  |-  ( (
ph  /\  n  e.  NN )  -> Disj  x  e.  ( 1 ... n
) ( ( (,) 
o.  F ) `  x ) )
56 volfiniun 18852 . . . . . . . 8  |-  ( ( ( 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
) ) )
5745, 47, 55, 56syl3anc 1187 . . . . . . 7  |-  ( (
ph  /\  n  e.  NN )  ->  ( vol `  U_ x  e.  ( 1 ... n ) ( ( (,)  o.  F ) `  x
) )  =  sum_ x  e.  ( 1 ... n ) ( vol `  ( ( (,)  o.  F ) `  x
) ) )
5824ralrimiva 2599 . . . . . . . . 9  |-  ( (
ph  /\  n  e.  NN )  ->  A. x  e.  ( 1 ... n
) ( ( (,) 
o.  F ) `  x )  e.  dom  vol )
59 finiunmbl 18849 . . . . . . . . 9  |-  ( ( ( 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 )
6045, 58, 59syl2anc 645 . . . . . . . 8  |-  ( (
ph  /\  n  e.  NN )  ->  U_ x  e.  ( 1 ... n
) ( ( (,) 
o.  F ) `  x )  e.  dom  vol )
61 mblvol 18837 . . . . . . . 8  |-  ( 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 ) ) )
6260, 61syl 17 . . . . . . 7  |-  ( (
ph  /\  n  e.  NN )  ->  ( vol `  U_ x  e.  ( 1 ... n ) ( ( (,)  o.  F ) `  x
) )  =  ( vol * `  U_ x  e.  ( 1 ... n
) ( ( (,) 
o.  F ) `  x ) ) )
6344, 57, 623eqtr2d 2294 . . . . . 6  |-  ( (
ph  /\  n  e.  NN )  ->  ( S `
 n )  =  ( vol * `  U_ x  e.  ( 1 ... n ) ( ( (,)  o.  F
) `  x )
) )
64 iunss1 3876 . . . . . . . . 9  |-  ( ( 1 ... n ) 
C_  NN  ->  U_ x  e.  ( 1 ... n
) ( ( (,) 
o.  F ) `  x )  C_  U_ x  e.  NN  ( ( (,) 
o.  F ) `  x ) )
6548, 64mp1i 13 . . . . . . . 8  |-  ( (
ph  /\  n  e.  NN )  ->  U_ x  e.  ( 1 ... n
) ( ( (,) 
o.  F ) `  x )  C_  U_ x  e.  NN  ( ( (,) 
o.  F ) `  x ) )
66 ioof 10693 . . . . . . . . . . 11  |-  (,) :
( RR*  X.  RR* ) --> ~P RR
67 ressxr 8830 . . . . . . . . . . . . . 14  |-  RR  C_  RR*
68 xpss12 4766 . . . . . . . . . . . . . 14  |-  ( ( RR  C_  RR*  /\  RR  C_ 
RR* )  ->  ( RR  X.  RR )  C_  ( RR*  X.  RR* )
)
6967, 67, 68mp2an 656 . . . . . . . . . . . . 13  |-  ( RR 
X.  RR )  C_  ( RR*  X.  RR* )
7013, 69sstri 3149 . . . . . . . . . . . 12  |-  (  <_  i^i  ( RR  X.  RR ) )  C_  ( RR*  X.  RR* )
71 fss 5321 . . . . . . . . . . . 12  |-  ( ( F : NN --> (  <_  i^i  ( RR  X.  RR ) )  /\  (  <_  i^i  ( RR  X.  RR ) )  C_  ( RR*  X.  RR* ) )  ->  F : NN --> ( RR*  X. 
RR* ) )
721, 70, 71sylancl 646 . . . . . . . . . . 11  |-  ( ph  ->  F : NN --> ( RR*  X. 
RR* ) )
73 fco 5322 . . . . . . . . . . 11  |-  ( ( (,) : ( RR*  X. 
RR* ) --> ~P RR  /\  F : NN --> ( RR*  X. 
RR* ) )  -> 
( (,)  o.  F
) : NN --> ~P RR )
7466, 72, 73sylancr 647 . . . . . . . . . 10  |-  ( ph  ->  ( (,)  o.  F
) : NN --> ~P RR )
7574adantr 453 . . . . . . . . 9  |-  ( (
ph  /\  n  e.  NN )  ->  ( (,) 
o.  F ) : NN --> ~P RR )
76 ffn 5313 . . . . . . . . 9  |-  ( ( (,)  o.  F ) : NN --> ~P RR  ->  ( (,)  o.  F
)  Fn  NN )
77 fniunfv 5693 . . . . . . . . 9  |-  ( ( (,)  o.  F )  Fn  NN  ->  U_ x  e.  NN  ( ( (,) 
o.  F ) `  x )  =  U. ran  ( (,)  o.  F
) )
7875, 76, 773syl 20 . . . . . . . 8  |-  ( (
ph  /\  n  e.  NN )  ->  U_ x  e.  NN  ( ( (,) 
o.  F ) `  x )  =  U. ran  ( (,)  o.  F
) )
7965, 78sseqtrd 3175 . . . . . . 7  |-  ( (
ph  /\  n  e.  NN )  ->  U_ x  e.  ( 1 ... n
) ( ( (,) 
o.  F ) `  x )  C_  U. ran  ( (,)  o.  F ) )
80 frn 5319 . . . . . . . . . 10  |-  ( ( (,)  o.  F ) : NN --> ~P RR  ->  ran  ( (,)  o.  F )  C_  ~P RR )
8174, 80syl 17 . . . . . . . . 9  |-  ( ph  ->  ran  ( (,)  o.  F )  C_  ~P RR )
82 sspwuni 3947 . . . . . . . . 9  |-  ( ran  ( (,)  o.  F
)  C_  ~P RR  <->  U.
ran  ( (,)  o.  F )  C_  RR )
8381, 82sylib 190 . . . . . . . 8  |-  ( ph  ->  U. ran  ( (,) 
o.  F )  C_  RR )
8483adantr 453 . . . . . . 7  |-  ( (
ph  /\  n  e.  NN )  ->  U. ran  ( (,)  o.  F ) 
C_  RR )
85 ovolss 18792 . . . . . . 7  |-  ( (
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 ) ) )
8679, 84, 85syl2anc 645 . . . . . 6  |-  ( (
ph  /\  n  e.  NN )  ->  ( vol
* `  U_ x  e.  ( 1 ... n
) ( ( (,) 
o.  F ) `  x ) )  <_ 
( vol * `  U. ran  ( (,)  o.  F ) ) )
8763, 86eqbrtrd 4003 . . . . 5  |-  ( (
ph  /\  n  e.  NN )  ->  ( S `
 n )  <_ 
( vol * `  U. ran  ( (,)  o.  F ) ) )
8887ralrimiva 2599 . . . 4  |-  ( ph  ->  A. n  e.  NN  ( S `  n )  <_  ( vol * `  U. ran  ( (,) 
o.  F ) ) )
898, 3ovolsf 18780 . . . . . 6  |-  ( F : NN --> (  <_  i^i  ( RR  X.  RR ) )  ->  S : NN --> ( 0 [,) 
+oo ) )
901, 89syl 17 . . . . 5  |-  ( ph  ->  S : NN --> ( 0 [,)  +oo ) )
91 ffn 5313 . . . . 5  |-  ( S : NN --> ( 0 [,)  +oo )  ->  S  Fn  NN )
92 breq1 3986 . . . . . 6  |-  ( y  =  ( S `  n )  ->  (
y  <_  ( vol * `
 U. ran  ( (,)  o.  F ) )  <-> 
( S `  n
)  <_  ( vol * `
 U. ran  ( (,)  o.  F ) ) ) )
9392ralrn 5588 . . . . 5  |-  ( 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 ) ) ) )
9490, 91, 933syl 20 . . . 4  |-  ( ph  ->  ( A. y  e. 
ran  S  y  <_  ( vol * `  U. ran  ( (,)  o.  F
) )  <->  A. n  e.  NN  ( S `  n )  <_  ( vol * `  U. ran  ( (,)  o.  F ) ) ) )
9588, 94mpbird 225 . . 3  |-  ( ph  ->  A. y  e.  ran  S  y  <_  ( vol * `
 U. ran  ( (,)  o.  F ) ) )
96 frn 5319 . . . . . 6  |-  ( S : NN --> ( 0 [,)  +oo )  ->  ran  S 
C_  ( 0 [,) 
+oo ) )
971, 89, 963syl 20 . . . . 5  |-  ( ph  ->  ran  S  C_  (
0 [,)  +oo ) )
98 icossxr 10686 . . . . 5  |-  ( 0 [,)  +oo )  C_  RR*
9997, 98syl6ss 3152 . . . 4  |-  ( ph  ->  ran  S  C_  RR* )
100 ovolcl 18785 . . . . 5  |-  ( U. ran  ( (,)  o.  F
)  C_  RR  ->  ( vol * `  U. ran  ( (,)  o.  F
) )  e.  RR* )
10183, 100syl 17 . . . 4  |-  ( ph  ->  ( vol * `  U. ran  ( (,)  o.  F ) )  e. 
RR* )
102 supxrleub 10597 . . . 4  |-  ( ( 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 ) ) ) )
10399, 101, 102syl2anc 645 . . 3  |-  ( ph  ->  ( sup ( ran 
S ,  RR* ,  <  )  <_  ( vol * `  U. ran  ( (,) 
o.  F ) )  <->  A. y  e.  ran  S  y  <_  ( vol * `
 U. ran  ( (,)  o.  F ) ) ) )
10495, 103mpbird 225 . 2  |-  ( ph  ->  sup ( ran  S ,  RR* ,  <  )  <_  ( vol * `  U. ran  ( (,)  o.  F ) ) )
105 supxrcl 10585 . . . 4  |-  ( ran 
S  C_  RR*  ->  sup ( ran  S ,  RR* ,  <  )  e.  RR* )
10699, 105syl 17 . . 3  |-  ( ph  ->  sup ( ran  S ,  RR* ,  <  )  e.  RR* )
107 xrletri3 10439 . . 3  |-  ( ( ( vol * `  U. ran  ( (,)  o.  F ) )  e. 
RR*  /\  sup ( ran  S ,  RR* ,  <  )  e.  RR* )  ->  (
( vol * `  U. ran  ( (,)  o.  F ) )  =  sup ( ran  S ,  RR* ,  <  )  <->  ( ( vol * `  U. ran  ( (,)  o.  F ) )  <_  sup ( ran  S ,  RR* ,  <  )  /\  sup ( ran  S ,  RR* ,  <  )  <_ 
( vol * `  U. ran  ( (,)  o.  F ) ) ) ) )
108101, 106, 107syl2anc 645 . 2  |-  ( ph  ->  ( ( vol * `  U. ran  ( (,) 
o.  F ) )  =  sup ( ran 
S ,  RR* ,  <  )  <-> 
( ( vol * `  U. ran  ( (,) 
o.  F ) )  <_  sup ( ran  S ,  RR* ,  <  )  /\  sup ( ran  S ,  RR* ,  <  )  <_  ( vol * `  U. ran  ( (,)  o.  F ) ) ) ) )
1095, 104, 108mpbir2and 893 1  |-  ( ph  ->  ( vol * `  U. ran  ( (,)  o.  F ) )  =  sup ( ran  S ,  RR* ,  <  )
)
Colors of variables: wff set class
Syntax hints:    -> wi 6    <-> wb 178    /\ wa 360    /\ w3a 939    = wceq 1619    e. wcel 1621   A.wral 2516    i^i cin 3112    C_ wss 3113   ~Pcpw 3585   <.cop 3603   U.cuni 3787   U_ciun 3865  Disj wdisj 3953   class class class wbr 3983    X. cxp 4645   dom cdm 4647   ran crn 4648    o. ccom 4651    Fn wfn 4654   -->wf 4655   ` cfv 4659  (class class class)co 5778   1stc1st 6040   2ndc2nd 6041   Fincfn 6817   supcsup 7147   RRcr 8690   0cc0 8691   1c1 8692    + caddc 8694    +oocpnf 8818   RR*cxr 8820    < clt 8821    <_ cle 8822    - cmin 8991   NNcn 9700   ZZ>=cuz 10183   (,)cioo 10608   [,)cico 10610   ...cfz 10734    seq cseq 10998   abscabs 11670   sum_csu 12109   vol
*covol 18770   volcvol 18771
This theorem is referenced by:  uniiccvol  18883  uniioombllem2  18886
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-6 1534  ax-7 1535  ax-gen 1536  ax-8 1623  ax-11 1624  ax-13 1625  ax-14 1626  ax-17 1628  ax-12o 1664  ax-10 1678  ax-9 1684  ax-4 1692  ax-16 1927  ax-ext 2237  ax-rep 4091  ax-sep 4101  ax-nul 4109  ax-pow 4146  ax-pr 4172  ax-un 4470  ax-inf2 7296  ax-cnex 8747  ax-resscn 8748  ax-1cn 8749  ax-icn 8750  ax-addcl 8751  ax-addrcl 8752  ax-mulcl 8753  ax-mulrcl 8754  ax-mulcom 8755  ax-addass 8756  ax-mulass 8757  ax-distr 8758  ax-i2m1 8759  ax-1ne0 8760  ax-1rid 8761  ax-rnegex 8762  ax-rrecex 8763  ax-cnre 8764  ax-pre-lttri 8765  ax-pre-lttrn 8766  ax-pre-ltadd 8767  ax-pre-mulgt0 8768  ax-pre-sup 8769
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3or 940  df-3an 941  df-tru 1315  df-ex 1538  df-nf 1540  df-sb 1884  df-eu 2121  df-mo 2122  df-clab 2243  df-cleq 2249  df-clel 2252  df-nfc 2381  df-ne 2421  df-nel 2422  df-ral 2521  df-rex 2522  df-reu 2523  df-rmo 2524  df-rab 2525  df-v 2759  df-sbc 2953  df-csb 3043  df-dif 3116  df-un 3118  df-in 3120  df-ss 3127  df-pss 3129  df-nul 3417  df-if 3526  df-pw 3587  df-sn 3606  df-pr 3607  df-tp 3608  df-op 3609  df-uni 3788  df-int 3823  df-iun 3867  df-disj 3954  df-br 3984  df-opab 4038  df-mpt 4039  df-tr 4074  df-eprel 4263  df-id 4267  df-po 4272  df-so 4273  df-fr 4310  df-se 4311  df-we 4312  df-ord 4353  df-on 4354  df-lim 4355  df-suc 4356  df-om 4615  df-xp 4661  df-rel 4662  df-cnv 4663  df-co 4664  df-dm 4665  df-rn 4666  df-res 4667  df-ima 4668  df-fun 4669  df-fn 4670  df-f 4671  df-f1 4672  df-fo 4673  df-f1o 4674  df-fv 4675  df-isom 4676  df-ov 5781  df-oprab 5782  df-mpt2 5783  df-of 5998  df-1st 6042  df-2nd 6043  df-iota 6211  df-riota 6258  df-recs 6342  df-rdg 6377  df-1o 6433  df-2o 6434  df-oadd 6437  df-er 6614  df-map 6728  df-pm 6729  df-en 6818  df-dom 6819  df-sdom 6820  df-fin 6821  df-fi 7119  df-sup 7148  df-oi 7179  df-card 7526  df-cda 7748  df-pnf 8823  df-mnf 8824  df-xr 8825  df-ltxr 8826  df-le 8827  df-sub 8993  df-neg 8994  df-div 9378  df-n 9701  df-2 9758  df-3 9759  df-n0 9919  df-z 9978  df-uz 10184  df-q 10270  df-rp 10308  df-xneg 10405  df-xadd 10406  df-xmul 10407  df-ioo 10612  df-ico 10614  df-icc 10615  df-fz 10735  df-fzo 10823  df-fl 10877  df-seq 10999  df-exp 11057  df-hash 11290  df-cj 11535  df-re 11536  df-im 11537  df-sqr 11671  df-abs 11672  df-clim 11913  df-rlim 11914  df-sum 12110  df-rest 13275  df-topgen 13292  df-xmet 16321  df-met 16322  df-bl 16323  df-mopn 16324  df-top 16584  df-bases 16586  df-topon 16587  df-cmp 17062  df-ovol 18772  df-vol 18773
  Copyright terms: Public domain W3C validator