Metamath Proof Explorer

Theorem uniioombllem2a

Description: Lemma for uniioombl . (Contributed by Mario Carneiro, 7-May-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 ) )
uniioombl.a 
|- A = U. ran ( (,) o. F )
uniioombl.e 
|- ( ph -> ( vol* ` E ) e. RR )
uniioombl.c 
|- ( ph -> C e. RR+ )
uniioombl.g 
|- ( ph -> G : NN --> ( <_ i^i ( RR X. RR ) ) )
uniioombl.s 
|- ( ph -> E C_ U. ran ( (,) o. G ) )
uniioombl.t 
|- T = seq 1 ( + , ( ( abs o. - ) o. G ) )
uniioombl.v 
|- ( ph -> sup ( ran T , RR* , < ) <_ ( ( vol* ` E ) + C ) )
Assertion uniioombllem2a 
|- ( ( ( ph /\ J e. NN ) /\ z e. NN ) -> ( ( (,) ` ( F ` z ) ) i^i ( (,) ` ( G ` J ) ) ) e. ran (,) )

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 uniioombl.a 
 |-  A = U. ran ( (,) o. F )
5 uniioombl.e 
 |-  ( ph -> ( vol* ` E ) e. RR )
6 uniioombl.c 
 |-  ( ph -> C e. RR+ )
7 uniioombl.g 
 |-  ( ph -> G : NN --> ( <_ i^i ( RR X. RR ) ) )
8 uniioombl.s 
 |-  ( ph -> E C_ U. ran ( (,) o. G ) )
9 uniioombl.t 
 |-  T = seq 1 ( + , ( ( abs o. - ) o. G ) )
10 uniioombl.v 
 |-  ( ph -> sup ( ran T , RR* , < ) <_ ( ( vol* ` E ) + C ) )
11 1 adantr 
 |-  ( ( ph /\ J e. NN ) -> F : NN --> ( <_ i^i ( RR X. RR ) ) )
12 11 ffvelrnda 
 |-  ( ( ( ph /\ J e. NN ) /\ z e. NN ) -> ( F ` z ) e. ( <_ i^i ( RR X. RR ) ) )
13 12 elin2d 
 |-  ( ( ( ph /\ J e. NN ) /\ z e. NN ) -> ( F ` z ) e. ( RR X. RR ) )
14 1st2nd2 
 |-  ( ( F ` z ) e. ( RR X. RR ) -> ( F ` z ) = <. ( 1st ` ( F ` z ) ) , ( 2nd ` ( F ` z ) ) >. )
15 13 14 syl 
 |-  ( ( ( ph /\ J e. NN ) /\ z e. NN ) -> ( F ` z ) = <. ( 1st ` ( F ` z ) ) , ( 2nd ` ( F ` z ) ) >. )
16 15 fveq2d 
 |-  ( ( ( ph /\ J e. NN ) /\ z e. NN ) -> ( (,) ` ( F ` z ) ) = ( (,) ` <. ( 1st ` ( F ` z ) ) , ( 2nd ` ( F ` z ) ) >. ) )
17 df-ov 
 |-  ( ( 1st ` ( F ` z ) ) (,) ( 2nd ` ( F ` z ) ) ) = ( (,) ` <. ( 1st ` ( F ` z ) ) , ( 2nd ` ( F ` z ) ) >. )
18 16 17 eqtr4di 
 |-  ( ( ( ph /\ J e. NN ) /\ z e. NN ) -> ( (,) ` ( F ` z ) ) = ( ( 1st ` ( F ` z ) ) (,) ( 2nd ` ( F ` z ) ) ) )
19 7 ffvelrnda 
 |-  ( ( ph /\ J e. NN ) -> ( G ` J ) e. ( <_ i^i ( RR X. RR ) ) )
20 19 elin2d 
 |-  ( ( ph /\ J e. NN ) -> ( G ` J ) e. ( RR X. RR ) )
21 1st2nd2 
 |-  ( ( G ` J ) e. ( RR X. RR ) -> ( G ` J ) = <. ( 1st ` ( G ` J ) ) , ( 2nd ` ( G ` J ) ) >. )
22 20 21 syl 
 |-  ( ( ph /\ J e. NN ) -> ( G ` J ) = <. ( 1st ` ( G ` J ) ) , ( 2nd ` ( G ` J ) ) >. )
23 22 fveq2d 
 |-  ( ( ph /\ J e. NN ) -> ( (,) ` ( G ` J ) ) = ( (,) ` <. ( 1st ` ( G ` J ) ) , ( 2nd ` ( G ` J ) ) >. ) )
24 df-ov 
 |-  ( ( 1st ` ( G ` J ) ) (,) ( 2nd ` ( G ` J ) ) ) = ( (,) ` <. ( 1st ` ( G ` J ) ) , ( 2nd ` ( G ` J ) ) >. )
25 23 24 eqtr4di 
 |-  ( ( ph /\ J e. NN ) -> ( (,) ` ( G ` J ) ) = ( ( 1st ` ( G ` J ) ) (,) ( 2nd ` ( G ` J ) ) ) )
26 25 adantr 
 |-  ( ( ( ph /\ J e. NN ) /\ z e. NN ) -> ( (,) ` ( G ` J ) ) = ( ( 1st ` ( G ` J ) ) (,) ( 2nd ` ( G ` J ) ) ) )
27 18 26 ineq12d 
 |-  ( ( ( ph /\ J e. NN ) /\ z e. NN ) -> ( ( (,) ` ( F ` z ) ) i^i ( (,) ` ( G ` J ) ) ) = ( ( ( 1st ` ( F ` z ) ) (,) ( 2nd ` ( F ` z ) ) ) i^i ( ( 1st ` ( G ` J ) ) (,) ( 2nd ` ( G ` J ) ) ) ) )
28 ovolfcl 
 |-  ( ( F : NN --> ( <_ i^i ( RR X. RR ) ) /\ z e. NN ) -> ( ( 1st ` ( F ` z ) ) e. RR /\ ( 2nd ` ( F ` z ) ) e. RR /\ ( 1st ` ( F ` z ) ) <_ ( 2nd ` ( F ` z ) ) ) )
29 11 28 sylan 
 |-  ( ( ( ph /\ J e. NN ) /\ z e. NN ) -> ( ( 1st ` ( F ` z ) ) e. RR /\ ( 2nd ` ( F ` z ) ) e. RR /\ ( 1st ` ( F ` z ) ) <_ ( 2nd ` ( F ` z ) ) ) )
30 29 simp1d 
 |-  ( ( ( ph /\ J e. NN ) /\ z e. NN ) -> ( 1st ` ( F ` z ) ) e. RR )
31 30 rexrd 
 |-  ( ( ( ph /\ J e. NN ) /\ z e. NN ) -> ( 1st ` ( F ` z ) ) e. RR* )
32 29 simp2d 
 |-  ( ( ( ph /\ J e. NN ) /\ z e. NN ) -> ( 2nd ` ( F ` z ) ) e. RR )
33 32 rexrd 
 |-  ( ( ( ph /\ J e. NN ) /\ z e. NN ) -> ( 2nd ` ( F ` z ) ) e. RR* )
34 ovolfcl 
 |-  ( ( G : NN --> ( <_ i^i ( RR X. RR ) ) /\ J e. NN ) -> ( ( 1st ` ( G ` J ) ) e. RR /\ ( 2nd ` ( G ` J ) ) e. RR /\ ( 1st ` ( G ` J ) ) <_ ( 2nd ` ( G ` J ) ) ) )
35 7 34 sylan 
 |-  ( ( ph /\ J e. NN ) -> ( ( 1st ` ( G ` J ) ) e. RR /\ ( 2nd ` ( G ` J ) ) e. RR /\ ( 1st ` ( G ` J ) ) <_ ( 2nd ` ( G ` J ) ) ) )
36 35 simp1d 
 |-  ( ( ph /\ J e. NN ) -> ( 1st ` ( G ` J ) ) e. RR )
37 36 rexrd 
 |-  ( ( ph /\ J e. NN ) -> ( 1st ` ( G ` J ) ) e. RR* )
38 37 adantr 
 |-  ( ( ( ph /\ J e. NN ) /\ z e. NN ) -> ( 1st ` ( G ` J ) ) e. RR* )
39 35 simp2d 
 |-  ( ( ph /\ J e. NN ) -> ( 2nd ` ( G ` J ) ) e. RR )
40 39 rexrd 
 |-  ( ( ph /\ J e. NN ) -> ( 2nd ` ( G ` J ) ) e. RR* )
41 40 adantr 
 |-  ( ( ( ph /\ J e. NN ) /\ z e. NN ) -> ( 2nd ` ( G ` J ) ) e. RR* )
42 iooin 
 |-  ( ( ( ( 1st ` ( F ` z ) ) e. RR* /\ ( 2nd ` ( F ` z ) ) e. RR* ) /\ ( ( 1st ` ( G ` J ) ) e. RR* /\ ( 2nd ` ( G ` J ) ) e. RR* ) ) -> ( ( ( 1st ` ( F ` z ) ) (,) ( 2nd ` ( F ` z ) ) ) i^i ( ( 1st ` ( G ` J ) ) (,) ( 2nd ` ( G ` J ) ) ) ) = ( if ( ( 1st ` ( F ` z ) ) <_ ( 1st ` ( G ` J ) ) , ( 1st ` ( G ` J ) ) , ( 1st ` ( F ` z ) ) ) (,) if ( ( 2nd ` ( F ` z ) ) <_ ( 2nd ` ( G ` J ) ) , ( 2nd ` ( F ` z ) ) , ( 2nd ` ( G ` J ) ) ) ) )
43 31 33 38 41 42 syl22anc 
 |-  ( ( ( ph /\ J e. NN ) /\ z e. NN ) -> ( ( ( 1st ` ( F ` z ) ) (,) ( 2nd ` ( F ` z ) ) ) i^i ( ( 1st ` ( G ` J ) ) (,) ( 2nd ` ( G ` J ) ) ) ) = ( if ( ( 1st ` ( F ` z ) ) <_ ( 1st ` ( G ` J ) ) , ( 1st ` ( G ` J ) ) , ( 1st ` ( F ` z ) ) ) (,) if ( ( 2nd ` ( F ` z ) ) <_ ( 2nd ` ( G ` J ) ) , ( 2nd ` ( F ` z ) ) , ( 2nd ` ( G ` J ) ) ) ) )
44 27 43 eqtrd 
 |-  ( ( ( ph /\ J e. NN ) /\ z e. NN ) -> ( ( (,) ` ( F ` z ) ) i^i ( (,) ` ( G ` J ) ) ) = ( if ( ( 1st ` ( F ` z ) ) <_ ( 1st ` ( G ` J ) ) , ( 1st ` ( G ` J ) ) , ( 1st ` ( F ` z ) ) ) (,) if ( ( 2nd ` ( F ` z ) ) <_ ( 2nd ` ( G ` J ) ) , ( 2nd ` ( F ` z ) ) , ( 2nd ` ( G ` J ) ) ) ) )
45 ioorebas 
 |-  ( if ( ( 1st ` ( F ` z ) ) <_ ( 1st ` ( G ` J ) ) , ( 1st ` ( G ` J ) ) , ( 1st ` ( F ` z ) ) ) (,) if ( ( 2nd ` ( F ` z ) ) <_ ( 2nd ` ( G ` J ) ) , ( 2nd ` ( F ` z ) ) , ( 2nd ` ( G ` J ) ) ) ) e. ran (,)
46 44 45 eqeltrdi 
 |-  ( ( ( ph /\ J e. NN ) /\ z e. NN ) -> ( ( (,) ` ( F ` z ) ) i^i ( (,) ` ( G ` J ) ) ) e. ran (,) )