Metamath Proof Explorer


Theorem voliunlem3

Description: Lemma for voliun . (Contributed by Mario Carneiro, 20-Mar-2014)

Ref Expression
Hypotheses voliunlem.3
|- ( ph -> F : NN --> dom vol )
voliunlem.5
|- ( ph -> Disj_ i e. NN ( F ` i ) )
voliunlem.6
|- H = ( n e. NN |-> ( vol* ` ( x i^i ( F ` n ) ) ) )
voliunlem3.1
|- S = seq 1 ( + , G )
voliunlem3.2
|- G = ( n e. NN |-> ( vol ` ( F ` n ) ) )
voliunlem3.4
|- ( ph -> A. i e. NN ( vol ` ( F ` i ) ) e. RR )
Assertion voliunlem3
|- ( ph -> ( vol ` U. ran F ) = sup ( ran S , RR* , < ) )

Proof

Step Hyp Ref Expression
1 voliunlem.3
 |-  ( ph -> F : NN --> dom vol )
2 voliunlem.5
 |-  ( ph -> Disj_ i e. NN ( F ` i ) )
3 voliunlem.6
 |-  H = ( n e. NN |-> ( vol* ` ( x i^i ( F ` n ) ) ) )
4 voliunlem3.1
 |-  S = seq 1 ( + , G )
5 voliunlem3.2
 |-  G = ( n e. NN |-> ( vol ` ( F ` n ) ) )
6 voliunlem3.4
 |-  ( ph -> A. i e. NN ( vol ` ( F ` i ) ) e. RR )
7 1 2 3 voliunlem2
 |-  ( ph -> U. ran F e. dom vol )
8 mblvol
 |-  ( U. ran F e. dom vol -> ( vol ` U. ran F ) = ( vol* ` U. ran F ) )
9 7 8 syl
 |-  ( ph -> ( vol ` U. ran F ) = ( vol* ` U. ran F ) )
10 1 frnd
 |-  ( ph -> ran F C_ dom vol )
11 mblss
 |-  ( x e. dom vol -> x C_ RR )
12 reex
 |-  RR e. _V
13 12 elpw2
 |-  ( x e. ~P RR <-> x C_ RR )
14 11 13 sylibr
 |-  ( x e. dom vol -> x e. ~P RR )
15 14 ssriv
 |-  dom vol C_ ~P RR
16 10 15 sstrdi
 |-  ( ph -> ran F C_ ~P RR )
17 sspwuni
 |-  ( ran F C_ ~P RR <-> U. ran F C_ RR )
18 16 17 sylib
 |-  ( ph -> U. ran F C_ RR )
19 ovolcl
 |-  ( U. ran F C_ RR -> ( vol* ` U. ran F ) e. RR* )
20 18 19 syl
 |-  ( ph -> ( vol* ` U. ran F ) e. RR* )
21 nnuz
 |-  NN = ( ZZ>= ` 1 )
22 1zzd
 |-  ( ph -> 1 e. ZZ )
23 2fveq3
 |-  ( n = k -> ( vol ` ( F ` n ) ) = ( vol ` ( F ` k ) ) )
24 fvex
 |-  ( vol ` ( F ` k ) ) e. _V
25 23 5 24 fvmpt
 |-  ( k e. NN -> ( G ` k ) = ( vol ` ( F ` k ) ) )
26 25 adantl
 |-  ( ( ph /\ k e. NN ) -> ( G ` k ) = ( vol ` ( F ` k ) ) )
27 2fveq3
 |-  ( i = k -> ( vol ` ( F ` i ) ) = ( vol ` ( F ` k ) ) )
28 27 eleq1d
 |-  ( i = k -> ( ( vol ` ( F ` i ) ) e. RR <-> ( vol ` ( F ` k ) ) e. RR ) )
29 28 rspccva
 |-  ( ( A. i e. NN ( vol ` ( F ` i ) ) e. RR /\ k e. NN ) -> ( vol ` ( F ` k ) ) e. RR )
30 6 29 sylan
 |-  ( ( ph /\ k e. NN ) -> ( vol ` ( F ` k ) ) e. RR )
31 26 30 eqeltrd
 |-  ( ( ph /\ k e. NN ) -> ( G ` k ) e. RR )
32 21 22 31 serfre
 |-  ( ph -> seq 1 ( + , G ) : NN --> RR )
33 4 feq1i
 |-  ( S : NN --> RR <-> seq 1 ( + , G ) : NN --> RR )
34 32 33 sylibr
 |-  ( ph -> S : NN --> RR )
35 34 frnd
 |-  ( ph -> ran S C_ RR )
36 ressxr
 |-  RR C_ RR*
37 35 36 sstrdi
 |-  ( ph -> ran S C_ RR* )
38 supxrcl
 |-  ( ran S C_ RR* -> sup ( ran S , RR* , < ) e. RR* )
39 37 38 syl
 |-  ( ph -> sup ( ran S , RR* , < ) e. RR* )
40 eqid
 |-  seq 1 ( + , ( n e. NN |-> ( vol* ` ( F ` n ) ) ) ) = seq 1 ( + , ( n e. NN |-> ( vol* ` ( F ` n ) ) ) )
41 eqid
 |-  ( n e. NN |-> ( vol* ` ( F ` n ) ) ) = ( n e. NN |-> ( vol* ` ( F ` n ) ) )
42 1 ffvelrnda
 |-  ( ( ph /\ n e. NN ) -> ( F ` n ) e. dom vol )
43 mblss
 |-  ( ( F ` n ) e. dom vol -> ( F ` n ) C_ RR )
44 42 43 syl
 |-  ( ( ph /\ n e. NN ) -> ( F ` n ) C_ RR )
45 mblvol
 |-  ( ( F ` n ) e. dom vol -> ( vol ` ( F ` n ) ) = ( vol* ` ( F ` n ) ) )
46 42 45 syl
 |-  ( ( ph /\ n e. NN ) -> ( vol ` ( F ` n ) ) = ( vol* ` ( F ` n ) ) )
47 2fveq3
 |-  ( i = n -> ( vol ` ( F ` i ) ) = ( vol ` ( F ` n ) ) )
48 47 eleq1d
 |-  ( i = n -> ( ( vol ` ( F ` i ) ) e. RR <-> ( vol ` ( F ` n ) ) e. RR ) )
49 48 rspccva
 |-  ( ( A. i e. NN ( vol ` ( F ` i ) ) e. RR /\ n e. NN ) -> ( vol ` ( F ` n ) ) e. RR )
50 6 49 sylan
 |-  ( ( ph /\ n e. NN ) -> ( vol ` ( F ` n ) ) e. RR )
51 46 50 eqeltrrd
 |-  ( ( ph /\ n e. NN ) -> ( vol* ` ( F ` n ) ) e. RR )
52 40 41 44 51 ovoliun
 |-  ( ph -> ( vol* ` U_ n e. NN ( F ` n ) ) <_ sup ( ran seq 1 ( + , ( n e. NN |-> ( vol* ` ( F ` n ) ) ) ) , RR* , < ) )
53 1 ffnd
 |-  ( ph -> F Fn NN )
54 fniunfv
 |-  ( F Fn NN -> U_ n e. NN ( F ` n ) = U. ran F )
55 53 54 syl
 |-  ( ph -> U_ n e. NN ( F ` n ) = U. ran F )
56 55 fveq2d
 |-  ( ph -> ( vol* ` U_ n e. NN ( F ` n ) ) = ( vol* ` U. ran F ) )
57 46 mpteq2dva
 |-  ( ph -> ( n e. NN |-> ( vol ` ( F ` n ) ) ) = ( n e. NN |-> ( vol* ` ( F ` n ) ) ) )
58 5 57 syl5eq
 |-  ( ph -> G = ( n e. NN |-> ( vol* ` ( F ` n ) ) ) )
59 58 seqeq3d
 |-  ( ph -> seq 1 ( + , G ) = seq 1 ( + , ( n e. NN |-> ( vol* ` ( F ` n ) ) ) ) )
60 4 59 eqtr2id
 |-  ( ph -> seq 1 ( + , ( n e. NN |-> ( vol* ` ( F ` n ) ) ) ) = S )
61 60 rneqd
 |-  ( ph -> ran seq 1 ( + , ( n e. NN |-> ( vol* ` ( F ` n ) ) ) ) = ran S )
62 61 supeq1d
 |-  ( ph -> sup ( ran seq 1 ( + , ( n e. NN |-> ( vol* ` ( F ` n ) ) ) ) , RR* , < ) = sup ( ran S , RR* , < ) )
63 52 56 62 3brtr3d
 |-  ( ph -> ( vol* ` U. ran F ) <_ sup ( ran S , RR* , < ) )
64 ovolge0
 |-  ( U. ran F C_ RR -> 0 <_ ( vol* ` U. ran F ) )
65 18 64 syl
 |-  ( ph -> 0 <_ ( vol* ` U. ran F ) )
66 mnflt0
 |-  -oo < 0
67 mnfxr
 |-  -oo e. RR*
68 0xr
 |-  0 e. RR*
69 xrltletr
 |-  ( ( -oo e. RR* /\ 0 e. RR* /\ ( vol* ` U. ran F ) e. RR* ) -> ( ( -oo < 0 /\ 0 <_ ( vol* ` U. ran F ) ) -> -oo < ( vol* ` U. ran F ) ) )
70 67 68 69 mp3an12
 |-  ( ( vol* ` U. ran F ) e. RR* -> ( ( -oo < 0 /\ 0 <_ ( vol* ` U. ran F ) ) -> -oo < ( vol* ` U. ran F ) ) )
71 66 70 mpani
 |-  ( ( vol* ` U. ran F ) e. RR* -> ( 0 <_ ( vol* ` U. ran F ) -> -oo < ( vol* ` U. ran F ) ) )
72 20 65 71 sylc
 |-  ( ph -> -oo < ( vol* ` U. ran F ) )
73 xrrebnd
 |-  ( ( vol* ` U. ran F ) e. RR* -> ( ( vol* ` U. ran F ) e. RR <-> ( -oo < ( vol* ` U. ran F ) /\ ( vol* ` U. ran F ) < +oo ) ) )
74 20 73 syl
 |-  ( ph -> ( ( vol* ` U. ran F ) e. RR <-> ( -oo < ( vol* ` U. ran F ) /\ ( vol* ` U. ran F ) < +oo ) ) )
75 12 elpw2
 |-  ( U. ran F e. ~P RR <-> U. ran F C_ RR )
76 18 75 sylibr
 |-  ( ph -> U. ran F e. ~P RR )
77 simpl
 |-  ( ( x = U. ran F /\ ph ) -> x = U. ran F )
78 77 sseq1d
 |-  ( ( x = U. ran F /\ ph ) -> ( x C_ RR <-> U. ran F C_ RR ) )
79 77 fveq2d
 |-  ( ( x = U. ran F /\ ph ) -> ( vol* ` x ) = ( vol* ` U. ran F ) )
80 79 eleq1d
 |-  ( ( x = U. ran F /\ ph ) -> ( ( vol* ` x ) e. RR <-> ( vol* ` U. ran F ) e. RR ) )
81 simpll
 |-  ( ( ( x = U. ran F /\ ph ) /\ n e. NN ) -> x = U. ran F )
82 81 ineq1d
 |-  ( ( ( x = U. ran F /\ ph ) /\ n e. NN ) -> ( x i^i ( F ` n ) ) = ( U. ran F i^i ( F ` n ) ) )
83 fnfvelrn
 |-  ( ( F Fn NN /\ n e. NN ) -> ( F ` n ) e. ran F )
84 53 83 sylan
 |-  ( ( ph /\ n e. NN ) -> ( F ` n ) e. ran F )
85 elssuni
 |-  ( ( F ` n ) e. ran F -> ( F ` n ) C_ U. ran F )
86 84 85 syl
 |-  ( ( ph /\ n e. NN ) -> ( F ` n ) C_ U. ran F )
87 86 adantll
 |-  ( ( ( x = U. ran F /\ ph ) /\ n e. NN ) -> ( F ` n ) C_ U. ran F )
88 sseqin2
 |-  ( ( F ` n ) C_ U. ran F <-> ( U. ran F i^i ( F ` n ) ) = ( F ` n ) )
89 87 88 sylib
 |-  ( ( ( x = U. ran F /\ ph ) /\ n e. NN ) -> ( U. ran F i^i ( F ` n ) ) = ( F ` n ) )
90 82 89 eqtrd
 |-  ( ( ( x = U. ran F /\ ph ) /\ n e. NN ) -> ( x i^i ( F ` n ) ) = ( F ` n ) )
91 90 fveq2d
 |-  ( ( ( x = U. ran F /\ ph ) /\ n e. NN ) -> ( vol* ` ( x i^i ( F ` n ) ) ) = ( vol* ` ( F ` n ) ) )
92 46 adantll
 |-  ( ( ( x = U. ran F /\ ph ) /\ n e. NN ) -> ( vol ` ( F ` n ) ) = ( vol* ` ( F ` n ) ) )
93 91 92 eqtr4d
 |-  ( ( ( x = U. ran F /\ ph ) /\ n e. NN ) -> ( vol* ` ( x i^i ( F ` n ) ) ) = ( vol ` ( F ` n ) ) )
94 93 mpteq2dva
 |-  ( ( x = U. ran F /\ ph ) -> ( n e. NN |-> ( vol* ` ( x i^i ( F ` n ) ) ) ) = ( n e. NN |-> ( vol ` ( F ` n ) ) ) )
95 94 adantrr
 |-  ( ( x = U. ran F /\ ( ph /\ k e. NN ) ) -> ( n e. NN |-> ( vol* ` ( x i^i ( F ` n ) ) ) ) = ( n e. NN |-> ( vol ` ( F ` n ) ) ) )
96 95 3 5 3eqtr4g
 |-  ( ( x = U. ran F /\ ( ph /\ k e. NN ) ) -> H = G )
97 96 seqeq3d
 |-  ( ( x = U. ran F /\ ( ph /\ k e. NN ) ) -> seq 1 ( + , H ) = seq 1 ( + , G ) )
98 97 4 eqtr4di
 |-  ( ( x = U. ran F /\ ( ph /\ k e. NN ) ) -> seq 1 ( + , H ) = S )
99 98 fveq1d
 |-  ( ( x = U. ran F /\ ( ph /\ k e. NN ) ) -> ( seq 1 ( + , H ) ` k ) = ( S ` k ) )
100 difeq1
 |-  ( x = U. ran F -> ( x \ U. ran F ) = ( U. ran F \ U. ran F ) )
101 difid
 |-  ( U. ran F \ U. ran F ) = (/)
102 100 101 eqtrdi
 |-  ( x = U. ran F -> ( x \ U. ran F ) = (/) )
103 102 fveq2d
 |-  ( x = U. ran F -> ( vol* ` ( x \ U. ran F ) ) = ( vol* ` (/) ) )
104 ovol0
 |-  ( vol* ` (/) ) = 0
105 103 104 eqtrdi
 |-  ( x = U. ran F -> ( vol* ` ( x \ U. ran F ) ) = 0 )
106 105 adantr
 |-  ( ( x = U. ran F /\ ( ph /\ k e. NN ) ) -> ( vol* ` ( x \ U. ran F ) ) = 0 )
107 99 106 oveq12d
 |-  ( ( x = U. ran F /\ ( ph /\ k e. NN ) ) -> ( ( seq 1 ( + , H ) ` k ) + ( vol* ` ( x \ U. ran F ) ) ) = ( ( S ` k ) + 0 ) )
108 34 ffvelrnda
 |-  ( ( ph /\ k e. NN ) -> ( S ` k ) e. RR )
109 108 adantl
 |-  ( ( x = U. ran F /\ ( ph /\ k e. NN ) ) -> ( S ` k ) e. RR )
110 109 recnd
 |-  ( ( x = U. ran F /\ ( ph /\ k e. NN ) ) -> ( S ` k ) e. CC )
111 110 addid1d
 |-  ( ( x = U. ran F /\ ( ph /\ k e. NN ) ) -> ( ( S ` k ) + 0 ) = ( S ` k ) )
112 107 111 eqtrd
 |-  ( ( x = U. ran F /\ ( ph /\ k e. NN ) ) -> ( ( seq 1 ( + , H ) ` k ) + ( vol* ` ( x \ U. ran F ) ) ) = ( S ` k ) )
113 fveq2
 |-  ( x = U. ran F -> ( vol* ` x ) = ( vol* ` U. ran F ) )
114 113 adantr
 |-  ( ( x = U. ran F /\ ( ph /\ k e. NN ) ) -> ( vol* ` x ) = ( vol* ` U. ran F ) )
115 112 114 breq12d
 |-  ( ( x = U. ran F /\ ( ph /\ k e. NN ) ) -> ( ( ( seq 1 ( + , H ) ` k ) + ( vol* ` ( x \ U. ran F ) ) ) <_ ( vol* ` x ) <-> ( S ` k ) <_ ( vol* ` U. ran F ) ) )
116 115 expr
 |-  ( ( x = U. ran F /\ ph ) -> ( k e. NN -> ( ( ( seq 1 ( + , H ) ` k ) + ( vol* ` ( x \ U. ran F ) ) ) <_ ( vol* ` x ) <-> ( S ` k ) <_ ( vol* ` U. ran F ) ) ) )
117 116 pm5.74d
 |-  ( ( x = U. ran F /\ ph ) -> ( ( k e. NN -> ( ( seq 1 ( + , H ) ` k ) + ( vol* ` ( x \ U. ran F ) ) ) <_ ( vol* ` x ) ) <-> ( k e. NN -> ( S ` k ) <_ ( vol* ` U. ran F ) ) ) )
118 80 117 imbi12d
 |-  ( ( x = U. ran F /\ ph ) -> ( ( ( vol* ` x ) e. RR -> ( k e. NN -> ( ( seq 1 ( + , H ) ` k ) + ( vol* ` ( x \ U. ran F ) ) ) <_ ( vol* ` x ) ) ) <-> ( ( vol* ` U. ran F ) e. RR -> ( k e. NN -> ( S ` k ) <_ ( vol* ` U. ran F ) ) ) ) )
119 78 118 imbi12d
 |-  ( ( x = U. ran F /\ ph ) -> ( ( x C_ RR -> ( ( vol* ` x ) e. RR -> ( k e. NN -> ( ( seq 1 ( + , H ) ` k ) + ( vol* ` ( x \ U. ran F ) ) ) <_ ( vol* ` x ) ) ) ) <-> ( U. ran F C_ RR -> ( ( vol* ` U. ran F ) e. RR -> ( k e. NN -> ( S ` k ) <_ ( vol* ` U. ran F ) ) ) ) ) )
120 119 pm5.74da
 |-  ( x = U. ran F -> ( ( ph -> ( x C_ RR -> ( ( vol* ` x ) e. RR -> ( k e. NN -> ( ( seq 1 ( + , H ) ` k ) + ( vol* ` ( x \ U. ran F ) ) ) <_ ( vol* ` x ) ) ) ) ) <-> ( ph -> ( U. ran F C_ RR -> ( ( vol* ` U. ran F ) e. RR -> ( k e. NN -> ( S ` k ) <_ ( vol* ` U. ran F ) ) ) ) ) ) )
121 1 3ad2ant1
 |-  ( ( ph /\ x C_ RR /\ ( vol* ` x ) e. RR ) -> F : NN --> dom vol )
122 2 3ad2ant1
 |-  ( ( ph /\ x C_ RR /\ ( vol* ` x ) e. RR ) -> Disj_ i e. NN ( F ` i ) )
123 simp2
 |-  ( ( ph /\ x C_ RR /\ ( vol* ` x ) e. RR ) -> x C_ RR )
124 simp3
 |-  ( ( ph /\ x C_ RR /\ ( vol* ` x ) e. RR ) -> ( vol* ` x ) e. RR )
125 121 122 3 123 124 voliunlem1
 |-  ( ( ( ph /\ x C_ RR /\ ( vol* ` x ) e. RR ) /\ k e. NN ) -> ( ( seq 1 ( + , H ) ` k ) + ( vol* ` ( x \ U. ran F ) ) ) <_ ( vol* ` x ) )
126 125 3exp1
 |-  ( ph -> ( x C_ RR -> ( ( vol* ` x ) e. RR -> ( k e. NN -> ( ( seq 1 ( + , H ) ` k ) + ( vol* ` ( x \ U. ran F ) ) ) <_ ( vol* ` x ) ) ) ) )
127 120 126 vtoclg
 |-  ( U. ran F e. ~P RR -> ( ph -> ( U. ran F C_ RR -> ( ( vol* ` U. ran F ) e. RR -> ( k e. NN -> ( S ` k ) <_ ( vol* ` U. ran F ) ) ) ) ) )
128 76 127 mpcom
 |-  ( ph -> ( U. ran F C_ RR -> ( ( vol* ` U. ran F ) e. RR -> ( k e. NN -> ( S ` k ) <_ ( vol* ` U. ran F ) ) ) ) )
129 18 128 mpd
 |-  ( ph -> ( ( vol* ` U. ran F ) e. RR -> ( k e. NN -> ( S ` k ) <_ ( vol* ` U. ran F ) ) ) )
130 74 129 sylbird
 |-  ( ph -> ( ( -oo < ( vol* ` U. ran F ) /\ ( vol* ` U. ran F ) < +oo ) -> ( k e. NN -> ( S ` k ) <_ ( vol* ` U. ran F ) ) ) )
131 72 130 mpand
 |-  ( ph -> ( ( vol* ` U. ran F ) < +oo -> ( k e. NN -> ( S ` k ) <_ ( vol* ` U. ran F ) ) ) )
132 nltpnft
 |-  ( ( vol* ` U. ran F ) e. RR* -> ( ( vol* ` U. ran F ) = +oo <-> -. ( vol* ` U. ran F ) < +oo ) )
133 20 132 syl
 |-  ( ph -> ( ( vol* ` U. ran F ) = +oo <-> -. ( vol* ` U. ran F ) < +oo ) )
134 rexr
 |-  ( ( S ` k ) e. RR -> ( S ` k ) e. RR* )
135 pnfge
 |-  ( ( S ` k ) e. RR* -> ( S ` k ) <_ +oo )
136 108 134 135 3syl
 |-  ( ( ph /\ k e. NN ) -> ( S ` k ) <_ +oo )
137 136 ex
 |-  ( ph -> ( k e. NN -> ( S ` k ) <_ +oo ) )
138 breq2
 |-  ( ( vol* ` U. ran F ) = +oo -> ( ( S ` k ) <_ ( vol* ` U. ran F ) <-> ( S ` k ) <_ +oo ) )
139 138 imbi2d
 |-  ( ( vol* ` U. ran F ) = +oo -> ( ( k e. NN -> ( S ` k ) <_ ( vol* ` U. ran F ) ) <-> ( k e. NN -> ( S ` k ) <_ +oo ) ) )
140 137 139 syl5ibrcom
 |-  ( ph -> ( ( vol* ` U. ran F ) = +oo -> ( k e. NN -> ( S ` k ) <_ ( vol* ` U. ran F ) ) ) )
141 133 140 sylbird
 |-  ( ph -> ( -. ( vol* ` U. ran F ) < +oo -> ( k e. NN -> ( S ` k ) <_ ( vol* ` U. ran F ) ) ) )
142 131 141 pm2.61d
 |-  ( ph -> ( k e. NN -> ( S ` k ) <_ ( vol* ` U. ran F ) ) )
143 142 ralrimiv
 |-  ( ph -> A. k e. NN ( S ` k ) <_ ( vol* ` U. ran F ) )
144 34 ffnd
 |-  ( ph -> S Fn NN )
145 breq1
 |-  ( z = ( S ` k ) -> ( z <_ ( vol* ` U. ran F ) <-> ( S ` k ) <_ ( vol* ` U. ran F ) ) )
146 145 ralrn
 |-  ( S Fn NN -> ( A. z e. ran S z <_ ( vol* ` U. ran F ) <-> A. k e. NN ( S ` k ) <_ ( vol* ` U. ran F ) ) )
147 144 146 syl
 |-  ( ph -> ( A. z e. ran S z <_ ( vol* ` U. ran F ) <-> A. k e. NN ( S ` k ) <_ ( vol* ` U. ran F ) ) )
148 143 147 mpbird
 |-  ( ph -> A. z e. ran S z <_ ( vol* ` U. ran F ) )
149 supxrleub
 |-  ( ( ran S C_ RR* /\ ( vol* ` U. ran F ) e. RR* ) -> ( sup ( ran S , RR* , < ) <_ ( vol* ` U. ran F ) <-> A. z e. ran S z <_ ( vol* ` U. ran F ) ) )
150 37 20 149 syl2anc
 |-  ( ph -> ( sup ( ran S , RR* , < ) <_ ( vol* ` U. ran F ) <-> A. z e. ran S z <_ ( vol* ` U. ran F ) ) )
151 148 150 mpbird
 |-  ( ph -> sup ( ran S , RR* , < ) <_ ( vol* ` U. ran F ) )
152 20 39 63 151 xrletrid
 |-  ( ph -> ( vol* ` U. ran F ) = sup ( ran S , RR* , < ) )
153 9 152 eqtrd
 |-  ( ph -> ( vol ` U. ran F ) = sup ( ran S , RR* , < ) )