Metamath Proof Explorer


Theorem uniioombllem2

Description: Lemma for uniioombl . (Contributed by Mario Carneiro, 26-Mar-2015) (Revised by Mario Carneiro, 11-Dec-2016) (Revised by AV, 13-Sep-2020)

Ref Expression
Hypotheses uniioombl.1
|- ( ph -> F : NN --> ( <_ i^i ( RR X. RR ) ) )
uniioombl.2
|- ( ph -> Disj_ x e. NN ( (,) ` ( F ` x ) ) )
uniioombl.3
|- S = seq 1 ( + , ( ( abs o. - ) o. F ) )
uniioombl.a
|- A = U. ran ( (,) o. F )
uniioombl.e
|- ( ph -> ( vol* ` E ) e. RR )
uniioombl.c
|- ( ph -> C e. RR+ )
uniioombl.g
|- ( ph -> G : NN --> ( <_ i^i ( RR X. RR ) ) )
uniioombl.s
|- ( ph -> E C_ U. ran ( (,) o. G ) )
uniioombl.t
|- T = seq 1 ( + , ( ( abs o. - ) o. G ) )
uniioombl.v
|- ( ph -> sup ( ran T , RR* , < ) <_ ( ( vol* ` E ) + C ) )
uniioombllem2.h
|- H = ( z e. NN |-> ( ( (,) ` ( F ` z ) ) i^i ( (,) ` ( G ` J ) ) ) )
uniioombllem2.k
|- K = ( x e. ran (,) |-> if ( x = (/) , <. 0 , 0 >. , <. inf ( x , RR* , < ) , sup ( x , RR* , < ) >. ) )
Assertion uniioombllem2
|- ( ( ph /\ J e. NN ) -> seq 1 ( + , ( vol* o. H ) ) ~~> ( vol* ` ( ( (,) ` ( G ` J ) ) i^i A ) ) )

Proof

Step Hyp Ref Expression
1 uniioombl.1
 |-  ( ph -> F : NN --> ( <_ i^i ( RR X. RR ) ) )
2 uniioombl.2
 |-  ( ph -> Disj_ x e. NN ( (,) ` ( F ` x ) ) )
3 uniioombl.3
 |-  S = seq 1 ( + , ( ( abs o. - ) o. F ) )
4 uniioombl.a
 |-  A = U. ran ( (,) o. F )
5 uniioombl.e
 |-  ( ph -> ( vol* ` E ) e. RR )
6 uniioombl.c
 |-  ( ph -> C e. RR+ )
7 uniioombl.g
 |-  ( ph -> G : NN --> ( <_ i^i ( RR X. RR ) ) )
8 uniioombl.s
 |-  ( ph -> E C_ U. ran ( (,) o. G ) )
9 uniioombl.t
 |-  T = seq 1 ( + , ( ( abs o. - ) o. G ) )
10 uniioombl.v
 |-  ( ph -> sup ( ran T , RR* , < ) <_ ( ( vol* ` E ) + C ) )
11 uniioombllem2.h
 |-  H = ( z e. NN |-> ( ( (,) ` ( F ` z ) ) i^i ( (,) ` ( G ` J ) ) ) )
12 uniioombllem2.k
 |-  K = ( x e. ran (,) |-> if ( x = (/) , <. 0 , 0 >. , <. inf ( x , RR* , < ) , sup ( x , RR* , < ) >. ) )
13 nnuz
 |-  NN = ( ZZ>= ` 1 )
14 eqid
 |-  seq 1 ( + , ( ( abs o. - ) o. ( K o. H ) ) ) = seq 1 ( + , ( ( abs o. - ) o. ( K o. H ) ) )
15 1zzd
 |-  ( ( ph /\ J e. NN ) -> 1 e. ZZ )
16 eqidd
 |-  ( ( ( ph /\ J e. NN ) /\ n e. NN ) -> ( ( ( abs o. - ) o. ( K o. H ) ) ` n ) = ( ( ( abs o. - ) o. ( K o. H ) ) ` n ) )
17 1 2 3 4 5 6 7 8 9 10 uniioombllem2a
 |-  ( ( ( ph /\ J e. NN ) /\ z e. NN ) -> ( ( (,) ` ( F ` z ) ) i^i ( (,) ` ( G ` J ) ) ) e. ran (,) )
18 11 a1i
 |-  ( ( ph /\ J e. NN ) -> H = ( z e. NN |-> ( ( (,) ` ( F ` z ) ) i^i ( (,) ` ( G ` J ) ) ) ) )
19 12 ioorf
 |-  K : ran (,) --> ( <_ i^i ( RR* X. RR* ) )
20 19 a1i
 |-  ( ( ph /\ J e. NN ) -> K : ran (,) --> ( <_ i^i ( RR* X. RR* ) ) )
21 20 feqmptd
 |-  ( ( ph /\ J e. NN ) -> K = ( y e. ran (,) |-> ( K ` y ) ) )
22 fveq2
 |-  ( y = ( ( (,) ` ( F ` z ) ) i^i ( (,) ` ( G ` J ) ) ) -> ( K ` y ) = ( K ` ( ( (,) ` ( F ` z ) ) i^i ( (,) ` ( G ` J ) ) ) ) )
23 17 18 21 22 fmptco
 |-  ( ( ph /\ J e. NN ) -> ( K o. H ) = ( z e. NN |-> ( K ` ( ( (,) ` ( F ` z ) ) i^i ( (,) ` ( G ` J ) ) ) ) ) )
24 inss2
 |-  ( ( (,) ` ( F ` z ) ) i^i ( (,) ` ( G ` J ) ) ) C_ ( (,) ` ( G ` J ) )
25 inss2
 |-  ( <_ i^i ( RR X. RR ) ) C_ ( RR X. RR )
26 7 ffvelrnda
 |-  ( ( ph /\ J e. NN ) -> ( G ` J ) e. ( <_ i^i ( RR X. RR ) ) )
27 25 26 sselid
 |-  ( ( ph /\ J e. NN ) -> ( G ` J ) e. ( RR X. RR ) )
28 1st2nd2
 |-  ( ( G ` J ) e. ( RR X. RR ) -> ( G ` J ) = <. ( 1st ` ( G ` J ) ) , ( 2nd ` ( G ` J ) ) >. )
29 27 28 syl
 |-  ( ( ph /\ J e. NN ) -> ( G ` J ) = <. ( 1st ` ( G ` J ) ) , ( 2nd ` ( G ` J ) ) >. )
30 29 fveq2d
 |-  ( ( ph /\ J e. NN ) -> ( (,) ` ( G ` J ) ) = ( (,) ` <. ( 1st ` ( G ` J ) ) , ( 2nd ` ( G ` J ) ) >. ) )
31 df-ov
 |-  ( ( 1st ` ( G ` J ) ) (,) ( 2nd ` ( G ` J ) ) ) = ( (,) ` <. ( 1st ` ( G ` J ) ) , ( 2nd ` ( G ` J ) ) >. )
32 30 31 eqtr4di
 |-  ( ( ph /\ J e. NN ) -> ( (,) ` ( G ` J ) ) = ( ( 1st ` ( G ` J ) ) (,) ( 2nd ` ( G ` J ) ) ) )
33 ioossre
 |-  ( ( 1st ` ( G ` J ) ) (,) ( 2nd ` ( G ` J ) ) ) C_ RR
34 32 33 eqsstrdi
 |-  ( ( ph /\ J e. NN ) -> ( (,) ` ( G ` J ) ) C_ RR )
35 32 fveq2d
 |-  ( ( ph /\ J e. NN ) -> ( vol* ` ( (,) ` ( G ` J ) ) ) = ( vol* ` ( ( 1st ` ( G ` J ) ) (,) ( 2nd ` ( G ` J ) ) ) ) )
36 ovolfcl
 |-  ( ( G : NN --> ( <_ i^i ( RR X. RR ) ) /\ J e. NN ) -> ( ( 1st ` ( G ` J ) ) e. RR /\ ( 2nd ` ( G ` J ) ) e. RR /\ ( 1st ` ( G ` J ) ) <_ ( 2nd ` ( G ` J ) ) ) )
37 7 36 sylan
 |-  ( ( ph /\ J e. NN ) -> ( ( 1st ` ( G ` J ) ) e. RR /\ ( 2nd ` ( G ` J ) ) e. RR /\ ( 1st ` ( G ` J ) ) <_ ( 2nd ` ( G ` J ) ) ) )
38 ovolioo
 |-  ( ( ( 1st ` ( G ` J ) ) e. RR /\ ( 2nd ` ( G ` J ) ) e. RR /\ ( 1st ` ( G ` J ) ) <_ ( 2nd ` ( G ` J ) ) ) -> ( vol* ` ( ( 1st ` ( G ` J ) ) (,) ( 2nd ` ( G ` J ) ) ) ) = ( ( 2nd ` ( G ` J ) ) - ( 1st ` ( G ` J ) ) ) )
39 37 38 syl
 |-  ( ( ph /\ J e. NN ) -> ( vol* ` ( ( 1st ` ( G ` J ) ) (,) ( 2nd ` ( G ` J ) ) ) ) = ( ( 2nd ` ( G ` J ) ) - ( 1st ` ( G ` J ) ) ) )
40 35 39 eqtrd
 |-  ( ( ph /\ J e. NN ) -> ( vol* ` ( (,) ` ( G ` J ) ) ) = ( ( 2nd ` ( G ` J ) ) - ( 1st ` ( G ` J ) ) ) )
41 37 simp2d
 |-  ( ( ph /\ J e. NN ) -> ( 2nd ` ( G ` J ) ) e. RR )
42 37 simp1d
 |-  ( ( ph /\ J e. NN ) -> ( 1st ` ( G ` J ) ) e. RR )
43 41 42 resubcld
 |-  ( ( ph /\ J e. NN ) -> ( ( 2nd ` ( G ` J ) ) - ( 1st ` ( G ` J ) ) ) e. RR )
44 40 43 eqeltrd
 |-  ( ( ph /\ J e. NN ) -> ( vol* ` ( (,) ` ( G ` J ) ) ) e. RR )
45 ovolsscl
 |-  ( ( ( ( (,) ` ( F ` z ) ) i^i ( (,) ` ( G ` J ) ) ) C_ ( (,) ` ( G ` J ) ) /\ ( (,) ` ( G ` J ) ) C_ RR /\ ( vol* ` ( (,) ` ( G ` J ) ) ) e. RR ) -> ( vol* ` ( ( (,) ` ( F ` z ) ) i^i ( (,) ` ( G ` J ) ) ) ) e. RR )
46 24 34 44 45 mp3an2i
 |-  ( ( ph /\ J e. NN ) -> ( vol* ` ( ( (,) ` ( F ` z ) ) i^i ( (,) ` ( G ` J ) ) ) ) e. RR )
47 46 adantr
 |-  ( ( ( ph /\ J e. NN ) /\ z e. NN ) -> ( vol* ` ( ( (,) ` ( F ` z ) ) i^i ( (,) ` ( G ` J ) ) ) ) e. RR )
48 12 ioorcl
 |-  ( ( ( ( (,) ` ( F ` z ) ) i^i ( (,) ` ( G ` J ) ) ) e. ran (,) /\ ( vol* ` ( ( (,) ` ( F ` z ) ) i^i ( (,) ` ( G ` J ) ) ) ) e. RR ) -> ( K ` ( ( (,) ` ( F ` z ) ) i^i ( (,) ` ( G ` J ) ) ) ) e. ( <_ i^i ( RR X. RR ) ) )
49 17 47 48 syl2anc
 |-  ( ( ( ph /\ J e. NN ) /\ z e. NN ) -> ( K ` ( ( (,) ` ( F ` z ) ) i^i ( (,) ` ( G ` J ) ) ) ) e. ( <_ i^i ( RR X. RR ) ) )
50 23 49 fmpt3d
 |-  ( ( ph /\ J e. NN ) -> ( K o. H ) : NN --> ( <_ i^i ( RR X. RR ) ) )
51 eqid
 |-  ( ( abs o. - ) o. ( K o. H ) ) = ( ( abs o. - ) o. ( K o. H ) )
52 51 ovolfsf
 |-  ( ( K o. H ) : NN --> ( <_ i^i ( RR X. RR ) ) -> ( ( abs o. - ) o. ( K o. H ) ) : NN --> ( 0 [,) +oo ) )
53 50 52 syl
 |-  ( ( ph /\ J e. NN ) -> ( ( abs o. - ) o. ( K o. H ) ) : NN --> ( 0 [,) +oo ) )
54 53 ffvelrnda
 |-  ( ( ( ph /\ J e. NN ) /\ n e. NN ) -> ( ( ( abs o. - ) o. ( K o. H ) ) ` n ) e. ( 0 [,) +oo ) )
55 elrege0
 |-  ( ( ( ( abs o. - ) o. ( K o. H ) ) ` n ) e. ( 0 [,) +oo ) <-> ( ( ( ( abs o. - ) o. ( K o. H ) ) ` n ) e. RR /\ 0 <_ ( ( ( abs o. - ) o. ( K o. H ) ) ` n ) ) )
56 54 55 sylib
 |-  ( ( ( ph /\ J e. NN ) /\ n e. NN ) -> ( ( ( ( abs o. - ) o. ( K o. H ) ) ` n ) e. RR /\ 0 <_ ( ( ( abs o. - ) o. ( K o. H ) ) ` n ) ) )
57 56 simpld
 |-  ( ( ( ph /\ J e. NN ) /\ n e. NN ) -> ( ( ( abs o. - ) o. ( K o. H ) ) ` n ) e. RR )
58 56 simprd
 |-  ( ( ( ph /\ J e. NN ) /\ n e. NN ) -> 0 <_ ( ( ( abs o. - ) o. ( K o. H ) ) ` n ) )
59 23 fveq1d
 |-  ( ( ph /\ J e. NN ) -> ( ( K o. H ) ` z ) = ( ( z e. NN |-> ( K ` ( ( (,) ` ( F ` z ) ) i^i ( (,) ` ( G ` J ) ) ) ) ) ` z ) )
60 fvex
 |-  ( K ` ( ( (,) ` ( F ` z ) ) i^i ( (,) ` ( G ` J ) ) ) ) e. _V
61 eqid
 |-  ( z e. NN |-> ( K ` ( ( (,) ` ( F ` z ) ) i^i ( (,) ` ( G ` J ) ) ) ) ) = ( z e. NN |-> ( K ` ( ( (,) ` ( F ` z ) ) i^i ( (,) ` ( G ` J ) ) ) ) )
62 61 fvmpt2
 |-  ( ( z e. NN /\ ( K ` ( ( (,) ` ( F ` z ) ) i^i ( (,) ` ( G ` J ) ) ) ) e. _V ) -> ( ( z e. NN |-> ( K ` ( ( (,) ` ( F ` z ) ) i^i ( (,) ` ( G ` J ) ) ) ) ) ` z ) = ( K ` ( ( (,) ` ( F ` z ) ) i^i ( (,) ` ( G ` J ) ) ) ) )
63 60 62 mpan2
 |-  ( z e. NN -> ( ( z e. NN |-> ( K ` ( ( (,) ` ( F ` z ) ) i^i ( (,) ` ( G ` J ) ) ) ) ) ` z ) = ( K ` ( ( (,) ` ( F ` z ) ) i^i ( (,) ` ( G ` J ) ) ) ) )
64 59 63 sylan9eq
 |-  ( ( ( ph /\ J e. NN ) /\ z e. NN ) -> ( ( K o. H ) ` z ) = ( K ` ( ( (,) ` ( F ` z ) ) i^i ( (,) ` ( G ` J ) ) ) ) )
65 64 fveq2d
 |-  ( ( ( ph /\ J e. NN ) /\ z e. NN ) -> ( (,) ` ( ( K o. H ) ` z ) ) = ( (,) ` ( K ` ( ( (,) ` ( F ` z ) ) i^i ( (,) ` ( G ` J ) ) ) ) ) )
66 12 ioorinv
 |-  ( ( ( (,) ` ( F ` z ) ) i^i ( (,) ` ( G ` J ) ) ) e. ran (,) -> ( (,) ` ( K ` ( ( (,) ` ( F ` z ) ) i^i ( (,) ` ( G ` J ) ) ) ) ) = ( ( (,) ` ( F ` z ) ) i^i ( (,) ` ( G ` J ) ) ) )
67 17 66 syl
 |-  ( ( ( ph /\ J e. NN ) /\ z e. NN ) -> ( (,) ` ( K ` ( ( (,) ` ( F ` z ) ) i^i ( (,) ` ( G ` J ) ) ) ) ) = ( ( (,) ` ( F ` z ) ) i^i ( (,) ` ( G ` J ) ) ) )
68 65 67 eqtrd
 |-  ( ( ( ph /\ J e. NN ) /\ z e. NN ) -> ( (,) ` ( ( K o. H ) ` z ) ) = ( ( (,) ` ( F ` z ) ) i^i ( (,) ` ( G ` J ) ) ) )
69 68 ralrimiva
 |-  ( ( ph /\ J e. NN ) -> A. z e. NN ( (,) ` ( ( K o. H ) ` z ) ) = ( ( (,) ` ( F ` z ) ) i^i ( (,) ` ( G ` J ) ) ) )
70 2fveq3
 |-  ( z = x -> ( (,) ` ( ( K o. H ) ` z ) ) = ( (,) ` ( ( K o. H ) ` x ) ) )
71 2fveq3
 |-  ( z = x -> ( (,) ` ( F ` z ) ) = ( (,) ` ( F ` x ) ) )
72 71 ineq1d
 |-  ( z = x -> ( ( (,) ` ( F ` z ) ) i^i ( (,) ` ( G ` J ) ) ) = ( ( (,) ` ( F ` x ) ) i^i ( (,) ` ( G ` J ) ) ) )
73 70 72 eqeq12d
 |-  ( z = x -> ( ( (,) ` ( ( K o. H ) ` z ) ) = ( ( (,) ` ( F ` z ) ) i^i ( (,) ` ( G ` J ) ) ) <-> ( (,) ` ( ( K o. H ) ` x ) ) = ( ( (,) ` ( F ` x ) ) i^i ( (,) ` ( G ` J ) ) ) ) )
74 73 rspccva
 |-  ( ( A. z e. NN ( (,) ` ( ( K o. H ) ` z ) ) = ( ( (,) ` ( F ` z ) ) i^i ( (,) ` ( G ` J ) ) ) /\ x e. NN ) -> ( (,) ` ( ( K o. H ) ` x ) ) = ( ( (,) ` ( F ` x ) ) i^i ( (,) ` ( G ` J ) ) ) )
75 69 74 sylan
 |-  ( ( ( ph /\ J e. NN ) /\ x e. NN ) -> ( (,) ` ( ( K o. H ) ` x ) ) = ( ( (,) ` ( F ` x ) ) i^i ( (,) ` ( G ` J ) ) ) )
76 inss1
 |-  ( ( (,) ` ( F ` x ) ) i^i ( (,) ` ( G ` J ) ) ) C_ ( (,) ` ( F ` x ) )
77 75 76 eqsstrdi
 |-  ( ( ( ph /\ J e. NN ) /\ x e. NN ) -> ( (,) ` ( ( K o. H ) ` x ) ) C_ ( (,) ` ( F ` x ) ) )
78 77 ralrimiva
 |-  ( ( ph /\ J e. NN ) -> A. x e. NN ( (,) ` ( ( K o. H ) ` x ) ) C_ ( (,) ` ( F ` x ) ) )
79 2 adantr
 |-  ( ( ph /\ J e. NN ) -> Disj_ x e. NN ( (,) ` ( F ` x ) ) )
80 disjss2
 |-  ( A. x e. NN ( (,) ` ( ( K o. H ) ` x ) ) C_ ( (,) ` ( F ` x ) ) -> ( Disj_ x e. NN ( (,) ` ( F ` x ) ) -> Disj_ x e. NN ( (,) ` ( ( K o. H ) ` x ) ) ) )
81 78 79 80 sylc
 |-  ( ( ph /\ J e. NN ) -> Disj_ x e. NN ( (,) ` ( ( K o. H ) ` x ) ) )
82 50 81 14 uniioovol
 |-  ( ( ph /\ J e. NN ) -> ( vol* ` U. ran ( (,) o. ( K o. H ) ) ) = sup ( ran seq 1 ( + , ( ( abs o. - ) o. ( K o. H ) ) ) , RR* , < ) )
83 67 mpteq2dva
 |-  ( ( ph /\ J e. NN ) -> ( z e. NN |-> ( (,) ` ( K ` ( ( (,) ` ( F ` z ) ) i^i ( (,) ` ( G ` J ) ) ) ) ) ) = ( z e. NN |-> ( ( (,) ` ( F ` z ) ) i^i ( (,) ` ( G ` J ) ) ) ) )
84 rexpssxrxp
 |-  ( RR X. RR ) C_ ( RR* X. RR* )
85 25 84 sstri
 |-  ( <_ i^i ( RR X. RR ) ) C_ ( RR* X. RR* )
86 85 49 sselid
 |-  ( ( ( ph /\ J e. NN ) /\ z e. NN ) -> ( K ` ( ( (,) ` ( F ` z ) ) i^i ( (,) ` ( G ` J ) ) ) ) e. ( RR* X. RR* ) )
87 ioof
 |-  (,) : ( RR* X. RR* ) --> ~P RR
88 87 a1i
 |-  ( ( ph /\ J e. NN ) -> (,) : ( RR* X. RR* ) --> ~P RR )
89 88 feqmptd
 |-  ( ( ph /\ J e. NN ) -> (,) = ( y e. ( RR* X. RR* ) |-> ( (,) ` y ) ) )
90 fveq2
 |-  ( y = ( K ` ( ( (,) ` ( F ` z ) ) i^i ( (,) ` ( G ` J ) ) ) ) -> ( (,) ` y ) = ( (,) ` ( K ` ( ( (,) ` ( F ` z ) ) i^i ( (,) ` ( G ` J ) ) ) ) ) )
91 86 23 89 90 fmptco
 |-  ( ( ph /\ J e. NN ) -> ( (,) o. ( K o. H ) ) = ( z e. NN |-> ( (,) ` ( K ` ( ( (,) ` ( F ` z ) ) i^i ( (,) ` ( G ` J ) ) ) ) ) ) )
92 83 91 18 3eqtr4d
 |-  ( ( ph /\ J e. NN ) -> ( (,) o. ( K o. H ) ) = H )
93 92 rneqd
 |-  ( ( ph /\ J e. NN ) -> ran ( (,) o. ( K o. H ) ) = ran H )
94 93 unieqd
 |-  ( ( ph /\ J e. NN ) -> U. ran ( (,) o. ( K o. H ) ) = U. ran H )
95 fvex
 |-  ( (,) ` ( F ` z ) ) e. _V
96 95 inex1
 |-  ( ( (,) ` ( F ` z ) ) i^i ( (,) ` ( G ` J ) ) ) e. _V
97 11 fvmpt2
 |-  ( ( z e. NN /\ ( ( (,) ` ( F ` z ) ) i^i ( (,) ` ( G ` J ) ) ) e. _V ) -> ( H ` z ) = ( ( (,) ` ( F ` z ) ) i^i ( (,) ` ( G ` J ) ) ) )
98 96 97 mpan2
 |-  ( z e. NN -> ( H ` z ) = ( ( (,) ` ( F ` z ) ) i^i ( (,) ` ( G ` J ) ) ) )
99 incom
 |-  ( ( (,) ` ( F ` z ) ) i^i ( (,) ` ( G ` J ) ) ) = ( ( (,) ` ( G ` J ) ) i^i ( (,) ` ( F ` z ) ) )
100 98 99 eqtrdi
 |-  ( z e. NN -> ( H ` z ) = ( ( (,) ` ( G ` J ) ) i^i ( (,) ` ( F ` z ) ) ) )
101 100 iuneq2i
 |-  U_ z e. NN ( H ` z ) = U_ z e. NN ( ( (,) ` ( G ` J ) ) i^i ( (,) ` ( F ` z ) ) )
102 iunin2
 |-  U_ z e. NN ( ( (,) ` ( G ` J ) ) i^i ( (,) ` ( F ` z ) ) ) = ( ( (,) ` ( G ` J ) ) i^i U_ z e. NN ( (,) ` ( F ` z ) ) )
103 101 102 eqtri
 |-  U_ z e. NN ( H ` z ) = ( ( (,) ` ( G ` J ) ) i^i U_ z e. NN ( (,) ` ( F ` z ) ) )
104 17 11 fmptd
 |-  ( ( ph /\ J e. NN ) -> H : NN --> ran (,) )
105 104 ffnd
 |-  ( ( ph /\ J e. NN ) -> H Fn NN )
106 fniunfv
 |-  ( H Fn NN -> U_ z e. NN ( H ` z ) = U. ran H )
107 105 106 syl
 |-  ( ( ph /\ J e. NN ) -> U_ z e. NN ( H ` z ) = U. ran H )
108 103 107 eqtr3id
 |-  ( ( ph /\ J e. NN ) -> ( ( (,) ` ( G ` J ) ) i^i U_ z e. NN ( (,) ` ( F ` z ) ) ) = U. ran H )
109 1 adantr
 |-  ( ( ph /\ J e. NN ) -> F : NN --> ( <_ i^i ( RR X. RR ) ) )
110 fvco3
 |-  ( ( F : NN --> ( <_ i^i ( RR X. RR ) ) /\ z e. NN ) -> ( ( (,) o. F ) ` z ) = ( (,) ` ( F ` z ) ) )
111 109 110 sylan
 |-  ( ( ( ph /\ J e. NN ) /\ z e. NN ) -> ( ( (,) o. F ) ` z ) = ( (,) ` ( F ` z ) ) )
112 111 iuneq2dv
 |-  ( ( ph /\ J e. NN ) -> U_ z e. NN ( ( (,) o. F ) ` z ) = U_ z e. NN ( (,) ` ( F ` z ) ) )
113 ffn
 |-  ( (,) : ( RR* X. RR* ) --> ~P RR -> (,) Fn ( RR* X. RR* ) )
114 87 113 ax-mp
 |-  (,) Fn ( RR* X. RR* )
115 fss
 |-  ( ( F : NN --> ( <_ i^i ( RR X. RR ) ) /\ ( <_ i^i ( RR X. RR ) ) C_ ( RR* X. RR* ) ) -> F : NN --> ( RR* X. RR* ) )
116 109 85 115 sylancl
 |-  ( ( ph /\ J e. NN ) -> F : NN --> ( RR* X. RR* ) )
117 fnfco
 |-  ( ( (,) Fn ( RR* X. RR* ) /\ F : NN --> ( RR* X. RR* ) ) -> ( (,) o. F ) Fn NN )
118 114 116 117 sylancr
 |-  ( ( ph /\ J e. NN ) -> ( (,) o. F ) Fn NN )
119 fniunfv
 |-  ( ( (,) o. F ) Fn NN -> U_ z e. NN ( ( (,) o. F ) ` z ) = U. ran ( (,) o. F ) )
120 118 119 syl
 |-  ( ( ph /\ J e. NN ) -> U_ z e. NN ( ( (,) o. F ) ` z ) = U. ran ( (,) o. F ) )
121 120 4 eqtr4di
 |-  ( ( ph /\ J e. NN ) -> U_ z e. NN ( ( (,) o. F ) ` z ) = A )
122 112 121 eqtr3d
 |-  ( ( ph /\ J e. NN ) -> U_ z e. NN ( (,) ` ( F ` z ) ) = A )
123 122 ineq2d
 |-  ( ( ph /\ J e. NN ) -> ( ( (,) ` ( G ` J ) ) i^i U_ z e. NN ( (,) ` ( F ` z ) ) ) = ( ( (,) ` ( G ` J ) ) i^i A ) )
124 94 108 123 3eqtr2d
 |-  ( ( ph /\ J e. NN ) -> U. ran ( (,) o. ( K o. H ) ) = ( ( (,) ` ( G ` J ) ) i^i A ) )
125 124 fveq2d
 |-  ( ( ph /\ J e. NN ) -> ( vol* ` U. ran ( (,) o. ( K o. H ) ) ) = ( vol* ` ( ( (,) ` ( G ` J ) ) i^i A ) ) )
126 82 125 eqtr3d
 |-  ( ( ph /\ J e. NN ) -> sup ( ran seq 1 ( + , ( ( abs o. - ) o. ( K o. H ) ) ) , RR* , < ) = ( vol* ` ( ( (,) ` ( G ` J ) ) i^i A ) ) )
127 inss1
 |-  ( ( (,) ` ( G ` J ) ) i^i A ) C_ ( (,) ` ( G ` J ) )
128 ovolsscl
 |-  ( ( ( ( (,) ` ( G ` J ) ) i^i A ) C_ ( (,) ` ( G ` J ) ) /\ ( (,) ` ( G ` J ) ) C_ RR /\ ( vol* ` ( (,) ` ( G ` J ) ) ) e. RR ) -> ( vol* ` ( ( (,) ` ( G ` J ) ) i^i A ) ) e. RR )
129 127 34 44 128 mp3an2i
 |-  ( ( ph /\ J e. NN ) -> ( vol* ` ( ( (,) ` ( G ` J ) ) i^i A ) ) e. RR )
130 126 129 eqeltrd
 |-  ( ( ph /\ J e. NN ) -> sup ( ran seq 1 ( + , ( ( abs o. - ) o. ( K o. H ) ) ) , RR* , < ) e. RR )
131 51 14 ovolsf
 |-  ( ( K o. H ) : NN --> ( <_ i^i ( RR X. RR ) ) -> seq 1 ( + , ( ( abs o. - ) o. ( K o. H ) ) ) : NN --> ( 0 [,) +oo ) )
132 50 131 syl
 |-  ( ( ph /\ J e. NN ) -> seq 1 ( + , ( ( abs o. - ) o. ( K o. H ) ) ) : NN --> ( 0 [,) +oo ) )
133 132 frnd
 |-  ( ( ph /\ J e. NN ) -> ran seq 1 ( + , ( ( abs o. - ) o. ( K o. H ) ) ) C_ ( 0 [,) +oo ) )
134 icossxr
 |-  ( 0 [,) +oo ) C_ RR*
135 133 134 sstrdi
 |-  ( ( ph /\ J e. NN ) -> ran seq 1 ( + , ( ( abs o. - ) o. ( K o. H ) ) ) C_ RR* )
136 132 ffnd
 |-  ( ( ph /\ J e. NN ) -> seq 1 ( + , ( ( abs o. - ) o. ( K o. H ) ) ) Fn NN )
137 fnfvelrn
 |-  ( ( seq 1 ( + , ( ( abs o. - ) o. ( K o. H ) ) ) Fn NN /\ y e. NN ) -> ( seq 1 ( + , ( ( abs o. - ) o. ( K o. H ) ) ) ` y ) e. ran seq 1 ( + , ( ( abs o. - ) o. ( K o. H ) ) ) )
138 136 137 sylan
 |-  ( ( ( ph /\ J e. NN ) /\ y e. NN ) -> ( seq 1 ( + , ( ( abs o. - ) o. ( K o. H ) ) ) ` y ) e. ran seq 1 ( + , ( ( abs o. - ) o. ( K o. H ) ) ) )
139 supxrub
 |-  ( ( ran seq 1 ( + , ( ( abs o. - ) o. ( K o. H ) ) ) C_ RR* /\ ( seq 1 ( + , ( ( abs o. - ) o. ( K o. H ) ) ) ` y ) e. ran seq 1 ( + , ( ( abs o. - ) o. ( K o. H ) ) ) ) -> ( seq 1 ( + , ( ( abs o. - ) o. ( K o. H ) ) ) ` y ) <_ sup ( ran seq 1 ( + , ( ( abs o. - ) o. ( K o. H ) ) ) , RR* , < ) )
140 135 138 139 syl2an2r
 |-  ( ( ( ph /\ J e. NN ) /\ y e. NN ) -> ( seq 1 ( + , ( ( abs o. - ) o. ( K o. H ) ) ) ` y ) <_ sup ( ran seq 1 ( + , ( ( abs o. - ) o. ( K o. H ) ) ) , RR* , < ) )
141 140 ralrimiva
 |-  ( ( ph /\ J e. NN ) -> A. y e. NN ( seq 1 ( + , ( ( abs o. - ) o. ( K o. H ) ) ) ` y ) <_ sup ( ran seq 1 ( + , ( ( abs o. - ) o. ( K o. H ) ) ) , RR* , < ) )
142 brralrspcev
 |-  ( ( sup ( ran seq 1 ( + , ( ( abs o. - ) o. ( K o. H ) ) ) , RR* , < ) e. RR /\ A. y e. NN ( seq 1 ( + , ( ( abs o. - ) o. ( K o. H ) ) ) ` y ) <_ sup ( ran seq 1 ( + , ( ( abs o. - ) o. ( K o. H ) ) ) , RR* , < ) ) -> E. x e. RR A. y e. NN ( seq 1 ( + , ( ( abs o. - ) o. ( K o. H ) ) ) ` y ) <_ x )
143 130 141 142 syl2anc
 |-  ( ( ph /\ J e. NN ) -> E. x e. RR A. y e. NN ( seq 1 ( + , ( ( abs o. - ) o. ( K o. H ) ) ) ` y ) <_ x )
144 13 14 15 16 57 58 143 isumsup2
 |-  ( ( ph /\ J e. NN ) -> seq 1 ( + , ( ( abs o. - ) o. ( K o. H ) ) ) ~~> sup ( ran seq 1 ( + , ( ( abs o. - ) o. ( K o. H ) ) ) , RR , < ) )
145 51 ovolfs2
 |-  ( ( K o. H ) : NN --> ( <_ i^i ( RR X. RR ) ) -> ( ( abs o. - ) o. ( K o. H ) ) = ( ( vol* o. (,) ) o. ( K o. H ) ) )
146 50 145 syl
 |-  ( ( ph /\ J e. NN ) -> ( ( abs o. - ) o. ( K o. H ) ) = ( ( vol* o. (,) ) o. ( K o. H ) ) )
147 coass
 |-  ( ( vol* o. (,) ) o. ( K o. H ) ) = ( vol* o. ( (,) o. ( K o. H ) ) )
148 92 coeq2d
 |-  ( ( ph /\ J e. NN ) -> ( vol* o. ( (,) o. ( K o. H ) ) ) = ( vol* o. H ) )
149 147 148 eqtrid
 |-  ( ( ph /\ J e. NN ) -> ( ( vol* o. (,) ) o. ( K o. H ) ) = ( vol* o. H ) )
150 146 149 eqtrd
 |-  ( ( ph /\ J e. NN ) -> ( ( abs o. - ) o. ( K o. H ) ) = ( vol* o. H ) )
151 150 seqeq3d
 |-  ( ( ph /\ J e. NN ) -> seq 1 ( + , ( ( abs o. - ) o. ( K o. H ) ) ) = seq 1 ( + , ( vol* o. H ) ) )
152 rge0ssre
 |-  ( 0 [,) +oo ) C_ RR
153 133 152 sstrdi
 |-  ( ( ph /\ J e. NN ) -> ran seq 1 ( + , ( ( abs o. - ) o. ( K o. H ) ) ) C_ RR )
154 1nn
 |-  1 e. NN
155 132 fdmd
 |-  ( ( ph /\ J e. NN ) -> dom seq 1 ( + , ( ( abs o. - ) o. ( K o. H ) ) ) = NN )
156 154 155 eleqtrrid
 |-  ( ( ph /\ J e. NN ) -> 1 e. dom seq 1 ( + , ( ( abs o. - ) o. ( K o. H ) ) ) )
157 156 ne0d
 |-  ( ( ph /\ J e. NN ) -> dom seq 1 ( + , ( ( abs o. - ) o. ( K o. H ) ) ) =/= (/) )
158 dm0rn0
 |-  ( dom seq 1 ( + , ( ( abs o. - ) o. ( K o. H ) ) ) = (/) <-> ran seq 1 ( + , ( ( abs o. - ) o. ( K o. H ) ) ) = (/) )
159 158 necon3bii
 |-  ( dom seq 1 ( + , ( ( abs o. - ) o. ( K o. H ) ) ) =/= (/) <-> ran seq 1 ( + , ( ( abs o. - ) o. ( K o. H ) ) ) =/= (/) )
160 157 159 sylib
 |-  ( ( ph /\ J e. NN ) -> ran seq 1 ( + , ( ( abs o. - ) o. ( K o. H ) ) ) =/= (/) )
161 breq1
 |-  ( z = ( seq 1 ( + , ( ( abs o. - ) o. ( K o. H ) ) ) ` y ) -> ( z <_ x <-> ( seq 1 ( + , ( ( abs o. - ) o. ( K o. H ) ) ) ` y ) <_ x ) )
162 161 ralrn
 |-  ( seq 1 ( + , ( ( abs o. - ) o. ( K o. H ) ) ) Fn NN -> ( A. z e. ran seq 1 ( + , ( ( abs o. - ) o. ( K o. H ) ) ) z <_ x <-> A. y e. NN ( seq 1 ( + , ( ( abs o. - ) o. ( K o. H ) ) ) ` y ) <_ x ) )
163 136 162 syl
 |-  ( ( ph /\ J e. NN ) -> ( A. z e. ran seq 1 ( + , ( ( abs o. - ) o. ( K o. H ) ) ) z <_ x <-> A. y e. NN ( seq 1 ( + , ( ( abs o. - ) o. ( K o. H ) ) ) ` y ) <_ x ) )
164 163 rexbidv
 |-  ( ( ph /\ J e. NN ) -> ( E. x e. RR A. z e. ran seq 1 ( + , ( ( abs o. - ) o. ( K o. H ) ) ) z <_ x <-> E. x e. RR A. y e. NN ( seq 1 ( + , ( ( abs o. - ) o. ( K o. H ) ) ) ` y ) <_ x ) )
165 143 164 mpbird
 |-  ( ( ph /\ J e. NN ) -> E. x e. RR A. z e. ran seq 1 ( + , ( ( abs o. - ) o. ( K o. H ) ) ) z <_ x )
166 supxrre
 |-  ( ( ran seq 1 ( + , ( ( abs o. - ) o. ( K o. H ) ) ) C_ RR /\ ran seq 1 ( + , ( ( abs o. - ) o. ( K o. H ) ) ) =/= (/) /\ E. x e. RR A. z e. ran seq 1 ( + , ( ( abs o. - ) o. ( K o. H ) ) ) z <_ x ) -> sup ( ran seq 1 ( + , ( ( abs o. - ) o. ( K o. H ) ) ) , RR* , < ) = sup ( ran seq 1 ( + , ( ( abs o. - ) o. ( K o. H ) ) ) , RR , < ) )
167 153 160 165 166 syl3anc
 |-  ( ( ph /\ J e. NN ) -> sup ( ran seq 1 ( + , ( ( abs o. - ) o. ( K o. H ) ) ) , RR* , < ) = sup ( ran seq 1 ( + , ( ( abs o. - ) o. ( K o. H ) ) ) , RR , < ) )
168 167 126 eqtr3d
 |-  ( ( ph /\ J e. NN ) -> sup ( ran seq 1 ( + , ( ( abs o. - ) o. ( K o. H ) ) ) , RR , < ) = ( vol* ` ( ( (,) ` ( G ` J ) ) i^i A ) ) )
169 144 151 168 3brtr3d
 |-  ( ( ph /\ J e. NN ) -> seq 1 ( + , ( vol* o. H ) ) ~~> ( vol* ` ( ( (,) ` ( G ` J ) ) i^i A ) ) )