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

Theorem itg2addnclem2 26247
Description: Lemma for itg2addnc 26249. 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 9083 . . . . . . . . . . . 12  |-  0  e.  RR
3 pnfxr 10705 . . . . . . . . . . . 12  |-  +oo  e.  RR*
4 icossre 10983 . . . . . . . . . . . 12  |-  ( ( 0  e.  RR  /\  +oo 
e.  RR* )  ->  (
0 [,)  +oo )  C_  RR )
52, 3, 4mp2an 654 . . . . . . . . . . 11  |-  ( 0 [,)  +oo )  C_  RR
6 fss 5591 . . . . . . . . . . 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 5862 . . . . . . . 8  |-  ( ( ( ( ph  /\  h  e.  dom  S.1 )  /\  v  e.  RR+ )  /\  x  e.  RR )  ->  ( F `  x )  e.  RR )
10 rpre 10610 . . . . . . . . . 10  |-  ( v  e.  RR+  ->  v  e.  RR )
11 3re 10063 . . . . . . . . . . 11  |-  3  e.  RR
12 3ne0 10077 . . . . . . . . . . 11  |-  3  =/=  0
1311, 12pm3.2i 442 . . . . . . . . . 10  |-  ( 3  e.  RR  /\  3  =/=  0 )
14 redivcl 9725 . . . . . . . . . . 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 10621 . . . . . . . . . 10  |-  ( v  e.  RR+  ->  ( v  e.  CC  /\  v  =/=  0 ) )
19 3cn 10064 . . . . . . . . . . 11  |-  3  e.  CC
2019, 12pm3.2i 442 . . . . . . . . . 10  |-  ( 3  e.  CC  /\  3  =/=  0 )
21 divne0 9682 . . . . . . . . . 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 9834 . . . . . . 7  |-  ( ( ( ( ph  /\  h  e.  dom  S.1 )  /\  v  e.  RR+ )  /\  x  e.  RR )  ->  ( ( F `
 x )  / 
( v  /  3
) )  e.  RR )
25 reflcl 11197 . . . . . . 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 9359 . . . . . 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 9108 . . . 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 19560 . . . . . 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 5862 . . . 4  |-  ( ( ( ( ph  /\  h  e.  dom  S.1 )  /\  v  e.  RR+ )  /\  x  e.  RR )  ->  ( h `  x )  e.  RR )
33 ifcl 3767 . . . 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 2435 . . 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 5885 . 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 11303 . . . . 5  |-  ( 0 ... -u ( |_ `  -u ( ( sup ( ran  h ,  RR ,  <  )  /  ( v  /  3 ) )  +  1 ) ) )  e.  Fin
38 ovex 6098 . . . . . . 7  |-  ( ( t  -  1 )  x.  ( v  / 
3 ) )  e. 
_V
39 eqid 2435 . . . . . . 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 5565 . . . . . 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 5651 . . . . . 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 7384 . . . . 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 19561 . . . . 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 7366 . . . 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 10126 . . . . . . . . . . . . . . . . 17  |-  3  e.  NN
50 nnrp 10613 . . . . . . . . . . . . . . . . 17  |-  ( 3  e.  NN  ->  3  e.  RR+ )
5149, 50ax-mp 8 . . . . . . . . . . . . . . . 16  |-  3  e.  RR+
52 rpdivcl 10626 . . . . . . . . . . . . . . . 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 5862 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  h  e.  dom  S.1 )  /\  v  e.  RR+ )  /\  x  e.  RR )  ->  ( F `  x )  e.  ( 0 [,)  +oo )
)
57 elrege0 10999 . . . . . . . . . . . . . . . 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 10676 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  h  e.  dom  S.1 )  /\  v  e.  RR+ )  /\  x  e.  RR )  ->  0  <_  (
( F `  x
)  /  ( v  /  3 ) ) )
61 flge0nn0 11217 . . . . . . . . . . . . 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 10269 . . . . . . . . . . 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 5589 . . . . . . . . . . . . . . . . 17  |-  ( h : RR --> RR  ->  ran  h  C_  RR )
6630, 65syl 16 . . . . . . . . . . . . . . . 16  |-  ( h  e.  dom  S.1  ->  ran  h  C_  RR )
67 i1f0rn 19566 . . . . . . . . . . . . . . . . . 18  |-  ( h  e.  dom  S.1  ->  0  e.  ran  h )
68 elex2 2960 . . . . . . . . . . . . . . . . . 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 3629 . . . . . . . . . . . . . . . . 17  |-  ( ran  h  =/=  (/)  <->  E. x  x  e.  ran  h )
7169, 70sylibr 204 . . . . . . . . . . . . . . . 16  |-  ( h  e.  dom  S.1  ->  ran  h  =/=  (/) )
72 fimaxre2 9948 . . . . . . . . . . . . . . . . 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 5583 . . . . . . . . . . . . . . . . . 18  |-  ( h : RR --> RR  ->  h  Fn  RR )
7730, 76syl 16 . . . . . . . . . . . . . . . . 17  |-  ( h  e.  dom  S.1  ->  h  Fn  RR )
78 dffn3 5590 . . . . . . . . . . . . . . . . 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 5862 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  h  e.  dom  S.1 )  /\  v  e.  RR+ )  /\  x  e.  RR )  ->  ( h `  x )  e.  ran  h )
82 suprub 9961 . . . . . . . . . . . . . 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 9960 . . . . . . . . . . . . . . . . 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 9159 . . . . . . . . . . . . . . 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 10685 . . . . . . . . . . . . . . . 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 9082 . . . . . . . . . . . . . . . . . 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 9834 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ph  /\  h  e.  dom  S.1 )  /\  v  e.  RR+ )  /\  x  e.  RR )  ->  ( sup ( ran  h ,  RR ,  <  )  /  ( v  /  3 ) )  e.  RR )
9326, 91, 92lesubaddd 9615 . . . . . . . . . . . . . . . 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 9231 . . . . . . . . . . . . . . . . . 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 11225 . . . . . . . . . . . . . . . . 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 11224 . . . . . . . . . . . . . . . . . . 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 10367 . . . . . . . . . . . . . . . . 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 9159 . . . . . . . . . . . . . . . . 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 11199 . . . . . . . . . . . 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 10285 . . . . . . . . . . . 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 11041 . . . . . . . . . . 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 2435 . . . . . . . . 9  |-  ( ( ( |_ `  (
( F `  x
)  /  ( v  /  3 ) ) )  -  1 )  x.  ( v  / 
3 ) )  =  ( ( ( |_
`  ( ( F `
 x )  / 
( v  /  3
) ) )  - 
1 )  x.  (
v  /  3 ) )
119 oveq1 6080 . . . . . . . . . . . 12  |-  ( t  =  ( |_ `  ( ( F `  x )  /  (
v  /  3 ) ) )  ->  (
t  -  1 )  =  ( ( |_
`  ( ( F `
 x )  / 
( v  /  3
) ) )  - 
1 ) )
120119oveq1d 6088 . . . . . . . . . . 11  |-  ( t  =  ( |_ `  ( ( F `  x )  /  (
v  /  3 ) ) )  ->  (
( t  -  1 )  x.  ( v  /  3 ) )  =  ( ( ( |_ `  ( ( F `  x )  /  ( v  / 
3 ) ) )  -  1 )  x.  ( v  /  3
) ) )
121120eqeq2d 2446 . . . . . . . . . 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 3044 . . . . . . . . 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 6098 . . . . . . . . 9  |-  ( ( ( |_ `  (
( F `  x
)  /  ( v  /  3 ) ) )  -  1 )  x.  ( v  / 
3 ) )  e. 
_V
12539elrnmpt 5109 . . . . . . . . 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 3506 . . . . . . 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 3507 . . . . . . . 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 3758 . . . . 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 5885 . . . 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 5589 . . . 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 7321 . . 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 5355 . . . 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 3604 . . . . 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 3605 . . . . . . . 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 3530 . . . . . . 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 3605 . . . . . . 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 2455 . . . . . 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 3604 . . . . . . . 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 3530 . . . . . . 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 3605 . . . . . . 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 2455 . . . . . 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 3491 . . . . 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 2437 . . . . . . . 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 5734 . . . . . . . . . 10  |-  ( h `
 x )  e. 
_V
152124, 151ifex 3789 . . . . . . . . 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 3829 . . . . . . . 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 2602 . . . . . . . . . . . . 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 3764 . . . . . . . . 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 2938 . . . . 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 2466 . . . 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 2455 . . 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 3461 . . . . . 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 5589 . . . . . . . 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 3339 . . . . . 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 26230 . . . . . . . . . 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 5217 . . . . . . . . . . . . . 14  |-  ( `' h " ran  h
)  =  dom  h
175 iunid 4138 . . . . . . . . . . . . . . . 16  |-  U_ t  e.  ran  h { t }  =  ran  h
176175imaeq2i 5193 . . . . . . . . . . . . . . 15  |-  ( `' h " U_ t  e.  ran  h { t } )  =  ( `' h " ran  h
)
177 imaiun 5984 . . . . . . . . . . . . . . 15  |-  ( `' h " U_ t  e.  ran  h { t } )  =  U_ t  e.  ran  h ( `' h " { t } )
178176, 177eqtr3i 2457 . . . . . . . . . . . . . 14  |-  ( `' h " ran  h
)  =  U_ t  e.  ran  h ( `' h " { t } )
179174, 178eqtr3i 2457 . . . . . . . . . . . . 13  |-  dom  h  =  U_ t  e.  ran  h ( `' h " { t } )
180 fdm 5587 . . . . . . . . . . . . . 14  |-  ( h : RR --> RR  ->  dom  h  =  RR )
18130, 180syl 16 . . . . . . . . . . . . 13  |-  ( h  e.  dom  S.1  ->  dom  h  =  RR )
182179, 181syl5eqr 2481 . . . . . . . . . . . 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 2942 . . . . . . . . . . 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 2481 . . . . . . . . 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 5843 . . . . . . . . . . . . . . . . . 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 4216 . . . . . . . . . . . . . . 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 2939 . . . . . . . . . . . . . 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 3606 . . . . . . . . . . . . . . 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 5208 . . . . . . . . . . . . . . . . . 18  |-  ( `' h " { t } )  C_  ran  `' h
194 dfdm4 5055 . . . . . . . . . . . . . . . . . . 19  |-  dom  h  =  ran  `' h
195194, 181syl5eqr 2481 . . . . . . . . . . . . . . . . . 18  |-  ( h  e.  dom  S.1  ->  ran  `' h  =  RR )
196193, 195syl5sseq 3388 . . . . . . . . . . . . . . . . 17  |-  ( h  e.  dom  S.1  ->  ( `' h " { t } )  C_  RR )
197 dfss1 3537 . . . . . . . . . . . . . . . . 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 2942 . . . . . . . . . . . . . . . 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 2479 . . . . . . . . . . . . . 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 2470 . . . . . . . . . . . . 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  |-