Users' Mathboxes Mathbox for Brendan Leahy < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  itg2addnclem2 Unicode version

Theorem itg2addnclem2 26156
Description: Lemma for itg2addnc 26158. The function described is a simple function. (Contributed by Brendan Leahy, 29-Oct-2017.)
Hypotheses
Ref Expression
itg2addnc.f1  |-  ( ph  ->  F  e. MblFn )
itg2addnc.f2  |-  ( ph  ->  F : RR --> ( 0 [,)  +oo ) )
Assertion
Ref Expression
itg2addnclem2  |-  ( ( ( ph  /\  h  e.  dom  S.1 )  /\  v  e.  RR+ )  ->  (
x  e.  RR  |->  if ( ( ( ( ( |_ `  (
( F `  x
)  /  ( v  /  3 ) ) )  -  1 )  x.  ( v  / 
3 ) )  <_ 
( h `  x
)  /\  ( h `  x )  =/=  0
) ,  ( ( ( |_ `  (
( F `  x
)  /  ( v  /  3 ) ) )  -  1 )  x.  ( v  / 
3 ) ) ,  ( h `  x
) ) )  e. 
dom  S.1 )
Distinct variable groups:    x, v, h, F    ph, v, x, h

Proof of Theorem itg2addnclem2
Dummy variables  t 
y are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 itg2addnc.f2 . . . . . . . . . . 11  |-  ( ph  ->  F : RR --> ( 0 [,)  +oo ) )
2 0re 9047 . . . . . . . . . . . 12  |-  0  e.  RR
3 pnfxr 10669 . . . . . . . . . . . 12  |-  +oo  e.  RR*
4 icossre 10947 . . . . . . . . . . . 12  |-  ( ( 0  e.  RR  /\  +oo 
e.  RR* )  ->  (
0 [,)  +oo )  C_  RR )
52, 3, 4mp2an 654 . . . . . . . . . . 11  |-  ( 0 [,)  +oo )  C_  RR
6 fss 5558 . . . . . . . . . . 11  |-  ( ( F : RR --> ( 0 [,)  +oo )  /\  (
0 [,)  +oo )  C_  RR )  ->  F : RR
--> RR )
71, 5, 6sylancl 644 . . . . . . . . . 10  |-  ( ph  ->  F : RR --> RR )
87ad2antrr 707 . . . . . . . . 9  |-  ( ( ( ph  /\  h  e.  dom  S.1 )  /\  v  e.  RR+ )  ->  F : RR --> RR )
98ffvelrnda 5829 . . . . . . . 8  |-  ( ( ( ( ph  /\  h  e.  dom  S.1 )  /\  v  e.  RR+ )  /\  x  e.  RR )  ->  ( F `  x )  e.  RR )
10 rpre 10574 . . . . . . . . . 10  |-  ( v  e.  RR+  ->  v  e.  RR )
11 3re 10027 . . . . . . . . . . 11  |-  3  e.  RR
12 3ne0 10041 . . . . . . . . . . 11  |-  3  =/=  0
1311, 12pm3.2i 442 . . . . . . . . . 10  |-  ( 3  e.  RR  /\  3  =/=  0 )
14 redivcl 9689 . . . . . . . . . . 11  |-  ( ( v  e.  RR  /\  3  e.  RR  /\  3  =/=  0 )  ->  (
v  /  3 )  e.  RR )
15143expb 1154 . . . . . . . . . 10  |-  ( ( v  e.  RR  /\  ( 3  e.  RR  /\  3  =/=  0 ) )  ->  ( v  /  3 )  e.  RR )
1610, 13, 15sylancl 644 . . . . . . . . 9  |-  ( v  e.  RR+  ->  ( v  /  3 )  e.  RR )
1716ad2antlr 708 . . . . . . . 8  |-  ( ( ( ( ph  /\  h  e.  dom  S.1 )  /\  v  e.  RR+ )  /\  x  e.  RR )  ->  ( v  / 
3 )  e.  RR )
18 rpcnne0 10585 . . . . . . . . . 10  |-  ( v  e.  RR+  ->  ( v  e.  CC  /\  v  =/=  0 ) )
19 3cn 10028 . . . . . . . . . . 11  |-  3  e.  CC
2019, 12pm3.2i 442 . . . . . . . . . 10  |-  ( 3  e.  CC  /\  3  =/=  0 )
21 divne0 9646 . . . . . . . . . 10  |-  ( ( ( v  e.  CC  /\  v  =/=  0 )  /\  ( 3  e.  CC  /\  3  =/=  0 ) )  -> 
( v  /  3
)  =/=  0 )
2218, 20, 21sylancl 644 . . . . . . . . 9  |-  ( v  e.  RR+  ->  ( v  /  3 )  =/=  0 )
2322ad2antlr 708 . . . . . . . 8  |-  ( ( ( ( ph  /\  h  e.  dom  S.1 )  /\  v  e.  RR+ )  /\  x  e.  RR )  ->  ( v  / 
3 )  =/=  0
)
249, 17, 23redivcld 9798 . . . . . . 7  |-  ( ( ( ( ph  /\  h  e.  dom  S.1 )  /\  v  e.  RR+ )  /\  x  e.  RR )  ->  ( ( F `
 x )  / 
( v  /  3
) )  e.  RR )
25 reflcl 11160 . . . . . . 7  |-  ( ( ( F `  x
)  /  ( v  /  3 ) )  e.  RR  ->  ( |_ `  ( ( F `
 x )  / 
( v  /  3
) ) )  e.  RR )
2624, 25syl 16 . . . . . 6  |-  ( ( ( ( ph  /\  h  e.  dom  S.1 )  /\  v  e.  RR+ )  /\  x  e.  RR )  ->  ( |_ `  ( ( F `  x )  /  (
v  /  3 ) ) )  e.  RR )
27 peano2rem 9323 . . . . . 6  |-  ( ( |_ `  ( ( F `  x )  /  ( v  / 
3 ) ) )  e.  RR  ->  (
( |_ `  (
( F `  x
)  /  ( v  /  3 ) ) )  -  1 )  e.  RR )
2826, 27syl 16 . . . . 5  |-  ( ( ( ( ph  /\  h  e.  dom  S.1 )  /\  v  e.  RR+ )  /\  x  e.  RR )  ->  ( ( |_
`  ( ( F `
 x )  / 
( v  /  3
) ) )  - 
1 )  e.  RR )
2928, 17remulcld 9072 . . . 4  |-  ( ( ( ( ph  /\  h  e.  dom  S.1 )  /\  v  e.  RR+ )  /\  x  e.  RR )  ->  ( ( ( |_ `  ( ( F `  x )  /  ( v  / 
3 ) ) )  -  1 )  x.  ( v  /  3
) )  e.  RR )
30 i1ff 19521 . . . . . 6  |-  ( h  e.  dom  S.1  ->  h : RR --> RR )
3130ad2antlr 708 . . . . 5  |-  ( ( ( ph  /\  h  e.  dom  S.1 )  /\  v  e.  RR+ )  ->  h : RR --> RR )
3231ffvelrnda 5829 . . . 4  |-  ( ( ( ( ph  /\  h  e.  dom  S.1 )  /\  v  e.  RR+ )  /\  x  e.  RR )  ->  ( h `  x )  e.  RR )
33 ifcl 3735 . . . 4  |-  ( ( ( ( ( |_
`  ( ( F `
 x )  / 
( v  /  3
) ) )  - 
1 )  x.  (
v  /  3 ) )  e.  RR  /\  ( h `  x
)  e.  RR )  ->  if ( ( ( ( ( |_
`  ( ( F `
 x )  / 
( v  /  3
) ) )  - 
1 )  x.  (
v  /  3 ) )  <_  ( h `  x )  /\  (
h `  x )  =/=  0 ) ,  ( ( ( |_ `  ( ( F `  x )  /  (
v  /  3 ) ) )  -  1 )  x.  ( v  /  3 ) ) ,  ( h `  x ) )  e.  RR )
3429, 32, 33syl2anc 643 . . 3  |-  ( ( ( ( ph  /\  h  e.  dom  S.1 )  /\  v  e.  RR+ )  /\  x  e.  RR )  ->  if ( ( ( ( ( |_
`  ( ( F `
 x )  / 
( v  /  3
) ) )  - 
1 )  x.  (
v  /  3 ) )  <_  ( h `  x )  /\  (
h `  x )  =/=  0 ) ,  ( ( ( |_ `  ( ( F `  x )  /  (
v  /  3 ) ) )  -  1 )  x.  ( v  /  3 ) ) ,  ( h `  x ) )  e.  RR )
35 eqid 2404 . . 3  |-  ( x  e.  RR  |->  if ( ( ( ( ( |_ `  ( ( F `  x )  /  ( v  / 
3 ) ) )  -  1 )  x.  ( v  /  3
) )  <_  (
h `  x )  /\  ( h `  x
)  =/=  0 ) ,  ( ( ( |_ `  ( ( F `  x )  /  ( v  / 
3 ) ) )  -  1 )  x.  ( v  /  3
) ) ,  ( h `  x ) ) )  =  ( x  e.  RR  |->  if ( ( ( ( ( |_ `  (
( F `  x
)  /  ( v  /  3 ) ) )  -  1 )  x.  ( v  / 
3 ) )  <_ 
( h `  x
)  /\  ( h `  x )  =/=  0
) ,  ( ( ( |_ `  (
( F `  x
)  /  ( v  /  3 ) ) )  -  1 )  x.  ( v  / 
3 ) ) ,  ( h `  x
) ) )
3634, 35fmptd 5852 . 2  |-  ( ( ( ph  /\  h  e.  dom  S.1 )  /\  v  e.  RR+ )  ->  (
x  e.  RR  |->  if ( ( ( ( ( |_ `  (
( F `  x
)  /  ( v  /  3 ) ) )  -  1 )  x.  ( v  / 
3 ) )  <_ 
( h `  x
)  /\  ( h `  x )  =/=  0
) ,  ( ( ( |_ `  (
( F `  x
)  /  ( v  /  3 ) ) )  -  1 )  x.  ( v  / 
3 ) ) ,  ( h `  x
) ) ) : RR --> RR )
37 fzfi 11266 . . . . 5  |-  ( 0 ... -u ( |_ `  -u ( ( sup ( ran  h ,  RR ,  <  )  /  ( v  /  3 ) )  +  1 ) ) )  e.  Fin
38 ovex 6065 . . . . . . 7  |-  ( ( t  -  1 )  x.  ( v  / 
3 ) )  e. 
_V
39 eqid 2404 . . . . . . 7  |-  ( t  e.  ( 0 ... -u ( |_ `  -u (
( sup ( ran  h ,  RR ,  <  )  /  ( v  /  3 ) )  +  1 ) ) )  |->  ( ( t  -  1 )  x.  ( v  /  3
) ) )  =  ( t  e.  ( 0 ... -u ( |_ `  -u ( ( sup ( ran  h ,  RR ,  <  )  /  ( v  / 
3 ) )  +  1 ) ) ) 
|->  ( ( t  - 
1 )  x.  (
v  /  3 ) ) )
4038, 39fnmpti 5532 . . . . . 6  |-  ( t  e.  ( 0 ... -u ( |_ `  -u (
( sup ( ran  h ,  RR ,  <  )  /  ( v  /  3 ) )  +  1 ) ) )  |->  ( ( t  -  1 )  x.  ( v  /  3
) ) )  Fn  ( 0 ... -u ( |_ `  -u ( ( sup ( ran  h ,  RR ,  <  )  /  ( v  / 
3 ) )  +  1 ) ) )
41 dffn4 5618 . . . . . 6  |-  ( ( t  e.  ( 0 ... -u ( |_ `  -u ( ( sup ( ran  h ,  RR ,  <  )  /  ( v  /  3 ) )  +  1 ) ) )  |->  ( ( t  -  1 )  x.  ( v  /  3
) ) )  Fn  ( 0 ... -u ( |_ `  -u ( ( sup ( ran  h ,  RR ,  <  )  /  ( v  / 
3 ) )  +  1 ) ) )  <-> 
( t  e.  ( 0 ... -u ( |_ `  -u ( ( sup ( ran  h ,  RR ,  <  )  /  ( v  / 
3 ) )  +  1 ) ) ) 
|->  ( ( t  - 
1 )  x.  (
v  /  3 ) ) ) : ( 0 ... -u ( |_ `  -u ( ( sup ( ran  h ,  RR ,  <  )  /  ( v  / 
3 ) )  +  1 ) ) )
-onto->
ran  ( t  e.  ( 0 ... -u ( |_ `  -u ( ( sup ( ran  h ,  RR ,  <  )  /  ( v  / 
3 ) )  +  1 ) ) ) 
|->  ( ( t  - 
1 )  x.  (
v  /  3 ) ) ) )
4240, 41mpbi 200 . . . . 5  |-  ( t  e.  ( 0 ... -u ( |_ `  -u (
( sup ( ran  h ,  RR ,  <  )  /  ( v  /  3 ) )  +  1 ) ) )  |->  ( ( t  -  1 )  x.  ( v  /  3
) ) ) : ( 0 ... -u ( |_ `  -u ( ( sup ( ran  h ,  RR ,  <  )  /  ( v  / 
3 ) )  +  1 ) ) )
-onto->
ran  ( t  e.  ( 0 ... -u ( |_ `  -u ( ( sup ( ran  h ,  RR ,  <  )  /  ( v  / 
3 ) )  +  1 ) ) ) 
|->  ( ( t  - 
1 )  x.  (
v  /  3 ) ) )
43 fofi 7351 . . . . 5  |-  ( ( ( 0 ... -u ( |_ `  -u ( ( sup ( ran  h ,  RR ,  <  )  /  ( v  / 
3 ) )  +  1 ) ) )  e.  Fin  /\  (
t  e.  ( 0 ... -u ( |_ `  -u ( ( sup ( ran  h ,  RR ,  <  )  /  ( v  /  3 ) )  +  1 ) ) )  |->  ( ( t  -  1 )  x.  ( v  /  3
) ) ) : ( 0 ... -u ( |_ `  -u ( ( sup ( ran  h ,  RR ,  <  )  /  ( v  / 
3 ) )  +  1 ) ) )
-onto->
ran  ( t  e.  ( 0 ... -u ( |_ `  -u ( ( sup ( ran  h ,  RR ,  <  )  /  ( v  / 
3 ) )  +  1 ) ) ) 
|->  ( ( t  - 
1 )  x.  (
v  /  3 ) ) ) )  ->  ran  ( t  e.  ( 0 ... -u ( |_ `  -u ( ( sup ( ran  h ,  RR ,  <  )  /  ( v  / 
3 ) )  +  1 ) ) ) 
|->  ( ( t  - 
1 )  x.  (
v  /  3 ) ) )  e.  Fin )
4437, 42, 43mp2an 654 . . . 4  |-  ran  (
t  e.  ( 0 ... -u ( |_ `  -u ( ( sup ( ran  h ,  RR ,  <  )  /  ( v  /  3 ) )  +  1 ) ) )  |->  ( ( t  -  1 )  x.  ( v  /  3
) ) )  e. 
Fin
45 i1frn 19522 . . . . 5  |-  ( h  e.  dom  S.1  ->  ran  h  e.  Fin )
4645ad2antlr 708 . . . 4  |-  ( ( ( ph  /\  h  e.  dom  S.1 )  /\  v  e.  RR+ )  ->  ran  h  e.  Fin )
47 unfi 7333 . . . 4  |-  ( ( ran  ( t  e.  ( 0 ... -u ( |_ `  -u ( ( sup ( ran  h ,  RR ,  <  )  /  ( v  / 
3 ) )  +  1 ) ) ) 
|->  ( ( t  - 
1 )  x.  (
v  /  3 ) ) )  e.  Fin  /\ 
ran  h  e.  Fin )  ->  ( ran  (
t  e.  ( 0 ... -u ( |_ `  -u ( ( sup ( ran  h ,  RR ,  <  )  /  ( v  /  3 ) )  +  1 ) ) )  |->  ( ( t  -  1 )  x.  ( v  /  3
) ) )  u. 
ran  h )  e. 
Fin )
4844, 46, 47sylancr 645 . . 3  |-  ( ( ( ph  /\  h  e.  dom  S.1 )  /\  v  e.  RR+ )  ->  ( ran  ( t  e.  ( 0 ... -u ( |_ `  -u ( ( sup ( ran  h ,  RR ,  <  )  /  ( v  / 
3 ) )  +  1 ) ) ) 
|->  ( ( t  - 
1 )  x.  (
v  /  3 ) ) )  u.  ran  h )  e.  Fin )
49 3nn 10090 . . . . . . . . . . . . . . . . 17  |-  3  e.  NN
50 nnrp 10577 . . . . . . . . . . . . . . . . 17  |-  ( 3  e.  NN  ->  3  e.  RR+ )
5149, 50ax-mp 8 . . . . . . . . . . . . . . . 16  |-  3  e.  RR+
52 rpdivcl 10590 . . . . . . . . . . . . . . . 16  |-  ( ( v  e.  RR+  /\  3  e.  RR+ )  ->  (
v  /  3 )  e.  RR+ )
5351, 52mpan2 653 . . . . . . . . . . . . . . 15  |-  ( v  e.  RR+  ->  ( v  /  3 )  e.  RR+ )
5453ad2antlr 708 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  h  e.  dom  S.1 )  /\  v  e.  RR+ )  /\  x  e.  RR )  ->  ( v  / 
3 )  e.  RR+ )
551ad2antrr 707 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  h  e.  dom  S.1 )  /\  v  e.  RR+ )  ->  F : RR --> ( 0 [,) 
+oo ) )
5655ffvelrnda 5829 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  h  e.  dom  S.1 )  /\  v  e.  RR+ )  /\  x  e.  RR )  ->  ( F `  x )  e.  ( 0 [,)  +oo )
)
57 elrege0 10963 . . . . . . . . . . . . . . . 16  |-  ( ( F `  x )  e.  ( 0 [,) 
+oo )  <->  ( ( F `  x )  e.  RR  /\  0  <_ 
( F `  x
) ) )
5856, 57sylib 189 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  h  e.  dom  S.1 )  /\  v  e.  RR+ )  /\  x  e.  RR )  ->  ( ( F `
 x )  e.  RR  /\  0  <_ 
( F `  x
) ) )
5958simprd 450 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  h  e.  dom  S.1 )  /\  v  e.  RR+ )  /\  x  e.  RR )  ->  0  <_  ( F `  x )
)
609, 54, 59divge0d 10640 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  h  e.  dom  S.1 )  /\  v  e.  RR+ )  /\  x  e.  RR )  ->  0  <_  (
( F `  x
)  /  ( v  /  3 ) ) )
61 flge0nn0 11180 . . . . . . . . . . . . 13  |-  ( ( ( ( F `  x )  /  (
v  /  3 ) )  e.  RR  /\  0  <_  ( ( F `
 x )  / 
( v  /  3
) ) )  -> 
( |_ `  (
( F `  x
)  /  ( v  /  3 ) ) )  e.  NN0 )
6224, 60, 61syl2anc 643 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  h  e.  dom  S.1 )  /\  v  e.  RR+ )  /\  x  e.  RR )  ->  ( |_ `  ( ( F `  x )  /  (
v  /  3 ) ) )  e.  NN0 )
6362nn0ge0d 10233 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  h  e.  dom  S.1 )  /\  v  e.  RR+ )  /\  x  e.  RR )  ->  0  <_  ( |_ `  ( ( F `
 x )  / 
( v  /  3
) ) ) )
6463adantr 452 . . . . . . . . . 10  |-  ( ( ( ( ( ph  /\  h  e.  dom  S.1 )  /\  v  e.  RR+ )  /\  x  e.  RR )  /\  ( ( ( ( |_ `  (
( F `  x
)  /  ( v  /  3 ) ) )  -  1 )  x.  ( v  / 
3 ) )  <_ 
( h `  x
)  /\  ( h `  x )  =/=  0
) )  ->  0  <_  ( |_ `  (
( F `  x
)  /  ( v  /  3 ) ) ) )
65 frn 5556 . . . . . . . . . . . . . . . . 17  |-  ( h : RR --> RR  ->  ran  h  C_  RR )
6630, 65syl 16 . . . . . . . . . . . . . . . 16  |-  ( h  e.  dom  S.1  ->  ran  h  C_  RR )
67 i1f0rn 19527 . . . . . . . . . . . . . . . . . 18  |-  ( h  e.  dom  S.1  ->  0  e.  ran  h )
68 elex2 2928 . . . . . . . . . . . . . . . . . 18  |-  ( 0  e.  ran  h  ->  E. x  x  e.  ran  h )
6967, 68syl 16 . . . . . . . . . . . . . . . . 17  |-  ( h  e.  dom  S.1  ->  E. x  x  e.  ran  h )
70 n0 3597 . . . . . . . . . . . . . . . . 17  |-  ( ran  h  =/=  (/)  <->  E. x  x  e.  ran  h )
7169, 70sylibr 204 . . . . . . . . . . . . . . . 16  |-  ( h  e.  dom  S.1  ->  ran  h  =/=  (/) )
72 fimaxre2 9912 . . . . . . . . . . . . . . . . 17  |-  ( ( ran  h  C_  RR  /\ 
ran  h  e.  Fin )  ->  E. x  e.  RR  A. y  e.  ran  h  y  <_  x )
7366, 45, 72syl2anc 643 . . . . . . . . . . . . . . . 16  |-  ( h  e.  dom  S.1  ->  E. x  e.  RR  A. y  e.  ran  h  y  <_  x )
7466, 71, 733jca 1134 . . . . . . . . . . . . . . 15  |-  ( h  e.  dom  S.1  ->  ( ran  h  C_  RR  /\ 
ran  h  =/=  (/)  /\  E. x  e.  RR  A. y  e.  ran  h  y  <_  x ) )
7574ad3antlr 712 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  h  e.  dom  S.1 )  /\  v  e.  RR+ )  /\  x  e.  RR )  ->  ( ran  h  C_  RR  /\  ran  h  =/=  (/)  /\  E. x  e.  RR  A. y  e. 
ran  h  y  <_  x ) )
76 ffn 5550 . . . . . . . . . . . . . . . . . 18  |-  ( h : RR --> RR  ->  h  Fn  RR )
7730, 76syl 16 . . . . . . . . . . . . . . . . 17  |-  ( h  e.  dom  S.1  ->  h  Fn  RR )
78 dffn3 5557 . . . . . . . . . . . . . . . . 17  |-  ( h  Fn  RR  <->  h : RR
--> ran  h )
7977, 78sylib 189 . . . . . . . . . . . . . . . 16  |-  ( h  e.  dom  S.1  ->  h : RR --> ran  h
)
8079ad2antlr 708 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  h  e.  dom  S.1 )  /\  v  e.  RR+ )  ->  h : RR --> ran  h )
8180ffvelrnda 5829 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  h  e.  dom  S.1 )  /\  v  e.  RR+ )  /\  x  e.  RR )  ->  ( h `  x )  e.  ran  h )
82 suprub 9925 . . . . . . . . . . . . . 14  |-  ( ( ( ran  h  C_  RR  /\  ran  h  =/=  (/)  /\  E. x  e.  RR  A. y  e. 
ran  h  y  <_  x )  /\  (
h `  x )  e.  ran  h )  -> 
( h `  x
)  <_  sup ( ran  h ,  RR ,  <  ) )
8375, 81, 82syl2anc 643 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  h  e.  dom  S.1 )  /\  v  e.  RR+ )  /\  x  e.  RR )  ->  ( h `  x )  <_  sup ( ran  h ,  RR ,  <  ) )
84 suprcl 9924 . . . . . . . . . . . . . . . . 17  |-  ( ( ran  h  C_  RR  /\ 
ran  h  =/=  (/)  /\  E. x  e.  RR  A. y  e.  ran  h  y  <_  x )  ->  sup ( ran  h ,  RR ,  <  )  e.  RR )
8566, 71, 73, 84syl3anc 1184 . . . . . . . . . . . . . . . 16  |-  ( h  e.  dom  S.1  ->  sup ( ran  h ,  RR ,  <  )  e.  RR )
8685ad3antlr 712 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  h  e.  dom  S.1 )  /\  v  e.  RR+ )  /\  x  e.  RR )  ->  sup ( ran  h ,  RR ,  <  )  e.  RR )
87 letr 9123 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( |_
`  ( ( F `
 x )  / 
( v  /  3
) ) )  - 
1 )  x.  (
v  /  3 ) )  e.  RR  /\  ( h `  x
)  e.  RR  /\  sup ( ran  h ,  RR ,  <  )  e.  RR )  ->  (
( ( ( ( |_ `  ( ( F `  x )  /  ( v  / 
3 ) ) )  -  1 )  x.  ( v  /  3
) )  <_  (
h `  x )  /\  ( h `  x
)  <_  sup ( ran  h ,  RR ,  <  ) )  ->  (
( ( |_ `  ( ( F `  x )  /  (
v  /  3 ) ) )  -  1 )  x.  ( v  /  3 ) )  <_  sup ( ran  h ,  RR ,  <  )
) )
8829, 32, 86, 87syl3anc 1184 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  h  e.  dom  S.1 )  /\  v  e.  RR+ )  /\  x  e.  RR )  ->  ( ( ( ( ( |_ `  ( ( F `  x )  /  (
v  /  3 ) ) )  -  1 )  x.  ( v  /  3 ) )  <_  ( h `  x )  /\  (
h `  x )  <_  sup ( ran  h ,  RR ,  <  )
)  ->  ( (
( |_ `  (
( F `  x
)  /  ( v  /  3 ) ) )  -  1 )  x.  ( v  / 
3 ) )  <_  sup ( ran  h ,  RR ,  <  )
) )
8928, 86, 54lemuldivd 10649 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  h  e.  dom  S.1 )  /\  v  e.  RR+ )  /\  x  e.  RR )  ->  ( ( ( ( |_ `  (
( F `  x
)  /  ( v  /  3 ) ) )  -  1 )  x.  ( v  / 
3 ) )  <_  sup ( ran  h ,  RR ,  <  )  <->  ( ( |_ `  (
( F `  x
)  /  ( v  /  3 ) ) )  -  1 )  <_  ( sup ( ran  h ,  RR ,  <  )  /  ( v  /  3 ) ) ) )
90 1re 9046 . . . . . . . . . . . . . . . . . 18  |-  1  e.  RR
9190a1i 11 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ph  /\  h  e.  dom  S.1 )  /\  v  e.  RR+ )  /\  x  e.  RR )  ->  1  e.  RR )
9286, 17, 23redivcld 9798 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ph  /\  h  e.  dom  S.1 )  /\  v  e.  RR+ )  /\  x  e.  RR )  ->  ( sup ( ran  h ,  RR ,  <  )  /  ( v  /  3 ) )  e.  RR )
9326, 91, 92lesubaddd 9579 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  h  e.  dom  S.1 )  /\  v  e.  RR+ )  /\  x  e.  RR )  ->  ( ( ( |_ `  ( ( F `  x )  /  ( v  / 
3 ) ) )  -  1 )  <_ 
( sup ( ran  h ,  RR ,  <  )  /  ( v  /  3 ) )  <-> 
( |_ `  (
( F `  x
)  /  ( v  /  3 ) ) )  <_  ( ( sup ( ran  h ,  RR ,  <  )  /  ( v  / 
3 ) )  +  1 ) ) )
9489, 93bitrd 245 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  h  e.  dom  S.1 )  /\  v  e.  RR+ )  /\  x  e.  RR )  ->  ( ( ( ( |_ `  (
( F `  x
)  /  ( v  /  3 ) ) )  -  1 )  x.  ( v  / 
3 ) )  <_  sup ( ran  h ,  RR ,  <  )  <->  ( |_ `  ( ( F `  x )  /  ( v  / 
3 ) ) )  <_  ( ( sup ( ran  h ,  RR ,  <  )  /  ( v  / 
3 ) )  +  1 ) ) )
95 peano2re 9195 . . . . . . . . . . . . . . . . . 18  |-  ( ( sup ( ran  h ,  RR ,  <  )  /  ( v  / 
3 ) )  e.  RR  ->  ( ( sup ( ran  h ,  RR ,  <  )  /  ( v  / 
3 ) )  +  1 )  e.  RR )
9692, 95syl 16 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ph  /\  h  e.  dom  S.1 )  /\  v  e.  RR+ )  /\  x  e.  RR )  ->  ( ( sup ( ran  h ,  RR ,  <  )  /  ( v  / 
3 ) )  +  1 )  e.  RR )
97 ceige 11188 . . . . . . . . . . . . . . . . 17  |-  ( ( ( sup ( ran  h ,  RR ,  <  )  /  ( v  /  3 ) )  +  1 )  e.  RR  ->  ( ( sup ( ran  h ,  RR ,  <  )  /  ( v  / 
3 ) )  +  1 )  <_  -u ( |_ `  -u ( ( sup ( ran  h ,  RR ,  <  )  /  ( v  / 
3 ) )  +  1 ) ) )
9896, 97syl 16 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  h  e.  dom  S.1 )  /\  v  e.  RR+ )  /\  x  e.  RR )  ->  ( ( sup ( ran  h ,  RR ,  <  )  /  ( v  / 
3 ) )  +  1 )  <_  -u ( |_ `  -u ( ( sup ( ran  h ,  RR ,  <  )  /  ( v  / 
3 ) )  +  1 ) ) )
99 ceicl 11187 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( sup ( ran  h ,  RR ,  <  )  /  ( v  /  3 ) )  +  1 )  e.  RR  ->  -u ( |_
`  -u ( ( sup ( ran  h ,  RR ,  <  )  /  ( v  / 
3 ) )  +  1 ) )  e.  ZZ )
10096, 99syl 16 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ph  /\  h  e.  dom  S.1 )  /\  v  e.  RR+ )  /\  x  e.  RR )  ->  -u ( |_ `  -u ( ( sup ( ran  h ,  RR ,  <  )  /  ( v  /  3 ) )  +  1 ) )  e.  ZZ )
101100zred 10331 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ph  /\  h  e.  dom  S.1 )  /\  v  e.  RR+ )  /\  x  e.  RR )  ->  -u ( |_ `  -u ( ( sup ( ran  h ,  RR ,  <  )  /  ( v  /  3 ) )  +  1 ) )  e.  RR )
102 letr 9123 . . . . . . . . . . . . . . . . 17  |-  ( ( ( |_ `  (
( F `  x
)  /  ( v  /  3 ) ) )  e.  RR  /\  ( ( sup ( ran  h ,  RR ,  <  )  /  ( v  /  3 ) )  +  1 )  e.  RR  /\  -u ( |_ `  -u ( ( sup ( ran  h ,  RR ,  <  )  /  ( v  / 
3 ) )  +  1 ) )  e.  RR )  ->  (
( ( |_ `  ( ( F `  x )  /  (
v  /  3 ) ) )  <_  (
( sup ( ran  h ,  RR ,  <  )  /  ( v  /  3 ) )  +  1 )  /\  ( ( sup ( ran  h ,  RR ,  <  )  /  ( v  /  3 ) )  +  1 )  <_  -u ( |_ `  -u (
( sup ( ran  h ,  RR ,  <  )  /  ( v  /  3 ) )  +  1 ) ) )  ->  ( |_ `  ( ( F `  x )  /  (
v  /  3 ) ) )  <_  -u ( |_ `  -u ( ( sup ( ran  h ,  RR ,  <  )  /  ( v  / 
3 ) )  +  1 ) ) ) )
10326, 96, 101, 102syl3anc 1184 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  h  e.  dom  S.1 )  /\  v  e.  RR+ )  /\  x  e.  RR )  ->  ( ( ( |_ `  ( ( F `  x )  /  ( v  / 
3 ) ) )  <_  ( ( sup ( ran  h ,  RR ,  <  )  /  ( v  / 
3 ) )  +  1 )  /\  (
( sup ( ran  h ,  RR ,  <  )  /  ( v  /  3 ) )  +  1 )  <_  -u ( |_ `  -u (
( sup ( ran  h ,  RR ,  <  )  /  ( v  /  3 ) )  +  1 ) ) )  ->  ( |_ `  ( ( F `  x )  /  (
v  /  3 ) ) )  <_  -u ( |_ `  -u ( ( sup ( ran  h ,  RR ,  <  )  /  ( v  / 
3 ) )  +  1 ) ) ) )
10498, 103mpan2d 656 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  h  e.  dom  S.1 )  /\  v  e.  RR+ )  /\  x  e.  RR )  ->  ( ( |_
`  ( ( F `
 x )  / 
( v  /  3
) ) )  <_ 
( ( sup ( ran  h ,  RR ,  <  )  /  ( v  /  3 ) )  +  1 )  -> 
( |_ `  (
( F `  x
)  /  ( v  /  3 ) ) )  <_  -u ( |_
`  -u ( ( sup ( ran  h ,  RR ,  <  )  /  ( v  / 
3 ) )  +  1 ) ) ) )
10594, 104sylbid 207 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  h  e.  dom  S.1 )  /\  v  e.  RR+ )  /\  x  e.  RR )  ->  ( ( ( ( |_ `  (
( F `  x
)  /  ( v  /  3 ) ) )  -  1 )  x.  ( v  / 
3 ) )  <_  sup ( ran  h ,  RR ,  <  )  ->  ( |_ `  (
( F `  x
)  /  ( v  /  3 ) ) )  <_  -u ( |_
`  -u ( ( sup ( ran  h ,  RR ,  <  )  /  ( v  / 
3 ) )  +  1 ) ) ) )
10688, 105syld 42 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  h  e.  dom  S.1 )  /\  v  e.  RR+ )  /\  x  e.  RR )  ->  ( ( ( ( ( |_ `  ( ( F `  x )  /  (
v  /  3 ) ) )  -  1 )  x.  ( v  /  3 ) )  <_  ( h `  x )  /\  (
h `  x )  <_  sup ( ran  h ,  RR ,  <  )
)  ->  ( |_ `  ( ( F `  x )  /  (
v  /  3 ) ) )  <_  -u ( |_ `  -u ( ( sup ( ran  h ,  RR ,  <  )  /  ( v  / 
3 ) )  +  1 ) ) ) )
10783, 106mpan2d 656 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  h  e.  dom  S.1 )  /\  v  e.  RR+ )  /\  x  e.  RR )  ->  ( ( ( ( |_ `  (
( F `  x
)  /  ( v  /  3 ) ) )  -  1 )  x.  ( v  / 
3 ) )  <_ 
( h `  x
)  ->  ( |_ `  ( ( F `  x )  /  (
v  /  3 ) ) )  <_  -u ( |_ `  -u ( ( sup ( ran  h ,  RR ,  <  )  /  ( v  / 
3 ) )  +  1 ) ) ) )
108107adantrd 455 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  h  e.  dom  S.1 )  /\  v  e.  RR+ )  /\  x  e.  RR )  ->  ( ( ( ( ( |_ `  ( ( F `  x )  /  (
v  /  3 ) ) )  -  1 )  x.  ( v  /  3 ) )  <_  ( h `  x )  /\  (
h `  x )  =/=  0 )  ->  ( |_ `  ( ( F `
 x )  / 
( v  /  3
) ) )  <_  -u ( |_ `  -u (
( sup ( ran  h ,  RR ,  <  )  /  ( v  /  3 ) )  +  1 ) ) ) )
109108imp 419 . . . . . . . . . 10  |-  ( ( ( ( ( ph  /\  h  e.  dom  S.1 )  /\  v  e.  RR+ )  /\  x  e.  RR )  /\  ( ( ( ( |_ `  (
( F `  x
)  /  ( v  /  3 ) ) )  -  1 )  x.  ( v  / 
3 ) )  <_ 
( h `  x
)  /\  ( h `  x )  =/=  0
) )  ->  ( |_ `  ( ( F `
 x )  / 
( v  /  3
) ) )  <_  -u ( |_ `  -u (
( sup ( ran  h ,  RR ,  <  )  /  ( v  /  3 ) )  +  1 ) ) )
11024flcld 11162 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  h  e.  dom  S.1 )  /\  v  e.  RR+ )  /\  x  e.  RR )  ->  ( |_ `  ( ( F `  x )  /  (
v  /  3 ) ) )  e.  ZZ )
111110adantr 452 . . . . . . . . . . 11  |-  ( ( ( ( ( ph  /\  h  e.  dom  S.1 )  /\  v  e.  RR+ )  /\  x  e.  RR )  /\  ( ( ( ( |_ `  (
( F `  x
)  /  ( v  /  3 ) ) )  -  1 )  x.  ( v  / 
3 ) )  <_ 
( h `  x
)  /\  ( h `  x )  =/=  0
) )  ->  ( |_ `  ( ( F `
 x )  / 
( v  /  3
) ) )  e.  ZZ )
112 0z 10249 . . . . . . . . . . . 12  |-  0  e.  ZZ
113112a1i 11 . . . . . . . . . . 11  |-  ( ( ( ( ( ph  /\  h  e.  dom  S.1 )  /\  v  e.  RR+ )  /\  x  e.  RR )  /\  ( ( ( ( |_ `  (
( F `  x
)  /  ( v  /  3 ) ) )  -  1 )  x.  ( v  / 
3 ) )  <_ 
( h `  x
)  /\  ( h `  x )  =/=  0
) )  ->  0  e.  ZZ )
114100adantr 452 . . . . . . . . . . 11  |-  ( ( ( ( ( ph  /\  h  e.  dom  S.1 )  /\  v  e.  RR+ )  /\  x  e.  RR )  /\  ( ( ( ( |_ `  (
( F `  x
)  /  ( v  /  3 ) ) )  -  1 )  x.  ( v  / 
3 ) )  <_ 
( h `  x
)  /\  ( h `  x )  =/=  0
) )  ->  -u ( |_ `  -u ( ( sup ( ran  h ,  RR ,  <  )  /  ( v  / 
3 ) )  +  1 ) )  e.  ZZ )
115 elfz 11005 . . . . . . . . . . 11  |-  ( ( ( |_ `  (
( F `  x
)  /  ( v  /  3 ) ) )  e.  ZZ  /\  0  e.  ZZ  /\  -u ( |_ `  -u ( ( sup ( ran  h ,  RR ,  <  )  /  ( v  / 
3 ) )  +  1 ) )  e.  ZZ )  ->  (
( |_ `  (
( F `  x
)  /  ( v  /  3 ) ) )  e.  ( 0 ... -u ( |_ `  -u ( ( sup ( ran  h ,  RR ,  <  )  /  ( v  /  3 ) )  +  1 ) ) )  <->  ( 0  <_ 
( |_ `  (
( F `  x
)  /  ( v  /  3 ) ) )  /\  ( |_
`  ( ( F `
 x )  / 
( v  /  3
) ) )  <_  -u ( |_ `  -u (
( sup ( ran  h ,  RR ,  <  )  /  ( v  /  3 ) )  +  1 ) ) ) ) )
116111, 113, 114, 115syl3anc 1184 . . . . . . . . . 10  |-  ( ( ( ( ( ph  /\  h  e.  dom  S.1 )  /\  v  e.  RR+ )  /\  x  e.  RR )  /\  ( ( ( ( |_ `  (
( F `  x
)  /  ( v  /  3 ) ) )  -  1 )  x.  ( v  / 
3 ) )  <_ 
( h `  x
)  /\  ( h `  x )  =/=  0
) )  ->  (
( |_ `  (
( F `  x
)  /  ( v  /  3 ) ) )  e.  ( 0 ... -u ( |_ `  -u ( ( sup ( ran  h ,  RR ,  <  )  /  ( v  /  3 ) )  +  1 ) ) )  <->  ( 0  <_ 
( |_ `  (
( F `  x
)  /  ( v  /  3 ) ) )  /\  ( |_
`  ( ( F `
 x )  / 
( v  /  3
) ) )  <_  -u ( |_ `  -u (
( sup ( ran  h ,  RR ,  <  )  /  ( v  /  3 ) )  +  1 ) ) ) ) )
11764, 109, 116mpbir2and 889 . . . . . . . . 9  |-  ( ( ( ( ( ph  /\  h  e.  dom  S.1 )  /\  v  e.  RR+ )  /\  x  e.  RR )  /\  ( ( ( ( |_ `  (
( F `  x
)  /  ( v  /  3 ) ) )  -  1 )  x.  ( v  / 
3 ) )  <_ 
( h `  x
)  /\  ( h `  x )  =/=  0
) )  ->  ( |_ `  ( ( F `
 x )  / 
( v  /  3
) ) )  e.  ( 0 ... -u ( |_ `  -u ( ( sup ( ran  h ,  RR ,  <  )  /  ( v  / 
3 ) )  +  1 ) ) ) )
118 eqid 2404 . . . . . . . . 9  |-  ( ( ( |_ `  (
( F `  x
)  /  ( v  /  3 ) ) )  -  1 )  x.  ( v  / 
3 ) )  =  ( ( ( |_
`  ( ( F `
 x )  / 
( v  /  3
) ) )  - 
1 )  x.  (
v  /  3 ) )
119 oveq1 6047 . . . . . . . . . . . 12  |-  ( t  =  ( |_ `  ( ( F `  x )  /  (
v  /  3 ) ) )  ->  (
t  -  1 )  =  ( ( |_
`  ( ( F `
 x )  / 
( v  /  3
) ) )  - 
1 ) )
120119oveq1d 6055 . . . . . . . . . . 11  |-  ( t  =  ( |_ `  ( ( F `  x )  /  (
v  /  3 ) ) )  ->  (
( t  -  1 )  x.  ( v  /  3 ) )  =  ( ( ( |_ `  ( ( F `  x )  /  ( v  / 
3 ) ) )  -  1 )  x.  ( v  /  3
) ) )
121120eqeq2d 2415 . . . . . . . . . 10  |-  ( t  =  ( |_ `  ( ( F `  x )  /  (
v  /  3 ) ) )  ->  (
( ( ( |_
`  ( ( F `
 x )  / 
( v  /  3
) ) )  - 
1 )  x.  (
v  /  3 ) )  =  ( ( t  -  1 )  x.  ( v  / 
3 ) )  <->  ( (
( |_ `  (
( F `  x
)  /  ( v  /  3 ) ) )  -  1 )  x.  ( v  / 
3 ) )  =  ( ( ( |_
`  ( ( F `
 x )  / 
( v  /  3
) ) )  - 
1 )  x.  (
v  /  3 ) ) ) )
122121rspcev 3012 . . . . . . . . 9  |-  ( ( ( |_ `  (
( F `  x
)  /  ( v  /  3 ) ) )  e.  ( 0 ... -u ( |_ `  -u ( ( sup ( ran  h ,  RR ,  <  )  /  ( v  /  3 ) )  +  1 ) ) )  /\  ( ( ( |_ `  (
( F `  x
)  /  ( v  /  3 ) ) )  -  1 )  x.  ( v  / 
3 ) )  =  ( ( ( |_
`  ( ( F `
 x )  / 
( v  /  3
) ) )  - 
1 )  x.  (
v  /  3 ) ) )  ->  E. t  e.  ( 0 ... -u ( |_ `  -u ( ( sup ( ran  h ,  RR ,  <  )  /  ( v  / 
3 ) )  +  1 ) ) ) ( ( ( |_
`  ( ( F `
 x )  / 
( v  /  3
) ) )  - 
1 )  x.  (
v  /  3 ) )  =  ( ( t  -  1 )  x.  ( v  / 
3 ) ) )
123117, 118, 122sylancl 644 . . . . . . . 8  |-  ( ( ( ( ( ph  /\  h  e.  dom  S.1 )  /\  v  e.  RR+ )  /\  x  e.  RR )  /\  ( ( ( ( |_ `  (
( F `  x
)  /  ( v  /  3 ) ) )  -  1 )  x.  ( v  / 
3 ) )  <_ 
( h `  x
)  /\  ( h `  x )  =/=  0
) )  ->  E. t  e.  ( 0 ... -u ( |_ `  -u ( ( sup ( ran  h ,  RR ,  <  )  /  ( v  / 
3 ) )  +  1 ) ) ) ( ( ( |_
`  ( ( F `
 x )  / 
( v  /  3
) ) )  - 
1 )  x.  (
v  /  3 ) )  =  ( ( t  -  1 )  x.  ( v  / 
3 ) ) )
124 ovex 6065 . . . . . . . . 9  |-  ( ( ( |_ `  (
( F `  x
)  /  ( v  /  3 ) ) )  -  1 )  x.  ( v  / 
3 ) )  e. 
_V
12539elrnmpt 5076 . . . . . . . . 9  |-  ( ( ( ( |_ `  ( ( F `  x )  /  (
v  /  3 ) ) )  -  1 )  x.  ( v  /  3 ) )  e.  _V  ->  (
( ( ( |_
`  ( ( F `
 x )  / 
( v  /  3
) ) )  - 
1 )  x.  (
v  /  3 ) )  e.  ran  (
t  e.  ( 0 ... -u ( |_ `  -u ( ( sup ( ran  h ,  RR ,  <  )  /  ( v  /  3 ) )  +  1 ) ) )  |->  ( ( t  -  1 )  x.  ( v  /  3
) ) )  <->  E. t  e.  ( 0 ... -u ( |_ `  -u ( ( sup ( ran  h ,  RR ,  <  )  /  ( v  / 
3 ) )  +  1 ) ) ) ( ( ( |_
`  ( ( F `
 x )  / 
( v  /  3
) ) )  - 
1 )  x.  (
v  /  3 ) )  =  ( ( t  -  1 )  x.  ( v  / 
3 ) ) ) )
126124, 125ax-mp 8 . . . . . . . 8  |-  ( ( ( ( |_ `  ( ( F `  x )  /  (
v  /  3 ) ) )  -  1 )  x.  ( v  /  3 ) )  e.  ran  ( t  e.  ( 0 ... -u ( |_ `  -u (
( sup ( ran  h ,  RR ,  <  )  /  ( v  /  3 ) )  +  1 ) ) )  |->  ( ( t  -  1 )  x.  ( v  /  3
) ) )  <->  E. t  e.  ( 0 ... -u ( |_ `  -u ( ( sup ( ran  h ,  RR ,  <  )  /  ( v  / 
3 ) )  +  1 ) ) ) ( ( ( |_
`  ( ( F `
 x )  / 
( v  /  3
) ) )  - 
1 )  x.  (
v  /  3 ) )  =  ( ( t  -  1 )  x.  ( v  / 
3 ) ) )
127123, 126sylibr 204 . . . . . . 7  |-  ( ( ( ( ( ph  /\  h  e.  dom  S.1 )  /\  v  e.  RR+ )  /\  x  e.  RR )  /\  ( ( ( ( |_ `  (
( F `  x
)  /  ( v  /  3 ) ) )  -  1 )  x.  ( v  / 
3 ) )  <_ 
( h `  x
)  /\  ( h `  x )  =/=  0
) )  ->  (
( ( |_ `  ( ( F `  x )  /  (
v  /  3 ) ) )  -  1 )  x.  ( v  /  3 ) )  e.  ran  ( t  e.  ( 0 ... -u ( |_ `  -u (
( sup ( ran  h ,  RR ,  <  )  /  ( v  /  3 ) )  +  1 ) ) )  |->  ( ( t  -  1 )  x.  ( v  /  3
) ) ) )
128 elun1 3474 . . . . . . 7  |-  ( ( ( ( |_ `  ( ( F `  x )  /  (
v  /  3 ) ) )  -  1 )  x.  ( v  /  3 ) )  e.  ran  ( t  e.  ( 0 ... -u ( |_ `  -u (
( sup ( ran  h ,  RR ,  <  )  /  ( v  /  3 ) )  +  1 ) ) )  |->  ( ( t  -  1 )  x.  ( v  /  3
) ) )  -> 
( ( ( |_
`  ( ( F `
 x )  / 
( v  /  3
) ) )  - 
1 )  x.  (
v  /  3 ) )  e.  ( ran  ( t  e.  ( 0 ... -u ( |_ `  -u ( ( sup ( ran  h ,  RR ,  <  )  /  ( v  / 
3 ) )  +  1 ) ) ) 
|->  ( ( t  - 
1 )  x.  (
v  /  3 ) ) )  u.  ran  h ) )
129127, 128syl 16 . . . . . 6  |-  ( ( ( ( ( ph  /\  h  e.  dom  S.1 )  /\  v  e.  RR+ )  /\  x  e.  RR )  /\  ( ( ( ( |_ `  (
( F `  x
)  /  ( v  /  3 ) ) )  -  1 )  x.  ( v  / 
3 ) )  <_ 
( h `  x
)  /\  ( h `  x )  =/=  0
) )  ->  (
( ( |_ `  ( ( F `  x )  /  (
v  /  3 ) ) )  -  1 )  x.  ( v  /  3 ) )  e.  ( ran  (
t  e.  ( 0 ... -u ( |_ `  -u ( ( sup ( ran  h ,  RR ,  <  )  /  ( v  /  3 ) )  +  1 ) ) )  |->  ( ( t  -  1 )  x.  ( v  /  3
) ) )  u. 
ran  h ) )
130 elun2 3475 . . . . . . . 8  |-  ( ( h `  x )  e.  ran  h  -> 
( h `  x
)  e.  ( ran  ( t  e.  ( 0 ... -u ( |_ `  -u ( ( sup ( ran  h ,  RR ,  <  )  /  ( v  / 
3 ) )  +  1 ) ) ) 
|->  ( ( t  - 
1 )  x.  (
v  /  3 ) ) )  u.  ran  h ) )
13181, 130syl 16 . . . . . . 7  |-  ( ( ( ( ph  /\  h  e.  dom  S.1 )  /\  v  e.  RR+ )  /\  x  e.  RR )  ->  ( h `  x )  e.  ( ran  ( t  e.  ( 0 ... -u ( |_ `  -u ( ( sup ( ran  h ,  RR ,  <  )  /  ( v  / 
3 ) )  +  1 ) ) ) 
|->  ( ( t  - 
1 )  x.  (
v  /  3 ) ) )  u.  ran  h ) )
132131adantr 452 . . . . . 6  |-  ( ( ( ( ( ph  /\  h  e.  dom  S.1 )  /\  v  e.  RR+ )  /\  x  e.  RR )  /\  -.  ( ( ( ( |_ `  ( ( F `  x )  /  (
v  /  3 ) ) )  -  1 )  x.  ( v  /  3 ) )  <_  ( h `  x )  /\  (
h `  x )  =/=  0 ) )  -> 
( h `  x
)  e.  ( ran  ( t  e.  ( 0 ... -u ( |_ `  -u ( ( sup ( ran  h ,  RR ,  <  )  /  ( v  / 
3 ) )  +  1 ) ) ) 
|->  ( ( t  - 
1 )  x.  (
v  /  3 ) ) )  u.  ran  h ) )
133129, 132ifclda 3726 . . . . 5  |-  ( ( ( ( ph  /\  h  e.  dom  S.1 )  /\  v  e.  RR+ )  /\  x  e.  RR )  ->  if ( ( ( ( ( |_
`  ( ( F `
 x )  / 
( v  /  3
) ) )  - 
1 )  x.  (
v  /  3 ) )  <_  ( h `  x )  /\  (
h `  x )  =/=  0 ) ,  ( ( ( |_ `  ( ( F `  x )  /  (
v  /  3 ) ) )  -  1 )  x.  ( v  /  3 ) ) ,  ( h `  x ) )  e.  ( ran  ( t  e.  ( 0 ... -u ( |_ `  -u (
( sup ( ran  h ,  RR ,  <  )  /  ( v  /  3 ) )  +  1 ) ) )  |->  ( ( t  -  1 )  x.  ( v  /  3
) ) )  u. 
ran  h ) )
134133, 35fmptd 5852 . . . 4  |-  ( ( ( ph  /\  h  e.  dom  S.1 )  /\  v  e.  RR+ )  ->  (
x  e.  RR  |->  if ( ( ( ( ( |_ `  (
( F `  x
)  /  ( v  /  3 ) ) )  -  1 )  x.  ( v  / 
3 ) )  <_ 
( h `  x
)  /\  ( h `  x )  =/=  0
) ,  ( ( ( |_ `  (
( F `  x
)  /  ( v  /  3 ) ) )  -  1 )  x.  ( v  / 
3 ) ) ,  ( h `  x
) ) ) : RR --> ( ran  (
t  e.  ( 0 ... -u ( |_ `  -u ( ( sup ( ran  h ,  RR ,  <  )  /  ( v  /  3 ) )  +  1 ) ) )  |->  ( ( t  -  1 )  x.  ( v  /  3
) ) )  u. 
ran  h ) )
135 frn 5556 . . . 4  |-  ( ( x  e.  RR  |->  if ( ( ( ( ( |_ `  (
( F `  x
)  /  ( v  /  3 ) ) )  -  1 )  x.  ( v  / 
3 ) )  <_ 
( h `  x
)  /\  ( h `  x )  =/=  0
) ,  ( ( ( |_ `  (
( F `  x
)  /  ( v  /  3 ) ) )  -  1 )  x.  ( v  / 
3 ) ) ,  ( h `  x
) ) ) : RR --> ( ran  (
t  e.  ( 0 ... -u ( |_ `  -u ( ( sup ( ran  h ,  RR ,  <  )  /  ( v  /  3 ) )  +  1 ) ) )  |->  ( ( t  -  1 )  x.  ( v  /  3
) ) )  u. 
ran  h )  ->  ran  ( x  e.  RR  |->  if ( ( ( ( ( |_ `  (
( F `  x
)  /  ( v  /  3 ) ) )  -  1 )  x.  ( v  / 
3 ) )  <_ 
( h `  x
)  /\  ( h `  x )  =/=  0
) ,  ( ( ( |_ `  (
( F `  x
)  /  ( v  /  3 ) ) )  -  1 )  x.  ( v  / 
3 ) ) ,  ( h `  x
) ) )  C_  ( ran  ( t  e.  ( 0 ... -u ( |_ `  -u ( ( sup ( ran  h ,  RR ,  <  )  /  ( v  / 
3 ) )  +  1 ) ) ) 
|->  ( ( t  - 
1 )  x.  (
v  /  3 ) ) )  u.  ran  h ) )
136134, 135syl 16 . . 3  |-  ( ( ( ph  /\  h  e.  dom  S.1 )  /\  v  e.  RR+ )  ->  ran  ( x  e.  RR  |->  if ( ( ( ( ( |_ `  (
( F `  x
)  /  ( v  /  3 ) ) )  -  1 )  x.  ( v  / 
3 ) )  <_ 
( h `  x
)  /\  ( h `  x )  =/=  0
) ,  ( ( ( |_ `  (
( F `  x
)  /  ( v  /  3 ) ) )  -  1 )  x.  ( v  / 
3 ) ) ,  ( h `  x
) ) )  C_  ( ran  ( t  e.  ( 0 ... -u ( |_ `  -u ( ( sup ( ran  h ,  RR ,  <  )  /  ( v  / 
3 ) )  +  1 ) ) ) 
|->  ( ( t  - 
1 )  x.  (
v  /  3 ) ) )  u.  ran  h ) )
137 ssfi 7288 . . 3  |-  ( ( ( ran  ( t  e.  ( 0 ... -u ( |_ `  -u (
( sup ( ran  h ,  RR ,  <  )  /  ( v  /  3 ) )  +  1 ) ) )  |->  ( ( t  -  1 )  x.  ( v  /  3
) ) )  u. 
ran  h )  e. 
Fin  /\  ran  ( x  e.  RR  |->  if ( ( ( ( ( |_ `  ( ( F `  x )  /  ( v  / 
3 ) ) )  -  1 )  x.  ( v  /  3
) )  <_  (
h `  x )  /\  ( h `  x
)  =/=  0 ) ,  ( ( ( |_ `  ( ( F `  x )  /  ( v  / 
3 ) ) )  -  1 )  x.  ( v  /  3
) ) ,  ( h `  x ) ) )  C_  ( ran  ( t  e.  ( 0 ... -u ( |_ `  -u ( ( sup ( ran  h ,  RR ,  <  )  /  ( v  / 
3 ) )  +  1 ) ) ) 
|->  ( ( t  - 
1 )  x.  (
v  /  3 ) ) )  u.  ran  h ) )  ->  ran  ( x  e.  RR  |->  if ( ( ( ( ( |_ `  (
( F `  x
)  /  ( v  /  3 ) ) )  -  1 )  x.  ( v  / 
3 ) )  <_ 
( h `  x
)  /\  ( h `  x )  =/=  0
) ,  ( ( ( |_ `  (
( F `  x
)  /  ( v  /  3 ) ) )  -  1 )  x.  ( v  / 
3 ) ) ,  ( h `  x
) ) )  e. 
Fin )
13848, 136, 137syl2anc 643 . 2  |-  ( ( ( ph  /\  h  e.  dom  S.1 )  /\  v  e.  RR+ )  ->  ran  ( x  e.  RR  |->  if ( ( ( ( ( |_ `  (
( F `  x
)  /  ( v  /  3 ) ) )  -  1 )  x.  ( v  / 
3 ) )  <_ 
( h `  x
)  /\  ( h `  x )  =/=  0
) ,  ( ( ( |_ `  (
( F `  x
)  /  ( v  /  3 ) ) )  -  1 )  x.  ( v  / 
3 ) ) ,  ( h `  x
) ) )  e. 
Fin )
13935mptpreima 5322 . . . 4  |-  ( `' ( x  e.  RR  |->  if ( ( ( ( ( |_ `  (
( F `  x
)  /  ( v  /  3 ) ) )  -  1 )  x.  ( v  / 
3 ) )  <_ 
( h `  x
)  /\  ( h `  x )  =/=  0
) ,  ( ( ( |_ `  (
( F `  x
)  /  ( v  /  3 ) ) )  -  1 )  x.  ( v  / 
3 ) ) ,  ( h `  x
) ) ) " { t } )  =  { x  e.  RR  |  if ( ( ( ( ( |_ `  ( ( F `  x )  /  ( v  / 
3 ) ) )  -  1 )  x.  ( v  /  3
) )  <_  (
h `  x )  /\  ( h `  x
)  =/=  0 ) ,  ( ( ( |_ `  ( ( F `  x )  /  ( v  / 
3 ) ) )  -  1 )  x.  ( v  /  3
) ) ,  ( h `  x ) )  e.  { t } }
140 unrab 3572 . . . . 5  |-  ( { x  e.  RR  | 
( ( ( ( ( |_ `  (
( F `  x
)  /  ( v  /  3 ) ) )  -  1 )  x.  ( v  / 
3 ) )  <_ 
( h `  x
)  /\  ( h `  x )  =/=  0
)  /\  t  =  ( ( ( |_
`  ( ( F `
 x )  / 
( v  /  3
) ) )  - 
1 )  x.  (
v  /  3 ) ) ) }  u.  { x  e.  RR  | 
( ( -.  (
( ( |_ `  ( ( F `  x )  /  (
v  /  3 ) ) )  -  1 )  x.  ( v  /  3 ) )  <_  ( h `  x )  \/  (
h `  x )  =  0 )  /\  t  =  ( h `  x ) ) } )  =  { x  e.  RR  |  ( ( ( ( ( ( |_ `  ( ( F `  x )  /  ( v  / 
3 ) ) )  -  1 )  x.  ( v  /  3
) )  <_  (
h `  x )  /\  ( h `  x
)  =/=  0 )  /\  t  =  ( ( ( |_ `  ( ( F `  x )  /  (
v  /  3 ) ) )  -  1 )  x.  ( v  /  3 ) ) )  \/  ( ( -.  ( ( ( |_ `  ( ( F `  x )  /  ( v  / 
3 ) ) )  -  1 )  x.  ( v  /  3
) )  <_  (
h `  x )  \/  ( h `  x
)  =  0 )  /\  t  =  ( h `  x ) ) ) }
141 inrab 3573 . . . . . . . 8  |-  ( { x  e.  RR  | 
( ( ( |_
`  ( ( F `
 x )  / 
( v  /  3
) ) )  - 
1 )  x.  (
v  /  3 ) )  <_  ( h `  x ) }  i^i  { x  e.  RR  | 
( h `  x
)  =/=  0 } )  =  { x  e.  RR  |  ( ( ( ( |_ `  ( ( F `  x )  /  (
v  /  3 ) ) )  -  1 )  x.  ( v  /  3 ) )  <_  ( h `  x )  /\  (
h `  x )  =/=  0 ) }
142141ineq1i 3498 . . . . . . 7  |-  ( ( { x  e.  RR  |  ( ( ( |_ `  ( ( F `  x )  /  ( v  / 
3 ) ) )  -  1 )  x.  ( v  /  3
) )  <_  (
h `  x ) }  i^i  { x  e.  RR  |  ( h `
 x )  =/=  0 } )  i^i 
{ x  e.  RR  |  t  =  (
( ( |_ `  ( ( F `  x )  /  (
v  /  3 ) ) )  -  1 )  x.  ( v  /  3 ) ) } )  =  ( { x  e.  RR  |  ( ( ( ( |_ `  (
( F `  x
)  /  ( v  /  3 ) ) )  -  1 )  x.  ( v  / 
3 ) )  <_ 
( h `  x
)  /\  ( h `  x )  =/=  0
) }  i^i  {
x  e.  RR  | 
t  =  ( ( ( |_ `  (
( F `  x
)  /  ( v  /  3 ) ) )  -  1 )  x.  ( v  / 
3 ) ) } )
143 inrab 3573 . . . . . . 7  |-  ( { x  e.  RR  | 
( ( ( ( |_ `  ( ( F `  x )  /  ( v  / 
3 ) ) )  -  1 )  x.  ( v  /  3
) )  <_  (
h `  x )  /\  ( h `  x
)  =/=  0 ) }  i^i  { x  e.  RR  |  t  =  ( ( ( |_
`  ( ( F `
 x )  / 
( v  /  3
) ) )  - 
1 )  x.  (
v  /  3 ) ) } )  =  { x  e.  RR  |  ( ( ( ( ( |_ `  ( ( F `  x )  /  (
v  /  3 ) ) )  -  1 )  x.  ( v  /  3 ) )  <_  ( h `  x )  /\  (
h `  x )  =/=  0 )  /\  t  =  ( ( ( |_ `  ( ( F `  x )  /  ( v  / 
3 ) ) )  -  1 )  x.  ( v  /  3
) ) ) }
144142, 143eqtri 2424 . . . . . 6  |-  ( ( { x  e.  RR  |  ( ( ( |_ `  ( ( F `  x )  /  ( v  / 
3 ) ) )  -  1 )  x.  ( v  /  3
) )  <_  (
h `  x ) }  i^i  { x  e.  RR  |  ( h `
 x )  =/=  0 } )  i^i 
{ x  e.  RR  |  t  =  (
( ( |_ `  ( ( F `  x )  /  (
v  /  3 ) ) )  -  1 )  x.  ( v  /  3 ) ) } )  =  {
x  e.  RR  | 
( ( ( ( ( |_ `  (
( F `  x
)  /  ( v  /  3 ) ) )  -  1 )  x.  ( v  / 
3 ) )  <_ 
( h `  x
)  /\  ( h `  x )  =/=  0
)  /\  t  =  ( ( ( |_
`  ( ( F `
 x )  / 
( v  /  3
) ) )  - 
1 )  x.  (
v  /  3 ) ) ) }
145 unrab 3572 . . . . . . . 8  |-  ( { x  e.  RR  |  -.  ( ( ( |_
`  ( ( F `
 x )  / 
( v  /  3
) ) )  - 
1 )  x.  (
v  /  3 ) )  <_  ( h `  x ) }  u.  { x  e.  RR  | 
( h `  x
)  =  0 } )  =  { x  e.  RR  |  ( -.  ( ( ( |_
`  ( ( F `
 x )  / 
( v  /  3
) ) )  - 
1 )  x.  (
v  /  3 ) )  <_  ( h `  x )  \/  (
h `  x )  =  0 ) }
146145ineq1i 3498 . . . . . . 7  |-  ( ( { x  e.  RR  |  -.  ( ( ( |_ `  ( ( F `  x )  /  ( v  / 
3 ) ) )  -  1 )  x.  ( v  /  3
) )  <_  (
h `  x ) }  u.  { x  e.  RR  |  ( h `
 x )  =  0 } )  i^i 
{ x  e.  RR  |  t  =  (
h `  x ) } )  =  ( { x  e.  RR  |  ( -.  (
( ( |_ `  ( ( F `  x )  /  (
v  /  3 ) ) )  -  1 )  x.  ( v  /  3 ) )  <_  ( h `  x )  \/  (
h `  x )  =  0 ) }  i^i  { x  e.  RR  |  t  =  ( h `  x
) } )
147 inrab 3573 . . . . . . 7  |-  ( { x  e.  RR  | 
( -.  ( ( ( |_ `  (
( F `  x
)  /  ( v  /  3 ) ) )  -  1 )  x.  ( v  / 
3 ) )  <_ 
( h `  x
)  \/  ( h `
 x )  =  0 ) }  i^i  { x  e.  RR  | 
t  =  ( h `
 x ) } )  =  { x  e.  RR  |  ( ( -.  ( ( ( |_ `  ( ( F `  x )  /  ( v  / 
3 ) ) )  -  1 )  x.  ( v  /  3
) )  <_  (
h `  x )  \/  ( h `  x
)  =  0 )  /\  t  =  ( h `  x ) ) }
148146, 147eqtri 2424 . . . . . 6  |-  ( ( { x  e.  RR  |  -.  ( ( ( |_ `  ( ( F `  x )  /  ( v  / 
3 ) ) )  -  1 )  x.  ( v  /  3
) )  <_  (
h `  x ) }  u.  { x  e.  RR  |  ( h `
 x )  =  0 } )  i^i 
{ x  e.  RR  |  t  =  (
h `  x ) } )  =  {
x  e.  RR  | 
( ( -.  (
( ( |_ `  ( ( F `  x )  /  (
v  /  3 ) ) )  -  1 )  x.  ( v  /  3 ) )  <_  ( h `  x )  \/  (
h `  x )  =  0 )  /\  t  =  ( h `  x ) ) }
149144, 148uneq12i 3459 . . . . 5  |-  ( ( ( { x  e.  RR  |  ( ( ( |_ `  (
( F `  x
)  /  ( v  /  3 ) ) )  -  1 )  x.  ( v  / 
3 ) )  <_ 
( h `  x
) }  i^i  {
x  e.  RR  | 
( h `  x
)  =/=  0 } )  i^i  { x  e.  RR  |  t  =  ( ( ( |_
`  ( ( F `
 x )  / 
( v  /  3
) ) )  - 
1 )  x.  (
v  /  3 ) ) } )  u.  ( ( { x  e.  RR  |  -.  (
( ( |_ `  ( ( F `  x )  /  (
v  /  3 ) ) )  -  1 )  x.  ( v  /  3 ) )  <_  ( h `  x ) }  u.  { x  e.  RR  | 
( h `  x
)  =  0 } )  i^i  { x  e.  RR  |  t  =  ( h `  x
) } ) )  =  ( { x  e.  RR  |  ( ( ( ( ( |_
`  ( ( F `
 x )  / 
( v  /  3
) ) )  - 
1 )  x.  (
v  /  3 ) )  <_  ( h `  x )  /\  (
h `  x )  =/=  0 )  /\  t  =  ( ( ( |_ `  ( ( F `  x )  /  ( v  / 
3 ) ) )  -  1 )  x.  ( v  /  3
) ) ) }  u.  { x  e.  RR  |  ( ( -.  ( ( ( |_ `  ( ( F `  x )  /  ( v  / 
3 ) ) )  -  1 )  x.  ( v  /  3
) )  <_  (
h `  x )  \/  ( h `  x
)  =  0 )  /\  t  =  ( h `  x ) ) } )
150 eqcom 2406 . . . . . . . 8  |-  ( if ( ( ( ( ( |_ `  (
( F `  x
)  /  ( v  /  3 ) ) )  -  1 )  x.  ( v  / 
3 ) )  <_ 
( h `  x
)  /\  ( h `  x )  =/=  0
) ,  ( ( ( |_ `  (
( F `  x
)  /  ( v  /  3 ) ) )  -  1 )  x.  ( v  / 
3 ) ) ,  ( h `  x
) )  =  t  <-> 
t  =  if ( ( ( ( ( |_ `  ( ( F `  x )  /  ( v  / 
3 ) ) )  -  1 )  x.  ( v  /  3
) )  <_  (
h `  x )  /\  ( h `  x
)  =/=  0 ) ,  ( ( ( |_ `  ( ( F `  x )  /  ( v  / 
3 ) ) )  -  1 )  x.  ( v  /  3
) ) ,  ( h `  x ) ) )
151 fvex 5701 . . . . . . . . . 10  |-  ( h `
 x )  e. 
_V
152124, 151ifex 3757 . . . . . . . . 9  |-  if ( ( ( ( ( |_ `  ( ( F `  x )  /  ( v  / 
3 ) ) )  -  1 )  x.  ( v  /  3
) )  <_  (
h `  x )  /\  ( h `  x
)  =/=  0 ) ,  ( ( ( |_ `  ( ( F `  x )  /  ( v  / 
3 ) ) )  -  1 )  x.  ( v  /  3
) ) ,  ( h `  x ) )  e.  _V
153152elsnc 3797 . . . . . . . 8  |-  ( if ( ( ( ( ( |_ `  (
( F `  x
)  /  ( v  /  3 ) ) )  -  1 )  x.  ( v  / 
3 ) )  <_ 
( h `  x
)  /\  ( h `  x )  =/=  0
) ,  ( ( ( |_ `  (
( F `  x
)  /  ( v  /  3 ) ) )  -  1 )  x.  ( v  / 
3 ) ) ,  ( h `  x
) )  e.  {
t }  <->  if (
( ( ( ( |_ `  ( ( F `  x )  /  ( v  / 
3 ) ) )  -  1 )  x.  ( v  /  3
) )  <_  (
h `  x )  /\  ( h `  x
)  =/=  0 ) ,  ( ( ( |_ `  ( ( F `  x )  /  ( v  / 
3 ) ) )  -  1 )  x.  ( v  /  3
) ) ,  ( h `  x ) )  =  t )
154 ianor 475 . . . . . . . . . . . 12  |-  ( -.  ( ( ( ( |_ `  ( ( F `  x )  /  ( v  / 
3 ) ) )  -  1 )  x.  ( v  /  3
) )  <_  (
h `  x )  /\  ( h `  x
)  =/=  0 )  <-> 
( -.  ( ( ( |_ `  (
( F `  x
)  /  ( v  /  3 ) ) )  -  1 )  x.  ( v  / 
3 ) )  <_ 
( h `  x
)  \/  -.  (
h `  x )  =/=  0 ) )
155 nne 2571 . . . . . . . . . . . . 13  |-  ( -.  ( h `  x
)  =/=  0  <->  (
h `  x )  =  0 )
156155orbi2i 506 . . . . . . . . . . . 12  |-  ( ( -.  ( ( ( |_ `  ( ( F `  x )  /  ( v  / 
3 ) ) )  -  1 )  x.  ( v  /  3
) )  <_  (
h `  x )  \/  -.  ( h `  x )  =/=  0
)  <->  ( -.  (
( ( |_ `  ( ( F `  x )  /  (
v  /  3 ) ) )  -  1 )  x.  ( v  /  3 ) )  <_  ( h `  x )  \/  (
h `  x )  =  0 ) )
157154, 156bitr2i 242 . . . . . . . . . . 11  |-  ( ( -.  ( ( ( |_ `  ( ( F `  x )  /  ( v  / 
3 ) ) )  -  1 )  x.  ( v  /  3
) )  <_  (
h `  x )  \/  ( h `  x
)  =  0 )  <->  -.  ( ( ( ( |_ `  ( ( F `  x )  /  ( v  / 
3 ) ) )  -  1 )  x.  ( v  /  3
) )  <_  (
h `  x )  /\  ( h `  x
)  =/=  0 ) )
158157anbi1i 677 . . . . . . . . . 10  |-  ( ( ( -.  ( ( ( |_ `  (
( F `  x
)  /  ( v  /  3 ) ) )  -  1 )  x.  ( v  / 
3 ) )  <_ 
( h `  x
)  \/  ( h `
 x )  =  0 )  /\  t  =  ( h `  x ) )  <->  ( -.  ( ( ( ( |_ `  ( ( F `  x )  /  ( v  / 
3 ) ) )  -  1 )  x.  ( v  /  3
) )  <_  (
h `  x )  /\  ( h `  x
)  =/=  0 )  /\  t  =  ( h `  x ) ) )
159158orbi2i 506 . . . . . . . . 9  |-  ( ( ( ( ( ( ( |_ `  (
( F `  x
)  /  ( v  /  3 ) ) )  -  1 )  x.  ( v  / 
3 ) )  <_ 
( h `  x
)  /\  ( h `  x )  =/=  0
)  /\  t  =  ( ( ( |_
`  ( ( F `
 x )  / 
( v  /  3
) ) )  - 
1 )  x.  (
v  /  3 ) ) )  \/  (
( -.  ( ( ( |_ `  (
( F `  x
)  /  ( v  /  3 ) ) )  -  1 )  x.  ( v  / 
3 ) )  <_ 
( h `  x
)  \/  ( h `
 x )  =  0 )  /\  t  =  ( h `  x ) ) )  <-> 
( ( ( ( ( ( |_ `  ( ( F `  x )  /  (
v  /  3 ) ) )  -  1 )  x.  ( v  /  3 ) )  <_  ( h `  x )  /\  (
h `  x )  =/=  0 )  /\  t  =  ( ( ( |_ `  ( ( F `  x )  /  ( v  / 
3 ) ) )  -  1 )  x.  ( v  /  3
) ) )  \/  ( -.  ( ( ( ( |_ `  ( ( F `  x )  /  (
v  /  3 ) ) )  -  1 )  x.  ( v  /  3 ) )  <_  ( h `  x )  /\  (
h `  x )  =/=  0 )  /\  t  =  ( h `  x ) ) ) )
160 eqif 3732 . . . . . . . . 9  |-  ( t  =  if ( ( ( ( ( |_
`  ( ( F `
 x )  / 
( v  /  3
) ) )  - 
1 )  x.  (
v  /  3 ) )  <_  ( h `  x )  /\  (
h `  x )  =/=  0 ) ,  ( ( ( |_ `  ( ( F `  x )  /  (
v  /  3 ) ) )  -  1 )  x.  ( v  /  3 ) ) ,  ( h `  x ) )  <->  ( (
( ( ( ( |_ `  ( ( F `  x )  /  ( v  / 
3 ) ) )  -  1 )  x.  ( v  /  3
) )  <_  (
h `  x )  /\  ( h `  x
)  =/=  0 )  /\  t  =  ( ( ( |_ `  ( ( F `  x )  /  (
v  /  3 ) ) )  -  1 )  x.  ( v  /  3 ) ) )  \/  ( -.  ( ( ( ( |_ `  ( ( F `  x )  /  ( v  / 
3 ) ) )  -  1 )  x.  ( v  /  3
) )  <_  (
h `  x )  /\  ( h `  x
)  =/=  0 )  /\  t  =  ( h `  x ) ) ) )
161159, 160bitr4i 244 . . . . . . . 8  |-  ( ( ( ( ( ( ( |_ `  (
( F `  x
)  /  ( v  /  3 ) ) )  -  1 )  x.  ( v  / 
3 ) )  <_ 
( h `  x
)  /\  ( h `  x )  =/=  0
)  /\  t  =  ( ( ( |_
`  ( ( F `
 x )  / 
( v  /  3
) ) )  - 
1 )  x.  (
v  /  3 ) ) )  \/  (
( -.  ( ( ( |_ `  (
( F `  x
)  /  ( v  /  3 ) ) )  -  1 )  x.  ( v  / 
3 ) )  <_ 
( h `  x
)  \/  ( h `
 x )  =  0 )  /\  t  =  ( h `  x ) ) )  <-> 
t  =  if ( ( ( ( ( |_ `  ( ( F `  x )  /  ( v  / 
3 ) ) )  -  1 )  x.  ( v  /  3
) )  <_  (
h `  x )  /\  ( h `  x
)  =/=  0 ) ,  ( ( ( |_ `  ( ( F `  x )  /  ( v  / 
3 ) ) )  -  1 )  x.  ( v  /  3
) ) ,  ( h `  x ) ) )
162150, 153, 1613bitr4i 269 . . . . . . 7  |-  ( if ( ( ( ( ( |_ `  (
( F `  x
)  /  ( v  /  3 ) ) )  -  1 )  x.  ( v  / 
3 ) )  <_ 
( h `  x
)  /\  ( h `  x )  =/=  0
) ,  ( ( ( |_ `  (
( F `  x
)  /  ( v  /  3 ) ) )  -  1 )  x.  ( v  / 
3 ) ) ,  ( h `  x
) )  e.  {
t }  <->  ( (
( ( ( ( |_ `  ( ( F `  x )  /  ( v  / 
3 ) ) )  -  1 )  x.  ( v  /  3
) )  <_  (
h `  x )  /\  ( h `  x
)  =/=  0 )  /\  t  =  ( ( ( |_ `  ( ( F `  x )  /  (
v  /  3 ) ) )  -  1 )  x.  ( v  /  3 ) ) )  \/  ( ( -.  ( ( ( |_ `  ( ( F `  x )  /  ( v  / 
3 ) ) )  -  1 )  x.  ( v  /  3
) )  <_  (
h `  x )  \/  ( h `  x
)  =  0 )  /\  t  =  ( h `  x ) ) ) )
163162a1i 11 . . . . . 6  |-  ( x  e.  RR  ->  ( if ( ( ( ( ( |_ `  (
( F `  x
)  /  ( v  /  3 ) ) )  -  1 )  x.  ( v  / 
3 ) )  <_ 
( h `  x
)  /\  ( h `  x )  =/=  0
) ,  ( ( ( |_ `  (
( F `  x
)  /  ( v  /  3 ) ) )  -  1 )  x.  ( v  / 
3 ) ) ,  ( h `  x
) )  e.  {
t }  <->  ( (
( ( ( ( |_ `  ( ( F `  x )  /  ( v  / 
3 ) ) )  -  1 )  x.  ( v  /  3
) )  <_  (
h `  x )  /\  ( h `  x
)  =/=  0 )  /\  t  =  ( ( ( |_ `  ( ( F `  x )  /  (
v  /  3 ) ) )  -  1 )  x.  ( v  /  3 ) ) )  \/  ( ( -.  ( ( ( |_ `  ( ( F `  x )  /  ( v  / 
3 ) ) )  -  1 )  x.  ( v  /  3
) )  <_  (
h `  x )  \/  ( h `  x
)  =  0 )  /\  t  =  ( h `  x ) ) ) ) )
164163rabbiia 2906 . . . . 5  |-  { x  e.  RR  |  if ( ( ( ( ( |_ `  ( ( F `  x )  /  ( v  / 
3 ) ) )  -  1 )  x.  ( v  /  3
) )  <_  (
h `  x )  /\  ( h `  x
)  =/=  0 ) ,  ( ( ( |_ `  ( ( F `  x )  /  ( v  / 
3 ) ) )  -  1 )  x.  ( v  /  3
) ) ,  ( h `  x ) )  e.  { t } }  =  {
x  e.  RR  | 
( ( ( ( ( ( |_ `  ( ( F `  x )  /  (
v  /  3 ) ) )  -  1 )  x.  ( v  /  3 ) )  <_  ( h `  x )  /\  (
h `  x )  =/=  0 )  /\  t  =  ( ( ( |_ `  ( ( F `  x )  /  ( v  / 
3 ) ) )  -  1 )  x.  ( v  /  3
) ) )  \/  ( ( -.  (
( ( |_ `  ( ( F `  x )  /  (
v  /  3 ) ) )  -  1 )  x.  ( v  /  3 ) )  <_  ( h `  x )  \/  (
h `  x )  =  0 )  /\  t  =  ( h `  x ) ) ) }
165140, 149, 1643eqtr4ri 2435 . . . 4  |-  { x  e.  RR  |  if ( ( ( ( ( |_ `  ( ( F `  x )  /  ( v  / 
3 ) ) )  -  1 )  x.  ( v  /  3
) )  <_  (
h `  x )  /\  ( h `  x
)  =/=  0 ) ,  ( ( ( |_ `  ( ( F `  x )  /  ( v  / 
3 ) ) )  -  1 )  x.  ( v  /  3
) ) ,  ( h `  x ) )  e.  { t } }  =  ( ( ( { x  e.  RR  |  ( ( ( |_ `  (
( F `  x
)  /  ( v  /  3 ) ) )  -  1 )  x.  ( v  / 
3 ) )  <_ 
( h `  x
) }  i^i  {
x  e.  RR  | 
( h `  x
)  =/=  0 } )  i^i  { x  e.  RR  |  t  =  ( ( ( |_
`  ( ( F `
 x )  / 
( v  /  3
) ) )  - 
1 )  x.  (
v  /  3 ) ) } )  u.  ( ( { x  e.  RR  |  -.  (
( ( |_ `  ( ( F `  x )  /  (
v  /  3 ) ) )  -  1 )  x.  ( v  /  3 ) )  <_  ( h `  x ) }  u.  { x  e.  RR  | 
( h `  x
)  =  0 } )  i^i  { x  e.  RR  |  t  =  ( h `  x
) } ) )
166139, 165eqtri 2424 . . 3  |-  ( `' ( x  e.  RR  |->  if ( ( ( ( ( |_ `  (
( F `  x
)  /  ( v  /  3 ) ) )  -  1 )  x.  ( v  / 
3 ) )  <_ 
( h `  x
)  /\  ( h `  x )  =/=  0
) ,  ( ( ( |_ `  (
( F `  x
)  /  ( v  /  3 ) ) )  -  1 )  x.  ( v  / 
3 ) ) ,  ( h `  x
) ) ) " { t } )  =  ( ( ( { x  e.  RR  |  ( ( ( |_ `  ( ( F `  x )  /  ( v  / 
3 ) ) )  -  1 )  x.  ( v  /  3
) )  <_  (
h `  x ) }  i^i  { x  e.  RR  |  ( h `
 x )  =/=  0 } )  i^i 
{ x  e.  RR  |  t  =  (
( ( |_ `  ( ( F `  x )  /  (
v  /  3 ) ) )  -  1 )  x.  ( v  /  3 ) ) } )  u.  (
( { x  e.  RR  |  -.  (
( ( |_ `  ( ( F `  x )  /  (
v  /  3 ) ) )  -  1 )  x.  ( v  /  3 ) )  <_  ( h `  x ) }  u.  { x  e.  RR  | 
( h `  x
)  =  0 } )  i^i  { x  e.  RR  |  t  =  ( h `  x
) } ) )
167 eldifi 3429 . . . . . 6  |-  ( t  e.  ( ran  (
x  e.  RR  |->  if ( ( ( ( ( |_ `  (
( F `  x
)  /  ( v  /  3 ) ) )  -  1 )  x.  ( v  / 
3 ) )  <_ 
( h `  x
)  /\  ( h `  x )  =/=  0
) ,  ( ( ( |_ `  (
( F `  x
)  /  ( v  /  3 ) ) )  -  1 )  x.  ( v  / 
3 ) ) ,  ( h `  x
) ) )  \  { 0 } )  ->  t  e.  ran  ( x  e.  RR  |->  if ( ( ( ( ( |_ `  (
( F `  x
)  /  ( v  /  3 ) ) )  -  1 )  x.  ( v  / 
3 ) )  <_ 
( h `  x
)  /\  ( h `  x )  =/=  0
) ,  ( ( ( |_ `  (
( F `  x
)  /  ( v  /  3 ) ) )  -  1 )  x.  ( v  / 
3 ) ) ,  ( h `  x
) ) ) )
168 frn 5556 . . . . . . . 8  |-  ( ( x  e.  RR  |->  if ( ( ( ( ( |_ `  (
( F `  x
)  /  ( v  /  3 ) ) )  -  1 )  x.  ( v  / 
3 ) )  <_ 
( h `  x
)  /\  ( h `  x )  =/=  0
) ,  ( ( ( |_ `  (
( F `  x
)  /  ( v  /  3 ) ) )  -  1 )  x.  ( v  / 
3 ) ) ,  ( h `  x
) ) ) : RR --> RR  ->  ran  ( x  e.  RR  |->  if ( ( ( ( ( |_ `  (
( F `  x
)  /  ( v  /  3 ) ) )  -  1 )  x.  ( v  / 
3 ) )  <_ 
( h `  x
)  /\  ( h `  x )  =/=  0
) ,  ( ( ( |_ `  (
( F `  x
)  /  ( v  /  3 ) ) )  -  1 )  x.  ( v  / 
3 ) ) ,  ( h `  x
) ) )  C_  RR )
16936, 168syl 16 . . . . . . 7  |-  ( ( ( ph  /\  h  e.  dom  S.1 )  /\  v  e.  RR+ )  ->  ran  ( x  e.  RR  |->  if ( ( ( ( ( |_ `  (
( F `  x
)  /  ( v  /  3 ) ) )  -  1 )  x.  ( v  / 
3 ) )  <_ 
( h `  x
)  /\  ( h `  x )  =/=  0
) ,  ( ( ( |_ `  (
( F `  x
)  /  ( v  /  3 ) ) )  -  1 )  x.  ( v  / 
3 ) ) ,  ( h `  x
) ) )  C_  RR )
170169sseld 3307 . . . . . 6  |-  ( ( ( ph  /\  h  e.  dom  S.1 )  /\  v  e.  RR+ )  ->  (
t  e.  ran  (
x  e.  RR  |->  if ( ( ( ( ( |_ `  (
( F `  x
)  /  ( v  /  3 ) ) )  -  1 )  x.  ( v  / 
3 ) )  <_ 
( h `  x
)  /\  ( h `  x )  =/=  0
) ,  ( ( ( |_ `  (
( F `  x
)  /  ( v  /  3 ) ) )  -  1 )  x.  ( v  / 
3 ) ) ,  ( h `  x
) ) )  -> 
t  e.  RR ) )
171167, 170syl5 30 . . . . 5  |-  ( ( ( ph  /\  h  e.  dom  S.1 )  /\  v  e.  RR+ )  ->  (
t  e.  ( ran  ( x  e.  RR  |->  if ( ( ( ( ( |_ `  (
( F `  x
)  /  ( v  /  3 ) ) )  -  1 )  x.  ( v  / 
3 ) )  <_ 
( h `  x
)  /\  ( h `  x )  =/=  0
) ,  ( ( ( |_ `  (
( F `  x
)  /  ( v  /  3 ) ) )  -  1 )  x.  ( v  / 
3 ) ) ,  ( h `  x
) ) )  \  { 0 } )  ->  t  e.  RR ) )
172171imdistani 672 . . . 4  |-  ( ( ( ( ph  /\  h  e.  dom  S.1 )  /\  v  e.  RR+ )  /\  t  e.  ( ran  ( x  e.  RR  |->  if ( ( ( ( ( |_ `  (
( F `  x
)  /  ( v  /  3 ) ) )  -  1 )  x.  ( v  / 
3 ) )  <_ 
( h `  x
)  /\  ( h `  x )  =/=  0
) ,  ( ( ( |_ `  (
( F `  x
)  /  ( v  /  3 ) ) )  -  1 )  x.  ( v  / 
3 ) ) ,  ( h `  x
) ) )  \  { 0 } ) )  ->  ( (
( ph  /\  h  e.  dom  S.1 )  /\  v  e.  RR+ )  /\  t  e.  RR ) )
173 rabiun2 26139 . . . . . . . . . 10  |-  { x  e.  U_ t  e.  ran  h ( `' h " { t } )  |  ( ( ( |_ `  ( ( F `  x )  /  ( v  / 
3 ) ) )  -  1 )  x.  ( v  /  3
) )  <_  (
h `  x ) }  =  U_ t  e. 
ran  h { x  e.  ( `' h " { t } )  |  ( ( ( |_ `  ( ( F `  x )  /  ( v  / 
3 ) ) )  -  1 )  x.  ( v  /  3
) )  <_  (
h `  x ) }
174 cnvimarndm 5184 . . . . . . . . . . . . . 14  |-  ( `' h " ran  h
)  =  dom  h
175 iunid 4106 . . . . . . . . . . . . . . . 16  |-  U_ t  e.  ran  h { t }  =  ran  h
176175imaeq2i 5160 . . . . . . . . . . . . . . 15  |-  ( `' h " U_ t  e.  ran  h { t } )  =  ( `' h " ran  h
)
177 imaiun 5951 . . . . . . . . . . . . . . 15  |-  ( `' h " U_ t  e.  ran  h { t } )  =  U_ t  e.  ran  h ( `' h " { t } )
178176, 177eqtr3i 2426 . . . . . . . . . . . . . 14  |-  ( `' h " ran  h
)  =  U_ t  e.  ran  h ( `' h " { t } )
179174, 178eqtr3i 2426 . . . . . . . . . . . . 13  |-  dom  h  =  U_ t  e.  ran  h ( `' h " { t } )
180 fdm 5554 . . . . . . . . . . . . . 14  |-  ( h : RR --> RR  ->  dom  h  =  RR )
18130, 180syl 16 . . . . . . . . . . . . 13  |-  ( h  e.  dom  S.1  ->  dom  h  =  RR )
182179, 181syl5eqr 2450 . . . . . . . . . . . 12  |-  ( h  e.  dom  S.1  ->  U_ t  e.  ran  h
( `' h " { t } )  =  RR )
183182ad2antlr 708 . . . . . . . . . . 11  |-  ( ( ( ph  /\  h  e.  dom  S.1 )  /\  v  e.  RR+ )  ->  U_ t  e.  ran  h ( `' h " { t } )  =  RR )
184 rabeq 2910 . . . . . . . . . . 11  |-  ( U_ t  e.  ran  h ( `' h " { t } )  =  RR 
->  { x  e.  U_ t  e.  ran  h ( `' h " { t } )  |  ( ( ( |_ `  ( ( F `  x )  /  (
v  /  3 ) ) )  -  1 )  x.  ( v  /  3 ) )  <_  ( h `  x ) }  =  { x  e.  RR  |  ( ( ( |_ `  ( ( F `  x )  /  ( v  / 
3 ) ) )  -  1 )  x.  ( v  /  3
) )  <_  (
h `  x ) } )
185183, 184syl 16 . . . . . . . . . 10  |-  ( ( ( ph  /\  h  e.  dom  S.1 )  /\  v  e.  RR+ )  ->  { x  e.  U_ t  e.  ran  h ( `' h " { t } )  |  ( ( ( |_ `  ( ( F `  x )  /  ( v  / 
3 ) ) )  -  1 )  x.  ( v  /  3
) )  <_  (
h `  x ) }  =  { x  e.  RR  |  ( ( ( |_ `  (
( F `  x
)  /  ( v  /  3 ) ) )  -  1 )  x.  ( v  / 
3 ) )  <_ 
( h `  x
) } )
186173, 185syl5eqr 2450 . . . . . . . . 9  |-  ( ( ( ph  /\  h  e.  dom  S.1 )  /\  v  e.  RR+ )  ->  U_ t  e.  ran  h { x  e.  ( `' h " { t } )  |  ( ( ( |_ `  ( ( F `  x )  /  ( v  / 
3 ) ) )  -  1 )  x.  ( v  /  3
) )  <_  (
h `  x ) }  =  { x  e.  RR  |  ( ( ( |_ `  (
( F `  x
)  /  ( v  /  3 ) ) )  -  1 )  x.  ( v  / 
3 ) )  <_ 
( h `  x
) } )
187 fniniseg 5810 . . . . . . . . . . . . . . . . . 18  |-  ( h  Fn  RR  ->  (
x  e.  ( `' h " { t } )  <->  ( x  e.  RR  /\  ( h `
 x )  =  t ) ) )
18830, 76, 1873syl 19 . . . . . . . . . . . . . . . . 17  |-  ( h  e.  dom  S.1  ->  ( x  e.  ( `' h " { t } )  <->  ( x  e.  RR  /\  ( h `
 x )  =  t ) ) )
189188simplbda 608 . . . . . . . . . . . . . . . 16  |-  ( ( h  e.  dom  S.1  /\  x  e.  ( `' h " { t } ) )  -> 
( h `  x
)  =  t )
190189breq2d 4184 . . . . . . . . . . . . . . 15  |-  ( ( h  e.  dom  S.1  /\  x  e.  ( `' h " { t } ) )  -> 
( ( ( ( |_ `  ( ( F `  x )  /  ( v  / 
3 ) ) )  -  1 )  x.  ( v  /  3
) )  <_  (
h `  x )  <->  ( ( ( |_ `  ( ( F `  x )  /  (
v  /  3 ) ) )  -  1 )  x.  ( v  /  3 ) )  <_  t ) )
191190rabbidva 2907 . . . . . . . . . . . . . 14  |-  ( h  e.  dom  S.1  ->  { x  e.  ( `' h " { t } )  |  ( ( ( |_ `  ( ( F `  x )  /  (
v  /  3 ) ) )  -  1 )  x.  ( v  /  3 ) )  <_  ( h `  x ) }  =  { x  e.  ( `' h " { t } )  |  ( ( ( |_ `  ( ( F `  x )  /  (
v  /  3 ) ) )  -  1 )  x.  ( v  /  3 ) )  <_  t } )
192 inrab2 3574 . . . . . . . . . . . . . . 15  |-  ( { x  e.  RR  | 
( ( ( |_
`  ( ( F `
 x )  / 
( v  /  3
) ) )  - 
1 )  x.  (
v  /  3 ) )  <_  t }  i^i  ( `' h " { t } ) )  =  { x  e.  ( RR  i^i  ( `' h " { t } ) )  |  ( ( ( |_
`  ( ( F `
 x )  / 
( v  /  3
) ) )  - 
1 )  x.  (
v  /  3 ) )  <_  t }
193 imassrn 5175 . . . . . . . . . . . . . . . . . 18  |-  ( `' h " { t } )  C_  ran  `' h
194 dfdm4 5022 . . . . . . . . . . . . . . . . . . 19  |-  dom  h  =  ran  `' h
195194, 181syl5eqr 2450 . . . . . . . . . . . . . . . . . 18  |-  ( h  e.  dom  S.1  ->  ran  `' h  =  RR )
196193, 195syl5sseq 3356 . . . . . . . . . . . . . . . . 17  |-  ( h  e.  dom  S.1  ->  ( `' h " { t } )  C_  RR )
197 dfss1 3505 . . . . . . . . . . . . . . . . 17  |-  ( ( `' h " { t } )  C_  RR  <->  ( RR  i^i  ( `' h " { t } ) )  =  ( `' h " { t } ) )
198196, 197sylib 189 . . . . . . . . . . . . . . . 16  |-  ( h  e.  dom  S.1  ->  ( RR  i^i  ( `' h " { t } ) )  =  ( `' h " { t } ) )
199 rabeq 2910 . . . . . . . . . . . . . . . 16  |-  ( ( RR  i^i  ( `' h " { t } ) )  =  ( `' h " { t } )  ->  { x  e.  ( RR  i^i  ( `' h " { t } ) )  |  ( ( ( |_
`  ( ( F `
 x )  / 
( v  /  3
) ) )  - 
1 )  x.  (
v  /  3 ) )  <_  t }  =  { x  e.  ( `' h " { t } )  |  ( ( ( |_ `  ( ( F `  x )  /  (
v  /  3 ) ) )  -  1 )  x.  ( v  /  3 ) )  <_  t } )
200198, 199syl 16 . . . . . . . . . . . . . . 15  |-  ( h  e.  dom  S.1  ->  { x  e.  ( RR 
i^i  ( `' h " { t } ) )  |  ( ( ( |_ `  (
( F `  x
)  /  ( v  /  3 ) ) )  -  1 )  x.  ( v  / 
3 ) )  <_ 
t }  =  {
x  e.  ( `' h " { t } )  |  ( ( ( |_ `  ( ( F `  x )  /  (
v  /  3 ) ) )  -  1 )  x.  ( v  /  3 ) )  <_  t } )
201192, 200syl5eq 2448 . . . . . . . . . . . . . 14  |-  ( h  e.  dom  S.1  ->  ( { x  e.  RR  |  ( ( ( |_ `  ( ( F `  x )  /  ( v  / 
3 ) ) )  -  1 )  x.  ( v  /  3
) )  <_  t }  i^i  ( `' h " { t } ) )  =  { x  e.  ( `' h " { t } )  |  ( ( ( |_ `  ( ( F `  x )  /  ( v  / 
3 ) ) )  -  1 )  x.  ( v  /  3
) )  <_  t } )
202191, 201eqtr4d 2439 . . . . . . . . . . . . 13  |-  ( h  e.  dom  S.1  ->  { x  e.  ( `' h " { t } )  |  ( ( ( |_ `  ( ( F `  x )  /  (
v  /  3 ) ) )  -  1 )  x.  ( v  /  3 ) )  <_  ( h `  x ) }  =  ( { x  e.  RR  |  ( ( ( |_ `  ( ( F `  x )  /  ( v  / 
3 ) ) )  -  1 )  x.  ( v  /  3
) )  <_  t }  i^i  ( `' h " { t } ) ) )
203202ad3antlr 712 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  h  e.  dom  S.1 )  /\  v  e.  RR+ )  /\  t  e.  ran  h )  ->  { x  e.  ( `' h " { t } )  |  ( ( ( |_ `  ( ( F `  x )  /  ( v  / 
3 ) ) )  -  1 )  x.  ( v  /  3
) )  <_  (
h `  x ) }  =  ( {
x  e.  RR  | 
( ( ( |_
`  ( ( F `
 x )  / 
( v  /  3
) ) )  - 
1 )  x.  (
v  /  3 ) )  <_  t }  i^i  ( `' h " { t } ) ) )
20428adantlr 696 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ( ph  /\  h  e.  dom  S.1 )  /\  v  e.  RR+ )  /\  t  e.  ran  h )  /\  x  e.  RR )  ->  (
( |_ `  (
( F `  x
)  /  ( v  /  3 ) ) )  -  1 )  e.  RR )
20566ad2antlr 708 . . . . . . . . . . . . . . . . . . . 20  |-  (