Metamath Proof Explorer

Theorem ovolicc2lem5

Description: Lemma for ovolicc2 . (Contributed by Mario Carneiro, 14-Jun-2014)

Ref Expression
Hypotheses ovolicc.1 
|- ( ph -> A e. RR )
ovolicc.2 
|- ( ph -> B e. RR )
ovolicc.3 
|- ( ph -> A <_ B )
ovolicc2.4 
|- S = seq 1 ( + , ( ( abs o. - ) o. F ) )
ovolicc2.5 
|- ( ph -> F : NN --> ( <_ i^i ( RR X. RR ) ) )
ovolicc2.6 
|- ( ph -> U e. ( ~P ran ( (,) o. F ) i^i Fin ) )
ovolicc2.7 
|- ( ph -> ( A [,] B ) C_ U. U )
ovolicc2.8 
|- ( ph -> G : U --> NN )
ovolicc2.9 
|- ( ( ph /\ t e. U ) -> ( ( (,) o. F ) ` ( G ` t ) ) = t )
ovolicc2.10 
|- T = { u e. U | ( u i^i ( A [,] B ) ) =/= (/) }
Assertion ovolicc2lem5 
|- ( ph -> ( B - A ) <_ sup ( ran S , RR* , < ) )

Proof

Step Hyp Ref Expression
1 ovolicc.1 
 |-  ( ph -> A e. RR )
2 ovolicc.2 
 |-  ( ph -> B e. RR )
3 ovolicc.3 
 |-  ( ph -> A <_ B )
4 ovolicc2.4 
 |-  S = seq 1 ( + , ( ( abs o. - ) o. F ) )
5 ovolicc2.5 
 |-  ( ph -> F : NN --> ( <_ i^i ( RR X. RR ) ) )
6 ovolicc2.6 
 |-  ( ph -> U e. ( ~P ran ( (,) o. F ) i^i Fin ) )
7 ovolicc2.7 
 |-  ( ph -> ( A [,] B ) C_ U. U )
8 ovolicc2.8 
 |-  ( ph -> G : U --> NN )
9 ovolicc2.9 
 |-  ( ( ph /\ t e. U ) -> ( ( (,) o. F ) ` ( G ` t ) ) = t )
10 ovolicc2.10 
 |-  T = { u e. U | ( u i^i ( A [,] B ) ) =/= (/) }
11 1 rexrd 
 |-  ( ph -> A e. RR* )
12 2 rexrd 
 |-  ( ph -> B e. RR* )
13 lbicc2 
 |-  ( ( A e. RR* /\ B e. RR* /\ A <_ B ) -> A e. ( A [,] B ) )
14 11 12 3 13 syl3anc 
 |-  ( ph -> A e. ( A [,] B ) )
15 7 14 sseldd 
 |-  ( ph -> A e. U. U )
16 eluni2 
 |-  ( A e. U. U <-> E. z e. U A e. z )
17 15 16 sylib 
 |-  ( ph -> E. z e. U A e. z )
18 6 elin2d 
 |-  ( ph -> U e. Fin )
19 10 ssrab3 
 |-  T C_ U
20 ssfi 
 |-  ( ( U e. Fin /\ T C_ U ) -> T e. Fin )
21 18 19 20 sylancl 
 |-  ( ph -> T e. Fin )
22 7 adantr 
 |-  ( ( ph /\ t e. T ) -> ( A [,] B ) C_ U. U )
23 ineq1 
 |-  ( u = t -> ( u i^i ( A [,] B ) ) = ( t i^i ( A [,] B ) ) )
24 23 neeq1d 
 |-  ( u = t -> ( ( u i^i ( A [,] B ) ) =/= (/) <-> ( t i^i ( A [,] B ) ) =/= (/) ) )
25 24 10 elrab2 
 |-  ( t e. T <-> ( t e. U /\ ( t i^i ( A [,] B ) ) =/= (/) ) )
26 25 simplbi 
 |-  ( t e. T -> t e. U )
27 ffvelrn 
 |-  ( ( G : U --> NN /\ t e. U ) -> ( G ` t ) e. NN )
28 8 26 27 syl2an 
 |-  ( ( ph /\ t e. T ) -> ( G ` t ) e. NN )
29 5 ffvelrnda 
 |-  ( ( ph /\ ( G ` t ) e. NN ) -> ( F ` ( G ` t ) ) e. ( <_ i^i ( RR X. RR ) ) )
30 28 29 syldan 
 |-  ( ( ph /\ t e. T ) -> ( F ` ( G ` t ) ) e. ( <_ i^i ( RR X. RR ) ) )
31 30 elin2d 
 |-  ( ( ph /\ t e. T ) -> ( F ` ( G ` t ) ) e. ( RR X. RR ) )
32 xp2nd 
 |-  ( ( F ` ( G ` t ) ) e. ( RR X. RR ) -> ( 2nd ` ( F ` ( G ` t ) ) ) e. RR )
33 31 32 syl 
 |-  ( ( ph /\ t e. T ) -> ( 2nd ` ( F ` ( G ` t ) ) ) e. RR )
34 2 adantr 
 |-  ( ( ph /\ t e. T ) -> B e. RR )
35 33 34 ifcld 
 |-  ( ( ph /\ t e. T ) -> if ( ( 2nd ` ( F ` ( G ` t ) ) ) <_ B , ( 2nd ` ( F ` ( G ` t ) ) ) , B ) e. RR )
36 25 simprbi 
 |-  ( t e. T -> ( t i^i ( A [,] B ) ) =/= (/) )
37 36 adantl 
 |-  ( ( ph /\ t e. T ) -> ( t i^i ( A [,] B ) ) =/= (/) )
38 n0 
 |-  ( ( t i^i ( A [,] B ) ) =/= (/) <-> E. y y e. ( t i^i ( A [,] B ) ) )
39 37 38 sylib 
 |-  ( ( ph /\ t e. T ) -> E. y y e. ( t i^i ( A [,] B ) ) )
40 1 adantr 
 |-  ( ( ph /\ ( t e. T /\ y e. ( t i^i ( A [,] B ) ) ) ) -> A e. RR )
41 simprr 
 |-  ( ( ph /\ ( t e. T /\ y e. ( t i^i ( A [,] B ) ) ) ) -> y e. ( t i^i ( A [,] B ) ) )
42 41 elin2d 
 |-  ( ( ph /\ ( t e. T /\ y e. ( t i^i ( A [,] B ) ) ) ) -> y e. ( A [,] B ) )
43 2 adantr 
 |-  ( ( ph /\ ( t e. T /\ y e. ( t i^i ( A [,] B ) ) ) ) -> B e. RR )
44 elicc2 
 |-  ( ( A e. RR /\ B e. RR ) -> ( y e. ( A [,] B ) <-> ( y e. RR /\ A <_ y /\ y <_ B ) ) )
45 1 43 44 syl2an2r 
 |-  ( ( ph /\ ( t e. T /\ y e. ( t i^i ( A [,] B ) ) ) ) -> ( y e. ( A [,] B ) <-> ( y e. RR /\ A <_ y /\ y <_ B ) ) )
46 42 45 mpbid 
 |-  ( ( ph /\ ( t e. T /\ y e. ( t i^i ( A [,] B ) ) ) ) -> ( y e. RR /\ A <_ y /\ y <_ B ) )
47 46 simp1d 
 |-  ( ( ph /\ ( t e. T /\ y e. ( t i^i ( A [,] B ) ) ) ) -> y e. RR )
48 31 adantrr 
 |-  ( ( ph /\ ( t e. T /\ y e. ( t i^i ( A [,] B ) ) ) ) -> ( F ` ( G ` t ) ) e. ( RR X. RR ) )
49 48 32 syl 
 |-  ( ( ph /\ ( t e. T /\ y e. ( t i^i ( A [,] B ) ) ) ) -> ( 2nd ` ( F ` ( G ` t ) ) ) e. RR )
50 46 simp2d 
 |-  ( ( ph /\ ( t e. T /\ y e. ( t i^i ( A [,] B ) ) ) ) -> A <_ y )
51 41 elin1d 
 |-  ( ( ph /\ ( t e. T /\ y e. ( t i^i ( A [,] B ) ) ) ) -> y e. t )
52 28 adantrr 
 |-  ( ( ph /\ ( t e. T /\ y e. ( t i^i ( A [,] B ) ) ) ) -> ( G ` t ) e. NN )
53 fvco3 
 |-  ( ( F : NN --> ( <_ i^i ( RR X. RR ) ) /\ ( G ` t ) e. NN ) -> ( ( (,) o. F ) ` ( G ` t ) ) = ( (,) ` ( F ` ( G ` t ) ) ) )
54 5 52 53 syl2an2r 
 |-  ( ( ph /\ ( t e. T /\ y e. ( t i^i ( A [,] B ) ) ) ) -> ( ( (,) o. F ) ` ( G ` t ) ) = ( (,) ` ( F ` ( G ` t ) ) ) )
55 26 9 sylan2 
 |-  ( ( ph /\ t e. T ) -> ( ( (,) o. F ) ` ( G ` t ) ) = t )
56 55 adantrr 
 |-  ( ( ph /\ ( t e. T /\ y e. ( t i^i ( A [,] B ) ) ) ) -> ( ( (,) o. F ) ` ( G ` t ) ) = t )
57 1st2nd2 
 |-  ( ( F ` ( G ` t ) ) e. ( RR X. RR ) -> ( F ` ( G ` t ) ) = <. ( 1st ` ( F ` ( G ` t ) ) ) , ( 2nd ` ( F ` ( G ` t ) ) ) >. )
58 48 57 syl 
 |-  ( ( ph /\ ( t e. T /\ y e. ( t i^i ( A [,] B ) ) ) ) -> ( F ` ( G ` t ) ) = <. ( 1st ` ( F ` ( G ` t ) ) ) , ( 2nd ` ( F ` ( G ` t ) ) ) >. )
59 58 fveq2d 
 |-  ( ( ph /\ ( t e. T /\ y e. ( t i^i ( A [,] B ) ) ) ) -> ( (,) ` ( F ` ( G ` t ) ) ) = ( (,) ` <. ( 1st ` ( F ` ( G ` t ) ) ) , ( 2nd ` ( F ` ( G ` t ) ) ) >. ) )
60 df-ov 
 |-  ( ( 1st ` ( F ` ( G ` t ) ) ) (,) ( 2nd ` ( F ` ( G ` t ) ) ) ) = ( (,) ` <. ( 1st ` ( F ` ( G ` t ) ) ) , ( 2nd ` ( F ` ( G ` t ) ) ) >. )
61 59 60 eqtr4di 
 |-  ( ( ph /\ ( t e. T /\ y e. ( t i^i ( A [,] B ) ) ) ) -> ( (,) ` ( F ` ( G ` t ) ) ) = ( ( 1st ` ( F ` ( G ` t ) ) ) (,) ( 2nd ` ( F ` ( G ` t ) ) ) ) )
62 54 56 61 3eqtr3d 
 |-  ( ( ph /\ ( t e. T /\ y e. ( t i^i ( A [,] B ) ) ) ) -> t = ( ( 1st ` ( F ` ( G ` t ) ) ) (,) ( 2nd ` ( F ` ( G ` t ) ) ) ) )
63 51 62 eleqtrd 
 |-  ( ( ph /\ ( t e. T /\ y e. ( t i^i ( A [,] B ) ) ) ) -> y e. ( ( 1st ` ( F ` ( G ` t ) ) ) (,) ( 2nd ` ( F ` ( G ` t ) ) ) ) )
64 xp1st 
 |-  ( ( F ` ( G ` t ) ) e. ( RR X. RR ) -> ( 1st ` ( F ` ( G ` t ) ) ) e. RR )
65 48 64 syl 
 |-  ( ( ph /\ ( t e. T /\ y e. ( t i^i ( A [,] B ) ) ) ) -> ( 1st ` ( F ` ( G ` t ) ) ) e. RR )
66 rexr 
 |-  ( ( 1st ` ( F ` ( G ` t ) ) ) e. RR -> ( 1st ` ( F ` ( G ` t ) ) ) e. RR* )
67 rexr 
 |-  ( ( 2nd ` ( F ` ( G ` t ) ) ) e. RR -> ( 2nd ` ( F ` ( G ` t ) ) ) e. RR* )
68 elioo2 
 |-  ( ( ( 1st ` ( F ` ( G ` t ) ) ) e. RR* /\ ( 2nd ` ( F ` ( G ` t ) ) ) e. RR* ) -> ( y e. ( ( 1st ` ( F ` ( G ` t ) ) ) (,) ( 2nd ` ( F ` ( G ` t ) ) ) ) <-> ( y e. RR /\ ( 1st ` ( F ` ( G ` t ) ) ) < y /\ y < ( 2nd ` ( F ` ( G ` t ) ) ) ) ) )
69 66 67 68 syl2an 
 |-  ( ( ( 1st ` ( F ` ( G ` t ) ) ) e. RR /\ ( 2nd ` ( F ` ( G ` t ) ) ) e. RR ) -> ( y e. ( ( 1st ` ( F ` ( G ` t ) ) ) (,) ( 2nd ` ( F ` ( G ` t ) ) ) ) <-> ( y e. RR /\ ( 1st ` ( F ` ( G ` t ) ) ) < y /\ y < ( 2nd ` ( F ` ( G ` t ) ) ) ) ) )
70 65 49 69 syl2anc 
 |-  ( ( ph /\ ( t e. T /\ y e. ( t i^i ( A [,] B ) ) ) ) -> ( y e. ( ( 1st ` ( F ` ( G ` t ) ) ) (,) ( 2nd ` ( F ` ( G ` t ) ) ) ) <-> ( y e. RR /\ ( 1st ` ( F ` ( G ` t ) ) ) < y /\ y < ( 2nd ` ( F ` ( G ` t ) ) ) ) ) )
71 63 70 mpbid 
 |-  ( ( ph /\ ( t e. T /\ y e. ( t i^i ( A [,] B ) ) ) ) -> ( y e. RR /\ ( 1st ` ( F ` ( G ` t ) ) ) < y /\ y < ( 2nd ` ( F ` ( G ` t ) ) ) ) )
72 71 simp3d 
 |-  ( ( ph /\ ( t e. T /\ y e. ( t i^i ( A [,] B ) ) ) ) -> y < ( 2nd ` ( F ` ( G ` t ) ) ) )
73 47 49 72 ltled 
 |-  ( ( ph /\ ( t e. T /\ y e. ( t i^i ( A [,] B ) ) ) ) -> y <_ ( 2nd ` ( F ` ( G ` t ) ) ) )
74 40 47 49 50 73 letrd 
 |-  ( ( ph /\ ( t e. T /\ y e. ( t i^i ( A [,] B ) ) ) ) -> A <_ ( 2nd ` ( F ` ( G ` t ) ) ) )
75 74 expr 
 |-  ( ( ph /\ t e. T ) -> ( y e. ( t i^i ( A [,] B ) ) -> A <_ ( 2nd ` ( F ` ( G ` t ) ) ) ) )
76 75 exlimdv 
 |-  ( ( ph /\ t e. T ) -> ( E. y y e. ( t i^i ( A [,] B ) ) -> A <_ ( 2nd ` ( F ` ( G ` t ) ) ) ) )
77 39 76 mpd 
 |-  ( ( ph /\ t e. T ) -> A <_ ( 2nd ` ( F ` ( G ` t ) ) ) )
78 3 adantr 
 |-  ( ( ph /\ t e. T ) -> A <_ B )
79 breq2 
 |-  ( ( 2nd ` ( F ` ( G ` t ) ) ) = if ( ( 2nd ` ( F ` ( G ` t ) ) ) <_ B , ( 2nd ` ( F ` ( G ` t ) ) ) , B ) -> ( A <_ ( 2nd ` ( F ` ( G ` t ) ) ) <-> A <_ if ( ( 2nd ` ( F ` ( G ` t ) ) ) <_ B , ( 2nd ` ( F ` ( G ` t ) ) ) , B ) ) )
80 breq2 
 |-  ( B = if ( ( 2nd ` ( F ` ( G ` t ) ) ) <_ B , ( 2nd ` ( F ` ( G ` t ) ) ) , B ) -> ( A <_ B <-> A <_ if ( ( 2nd ` ( F ` ( G ` t ) ) ) <_ B , ( 2nd ` ( F ` ( G ` t ) ) ) , B ) ) )
81 79 80 ifboth 
 |-  ( ( A <_ ( 2nd ` ( F ` ( G ` t ) ) ) /\ A <_ B ) -> A <_ if ( ( 2nd ` ( F ` ( G ` t ) ) ) <_ B , ( 2nd ` ( F ` ( G ` t ) ) ) , B ) )
82 77 78 81 syl2anc 
 |-  ( ( ph /\ t e. T ) -> A <_ if ( ( 2nd ` ( F ` ( G ` t ) ) ) <_ B , ( 2nd ` ( F ` ( G ` t ) ) ) , B ) )
83 min2 
 |-  ( ( ( 2nd ` ( F ` ( G ` t ) ) ) e. RR /\ B e. RR ) -> if ( ( 2nd ` ( F ` ( G ` t ) ) ) <_ B , ( 2nd ` ( F ` ( G ` t ) ) ) , B ) <_ B )
84 33 34 83 syl2anc 
 |-  ( ( ph /\ t e. T ) -> if ( ( 2nd ` ( F ` ( G ` t ) ) ) <_ B , ( 2nd ` ( F ` ( G ` t ) ) ) , B ) <_ B )
85 elicc2 
 |-  ( ( A e. RR /\ B e. RR ) -> ( if ( ( 2nd ` ( F ` ( G ` t ) ) ) <_ B , ( 2nd ` ( F ` ( G ` t ) ) ) , B ) e. ( A [,] B ) <-> ( if ( ( 2nd ` ( F ` ( G ` t ) ) ) <_ B , ( 2nd ` ( F ` ( G ` t ) ) ) , B ) e. RR /\ A <_ if ( ( 2nd ` ( F ` ( G ` t ) ) ) <_ B , ( 2nd ` ( F ` ( G ` t ) ) ) , B ) /\ if ( ( 2nd ` ( F ` ( G ` t ) ) ) <_ B , ( 2nd ` ( F ` ( G ` t ) ) ) , B ) <_ B ) ) )
86 1 2 85 syl2anc 
 |-  ( ph -> ( if ( ( 2nd ` ( F ` ( G ` t ) ) ) <_ B , ( 2nd ` ( F ` ( G ` t ) ) ) , B ) e. ( A [,] B ) <-> ( if ( ( 2nd ` ( F ` ( G ` t ) ) ) <_ B , ( 2nd ` ( F ` ( G ` t ) ) ) , B ) e. RR /\ A <_ if ( ( 2nd ` ( F ` ( G ` t ) ) ) <_ B , ( 2nd ` ( F ` ( G ` t ) ) ) , B ) /\ if ( ( 2nd ` ( F ` ( G ` t ) ) ) <_ B , ( 2nd ` ( F ` ( G ` t ) ) ) , B ) <_ B ) ) )
87 86 adantr 
 |-  ( ( ph /\ t e. T ) -> ( if ( ( 2nd ` ( F ` ( G ` t ) ) ) <_ B , ( 2nd ` ( F ` ( G ` t ) ) ) , B ) e. ( A [,] B ) <-> ( if ( ( 2nd ` ( F ` ( G ` t ) ) ) <_ B , ( 2nd ` ( F ` ( G ` t ) ) ) , B ) e. RR /\ A <_ if ( ( 2nd ` ( F ` ( G ` t ) ) ) <_ B , ( 2nd ` ( F ` ( G ` t ) ) ) , B ) /\ if ( ( 2nd ` ( F ` ( G ` t ) ) ) <_ B , ( 2nd ` ( F ` ( G ` t ) ) ) , B ) <_ B ) ) )
88 35 82 84 87 mpbir3and 
 |-  ( ( ph /\ t e. T ) -> if ( ( 2nd ` ( F ` ( G ` t ) ) ) <_ B , ( 2nd ` ( F ` ( G ` t ) ) ) , B ) e. ( A [,] B ) )
89 22 88 sseldd 
 |-  ( ( ph /\ t e. T ) -> if ( ( 2nd ` ( F ` ( G ` t ) ) ) <_ B , ( 2nd ` ( F ` ( G ` t ) ) ) , B ) e. U. U )
90 eluni2 
 |-  ( if ( ( 2nd ` ( F ` ( G ` t ) ) ) <_ B , ( 2nd ` ( F ` ( G ` t ) ) ) , B ) e. U. U <-> E. x e. U if ( ( 2nd ` ( F ` ( G ` t ) ) ) <_ B , ( 2nd ` ( F ` ( G ` t ) ) ) , B ) e. x )
91 89 90 sylib 
 |-  ( ( ph /\ t e. T ) -> E. x e. U if ( ( 2nd ` ( F ` ( G ` t ) ) ) <_ B , ( 2nd ` ( F ` ( G ` t ) ) ) , B ) e. x )
92 simprl 
 |-  ( ( ( ph /\ t e. T ) /\ ( x e. U /\ if ( ( 2nd ` ( F ` ( G ` t ) ) ) <_ B , ( 2nd ` ( F ` ( G ` t ) ) ) , B ) e. x ) ) -> x e. U )
93 simprr 
 |-  ( ( ( ph /\ t e. T ) /\ ( x e. U /\ if ( ( 2nd ` ( F ` ( G ` t ) ) ) <_ B , ( 2nd ` ( F ` ( G ` t ) ) ) , B ) e. x ) ) -> if ( ( 2nd ` ( F ` ( G ` t ) ) ) <_ B , ( 2nd ` ( F ` ( G ` t ) ) ) , B ) e. x )
94 88 adantr 
 |-  ( ( ( ph /\ t e. T ) /\ ( x e. U /\ if ( ( 2nd ` ( F ` ( G ` t ) ) ) <_ B , ( 2nd ` ( F ` ( G ` t ) ) ) , B ) e. x ) ) -> if ( ( 2nd ` ( F ` ( G ` t ) ) ) <_ B , ( 2nd ` ( F ` ( G ` t ) ) ) , B ) e. ( A [,] B ) )
95 inelcm 
 |-  ( ( if ( ( 2nd ` ( F ` ( G ` t ) ) ) <_ B , ( 2nd ` ( F ` ( G ` t ) ) ) , B ) e. x /\ if ( ( 2nd ` ( F ` ( G ` t ) ) ) <_ B , ( 2nd ` ( F ` ( G ` t ) ) ) , B ) e. ( A [,] B ) ) -> ( x i^i ( A [,] B ) ) =/= (/) )
96 93 94 95 syl2anc 
 |-  ( ( ( ph /\ t e. T ) /\ ( x e. U /\ if ( ( 2nd ` ( F ` ( G ` t ) ) ) <_ B , ( 2nd ` ( F ` ( G ` t ) ) ) , B ) e. x ) ) -> ( x i^i ( A [,] B ) ) =/= (/) )
97 ineq1 
 |-  ( u = x -> ( u i^i ( A [,] B ) ) = ( x i^i ( A [,] B ) ) )
98 97 neeq1d 
 |-  ( u = x -> ( ( u i^i ( A [,] B ) ) =/= (/) <-> ( x i^i ( A [,] B ) ) =/= (/) ) )
99 98 10 elrab2 
 |-  ( x e. T <-> ( x e. U /\ ( x i^i ( A [,] B ) ) =/= (/) ) )
100 92 96 99 sylanbrc 
 |-  ( ( ( ph /\ t e. T ) /\ ( x e. U /\ if ( ( 2nd ` ( F ` ( G ` t ) ) ) <_ B , ( 2nd ` ( F ` ( G ` t ) ) ) , B ) e. x ) ) -> x e. T )
101 91 100 93 reximssdv 
 |-  ( ( ph /\ t e. T ) -> E. x e. T if ( ( 2nd ` ( F ` ( G ` t ) ) ) <_ B , ( 2nd ` ( F ` ( G ` t ) ) ) , B ) e. x )
102 101 ralrimiva 
 |-  ( ph -> A. t e. T E. x e. T if ( ( 2nd ` ( F ` ( G ` t ) ) ) <_ B , ( 2nd ` ( F ` ( G ` t ) ) ) , B ) e. x )
103 eleq2 
 |-  ( x = ( h ` t ) -> ( if ( ( 2nd ` ( F ` ( G ` t ) ) ) <_ B , ( 2nd ` ( F ` ( G ` t ) ) ) , B ) e. x <-> if ( ( 2nd ` ( F ` ( G ` t ) ) ) <_ B , ( 2nd ` ( F ` ( G ` t ) ) ) , B ) e. ( h ` t ) ) )
104 103 ac6sfi 
 |-  ( ( T e. Fin /\ A. t e. T E. x e. T if ( ( 2nd ` ( F ` ( G ` t ) ) ) <_ B , ( 2nd ` ( F ` ( G ` t ) ) ) , B ) e. x ) -> E. h ( h : T --> T /\ A. t e. T if ( ( 2nd ` ( F ` ( G ` t ) ) ) <_ B , ( 2nd ` ( F ` ( G ` t ) ) ) , B ) e. ( h ` t ) ) )
105 21 102 104 syl2anc 
 |-  ( ph -> E. h ( h : T --> T /\ A. t e. T if ( ( 2nd ` ( F ` ( G ` t ) ) ) <_ B , ( 2nd ` ( F ` ( G ` t ) ) ) , B ) e. ( h ` t ) ) )
106 105 adantr 
 |-  ( ( ph /\ ( z e. U /\ A e. z ) ) -> E. h ( h : T --> T /\ A. t e. T if ( ( 2nd ` ( F ` ( G ` t ) ) ) <_ B , ( 2nd ` ( F ` ( G ` t ) ) ) , B ) e. ( h ` t ) ) )
107 2fveq3 
 |-  ( x = t -> ( F ` ( G ` x ) ) = ( F ` ( G ` t ) ) )
108 107 fveq2d 
 |-  ( x = t -> ( 2nd ` ( F ` ( G ` x ) ) ) = ( 2nd ` ( F ` ( G ` t ) ) ) )
109 108 breq1d 
 |-  ( x = t -> ( ( 2nd ` ( F ` ( G ` x ) ) ) <_ B <-> ( 2nd ` ( F ` ( G ` t ) ) ) <_ B ) )
110 109 108 ifbieq1d 
 |-  ( x = t -> if ( ( 2nd ` ( F ` ( G ` x ) ) ) <_ B , ( 2nd ` ( F ` ( G ` x ) ) ) , B ) = if ( ( 2nd ` ( F ` ( G ` t ) ) ) <_ B , ( 2nd ` ( F ` ( G ` t ) ) ) , B ) )
111 fveq2 
 |-  ( x = t -> ( h ` x ) = ( h ` t ) )
112 110 111 eleq12d 
 |-  ( x = t -> ( if ( ( 2nd ` ( F ` ( G ` x ) ) ) <_ B , ( 2nd ` ( F ` ( G ` x ) ) ) , B ) e. ( h ` x ) <-> if ( ( 2nd ` ( F ` ( G ` t ) ) ) <_ B , ( 2nd ` ( F ` ( G ` t ) ) ) , B ) e. ( h ` t ) ) )
113 112 cbvralvw 
 |-  ( A. x e. T if ( ( 2nd ` ( F ` ( G ` x ) ) ) <_ B , ( 2nd ` ( F ` ( G ` x ) ) ) , B ) e. ( h ` x ) <-> A. t e. T if ( ( 2nd ` ( F ` ( G ` t ) ) ) <_ B , ( 2nd ` ( F ` ( G ` t ) ) ) , B ) e. ( h ` t ) )
114 1 adantr 
 |-  ( ( ph /\ ( ( z e. U /\ A e. z ) /\ ( h : T --> T /\ A. x e. T if ( ( 2nd ` ( F ` ( G ` x ) ) ) <_ B , ( 2nd ` ( F ` ( G ` x ) ) ) , B ) e. ( h ` x ) ) ) ) -> A e. RR )
115 2 adantr 
 |-  ( ( ph /\ ( ( z e. U /\ A e. z ) /\ ( h : T --> T /\ A. x e. T if ( ( 2nd ` ( F ` ( G ` x ) ) ) <_ B , ( 2nd ` ( F ` ( G ` x ) ) ) , B ) e. ( h ` x ) ) ) ) -> B e. RR )
116 3 adantr 
 |-  ( ( ph /\ ( ( z e. U /\ A e. z ) /\ ( h : T --> T /\ A. x e. T if ( ( 2nd ` ( F ` ( G ` x ) ) ) <_ B , ( 2nd ` ( F ` ( G ` x ) ) ) , B ) e. ( h ` x ) ) ) ) -> A <_ B )
117 5 adantr 
 |-  ( ( ph /\ ( ( z e. U /\ A e. z ) /\ ( h : T --> T /\ A. x e. T if ( ( 2nd ` ( F ` ( G ` x ) ) ) <_ B , ( 2nd ` ( F ` ( G ` x ) ) ) , B ) e. ( h ` x ) ) ) ) -> F : NN --> ( <_ i^i ( RR X. RR ) ) )
118 6 adantr 
 |-  ( ( ph /\ ( ( z e. U /\ A e. z ) /\ ( h : T --> T /\ A. x e. T if ( ( 2nd ` ( F ` ( G ` x ) ) ) <_ B , ( 2nd ` ( F ` ( G ` x ) ) ) , B ) e. ( h ` x ) ) ) ) -> U e. ( ~P ran ( (,) o. F ) i^i Fin ) )
119 7 adantr 
 |-  ( ( ph /\ ( ( z e. U /\ A e. z ) /\ ( h : T --> T /\ A. x e. T if ( ( 2nd ` ( F ` ( G ` x ) ) ) <_ B , ( 2nd ` ( F ` ( G ` x ) ) ) , B ) e. ( h ` x ) ) ) ) -> ( A [,] B ) C_ U. U )
120 8 adantr 
 |-  ( ( ph /\ ( ( z e. U /\ A e. z ) /\ ( h : T --> T /\ A. x e. T if ( ( 2nd ` ( F ` ( G ` x ) ) ) <_ B , ( 2nd ` ( F ` ( G ` x ) ) ) , B ) e. ( h ` x ) ) ) ) -> G : U --> NN )
121 9 adantlr 
 |-  ( ( ( ph /\ ( ( z e. U /\ A e. z ) /\ ( h : T --> T /\ A. x e. T if ( ( 2nd ` ( F ` ( G ` x ) ) ) <_ B , ( 2nd ` ( F ` ( G ` x ) ) ) , B ) e. ( h ` x ) ) ) ) /\ t e. U ) -> ( ( (,) o. F ) ` ( G ` t ) ) = t )
122 simprrl 
 |-  ( ( ph /\ ( ( z e. U /\ A e. z ) /\ ( h : T --> T /\ A. x e. T if ( ( 2nd ` ( F ` ( G ` x ) ) ) <_ B , ( 2nd ` ( F ` ( G ` x ) ) ) , B ) e. ( h ` x ) ) ) ) -> h : T --> T )
123 simprrr 
 |-  ( ( ph /\ ( ( z e. U /\ A e. z ) /\ ( h : T --> T /\ A. x e. T if ( ( 2nd ` ( F ` ( G ` x ) ) ) <_ B , ( 2nd ` ( F ` ( G ` x ) ) ) , B ) e. ( h ` x ) ) ) ) -> A. x e. T if ( ( 2nd ` ( F ` ( G ` x ) ) ) <_ B , ( 2nd ` ( F ` ( G ` x ) ) ) , B ) e. ( h ` x ) )
124 112 rspccva 
 |-  ( ( A. x e. T if ( ( 2nd ` ( F ` ( G ` x ) ) ) <_ B , ( 2nd ` ( F ` ( G ` x ) ) ) , B ) e. ( h ` x ) /\ t e. T ) -> if ( ( 2nd ` ( F ` ( G ` t ) ) ) <_ B , ( 2nd ` ( F ` ( G ` t ) ) ) , B ) e. ( h ` t ) )
125 123 124 sylan 
 |-  ( ( ( ph /\ ( ( z e. U /\ A e. z ) /\ ( h : T --> T /\ A. x e. T if ( ( 2nd ` ( F ` ( G ` x ) ) ) <_ B , ( 2nd ` ( F ` ( G ` x ) ) ) , B ) e. ( h ` x ) ) ) ) /\ t e. T ) -> if ( ( 2nd ` ( F ` ( G ` t ) ) ) <_ B , ( 2nd ` ( F ` ( G ` t ) ) ) , B ) e. ( h ` t ) )
126 simprlr 
 |-  ( ( ph /\ ( ( z e. U /\ A e. z ) /\ ( h : T --> T /\ A. x e. T if ( ( 2nd ` ( F ` ( G ` x ) ) ) <_ B , ( 2nd ` ( F ` ( G ` x ) ) ) , B ) e. ( h ` x ) ) ) ) -> A e. z )
127 simprll 
 |-  ( ( ph /\ ( ( z e. U /\ A e. z ) /\ ( h : T --> T /\ A. x e. T if ( ( 2nd ` ( F ` ( G ` x ) ) ) <_ B , ( 2nd ` ( F ` ( G ` x ) ) ) , B ) e. ( h ` x ) ) ) ) -> z e. U )
128 14 adantr 
 |-  ( ( ph /\ ( ( z e. U /\ A e. z ) /\ ( h : T --> T /\ A. x e. T if ( ( 2nd ` ( F ` ( G ` x ) ) ) <_ B , ( 2nd ` ( F ` ( G ` x ) ) ) , B ) e. ( h ` x ) ) ) ) -> A e. ( A [,] B ) )
129 inelcm 
 |-  ( ( A e. z /\ A e. ( A [,] B ) ) -> ( z i^i ( A [,] B ) ) =/= (/) )
130 126 128 129 syl2anc 
 |-  ( ( ph /\ ( ( z e. U /\ A e. z ) /\ ( h : T --> T /\ A. x e. T if ( ( 2nd ` ( F ` ( G ` x ) ) ) <_ B , ( 2nd ` ( F ` ( G ` x ) ) ) , B ) e. ( h ` x ) ) ) ) -> ( z i^i ( A [,] B ) ) =/= (/) )
131 ineq1 
 |-  ( u = z -> ( u i^i ( A [,] B ) ) = ( z i^i ( A [,] B ) ) )
132 131 neeq1d 
 |-  ( u = z -> ( ( u i^i ( A [,] B ) ) =/= (/) <-> ( z i^i ( A [,] B ) ) =/= (/) ) )
133 132 10 elrab2 
 |-  ( z e. T <-> ( z e. U /\ ( z i^i ( A [,] B ) ) =/= (/) ) )
134 127 130 133 sylanbrc 
 |-  ( ( ph /\ ( ( z e. U /\ A e. z ) /\ ( h : T --> T /\ A. x e. T if ( ( 2nd ` ( F ` ( G ` x ) ) ) <_ B , ( 2nd ` ( F ` ( G ` x ) ) ) , B ) e. ( h ` x ) ) ) ) -> z e. T )
135 eqid 
 |-  seq 1 ( ( h o. 1st ) , ( NN X. { z } ) ) = seq 1 ( ( h o. 1st ) , ( NN X. { z } ) )
136 fveq2 
 |-  ( m = n -> ( seq 1 ( ( h o. 1st ) , ( NN X. { z } ) ) ` m ) = ( seq 1 ( ( h o. 1st ) , ( NN X. { z } ) ) ` n ) )
137 136 eleq2d 
 |-  ( m = n -> ( B e. ( seq 1 ( ( h o. 1st ) , ( NN X. { z } ) ) ` m ) <-> B e. ( seq 1 ( ( h o. 1st ) , ( NN X. { z } ) ) ` n ) ) )
138 137 cbvrabv 
 |-  { m e. NN | B e. ( seq 1 ( ( h o. 1st ) , ( NN X. { z } ) ) ` m ) } = { n e. NN | B e. ( seq 1 ( ( h o. 1st ) , ( NN X. { z } ) ) ` n ) }
139 eqid 
 |-  inf ( { m e. NN | B e. ( seq 1 ( ( h o. 1st ) , ( NN X. { z } ) ) ` m ) } , RR , < ) = inf ( { m e. NN | B e. ( seq 1 ( ( h o. 1st ) , ( NN X. { z } ) ) ` m ) } , RR , < )
140 114 115 116 4 117 118 119 120 121 10 122 125 126 134 135 138 139 ovolicc2lem4 
 |-  ( ( ph /\ ( ( z e. U /\ A e. z ) /\ ( h : T --> T /\ A. x e. T if ( ( 2nd ` ( F ` ( G ` x ) ) ) <_ B , ( 2nd ` ( F ` ( G ` x ) ) ) , B ) e. ( h ` x ) ) ) ) -> ( B - A ) <_ sup ( ran S , RR* , < ) )
141 140 anassrs 
 |-  ( ( ( ph /\ ( z e. U /\ A e. z ) ) /\ ( h : T --> T /\ A. x e. T if ( ( 2nd ` ( F ` ( G ` x ) ) ) <_ B , ( 2nd ` ( F ` ( G ` x ) ) ) , B ) e. ( h ` x ) ) ) -> ( B - A ) <_ sup ( ran S , RR* , < ) )
142 141 expr 
 |-  ( ( ( ph /\ ( z e. U /\ A e. z ) ) /\ h : T --> T ) -> ( A. x e. T if ( ( 2nd ` ( F ` ( G ` x ) ) ) <_ B , ( 2nd ` ( F ` ( G ` x ) ) ) , B ) e. ( h ` x ) -> ( B - A ) <_ sup ( ran S , RR* , < ) ) )
143 113 142 syl5bir 
 |-  ( ( ( ph /\ ( z e. U /\ A e. z ) ) /\ h : T --> T ) -> ( A. t e. T if ( ( 2nd ` ( F ` ( G ` t ) ) ) <_ B , ( 2nd ` ( F ` ( G ` t ) ) ) , B ) e. ( h ` t ) -> ( B - A ) <_ sup ( ran S , RR* , < ) ) )
144 143 expimpd 
 |-  ( ( ph /\ ( z e. U /\ A e. z ) ) -> ( ( h : T --> T /\ A. t e. T if ( ( 2nd ` ( F ` ( G ` t ) ) ) <_ B , ( 2nd ` ( F ` ( G ` t ) ) ) , B ) e. ( h ` t ) ) -> ( B - A ) <_ sup ( ran S , RR* , < ) ) )
145 144 exlimdv 
 |-  ( ( ph /\ ( z e. U /\ A e. z ) ) -> ( E. h ( h : T --> T /\ A. t e. T if ( ( 2nd ` ( F ` ( G ` t ) ) ) <_ B , ( 2nd ` ( F ` ( G ` t ) ) ) , B ) e. ( h ` t ) ) -> ( B - A ) <_ sup ( ran S , RR* , < ) ) )
146 106 145 mpd 
 |-  ( ( ph /\ ( z e. U /\ A e. z ) ) -> ( B - A ) <_ sup ( ran S , RR* , < ) )
147 17 146 rexlimddv 
 |-  ( ph -> ( B - A ) <_ sup ( ran S , RR* , < ) )