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* , < ) )