This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem volsup2

Description: The volume of A is the supremum of the sequence vol*( A i^i ( -u n , n ) ) of volumes of bounded sets. (Contributed by Mario Carneiro, 30-Aug-2014)

Ref Expression
Assertion volsup2 
|- ( ( A e. dom vol /\ B e. RR /\ B < ( vol ` A ) ) -> E. n e. NN B < ( vol ` ( A i^i ( -u n [,] n ) ) ) )

Proof

Step Hyp Ref Expression
1 simp3 
 |-  ( ( A e. dom vol /\ B e. RR /\ B < ( vol ` A ) ) -> B < ( vol ` A ) )
2 rexr 
 |-  ( B e. RR -> B e. RR* )
3 2 3ad2ant2 
 |-  ( ( A e. dom vol /\ B e. RR /\ B < ( vol ` A ) ) -> B e. RR* )
4 iccssxr 
 |-  ( 0 [,] +oo ) C_ RR*
5 volf 
 |-  vol : dom vol --> ( 0 [,] +oo )
6 5 ffvelcdmi 
 |-  ( A e. dom vol -> ( vol ` A ) e. ( 0 [,] +oo ) )
7 4 6 sselid 
 |-  ( A e. dom vol -> ( vol ` A ) e. RR* )
8 7 3ad2ant1 
 |-  ( ( A e. dom vol /\ B e. RR /\ B < ( vol ` A ) ) -> ( vol ` A ) e. RR* )
9 xrltnle 
 |-  ( ( B e. RR* /\ ( vol ` A ) e. RR* ) -> ( B < ( vol ` A ) <-> -. ( vol ` A ) <_ B ) )
10 3 8 9 syl2anc 
 |-  ( ( A e. dom vol /\ B e. RR /\ B < ( vol ` A ) ) -> ( B < ( vol ` A ) <-> -. ( vol ` A ) <_ B ) )
11 1 10 mpbid 
 |-  ( ( A e. dom vol /\ B e. RR /\ B < ( vol ` A ) ) -> -. ( vol ` A ) <_ B )
12 negeq 
 |-  ( m = n -> -u m = -u n )
13 id 
 |-  ( m = n -> m = n )
14 12 13 oveq12d 
 |-  ( m = n -> ( -u m [,] m ) = ( -u n [,] n ) )
15 14 ineq2d 
 |-  ( m = n -> ( A i^i ( -u m [,] m ) ) = ( A i^i ( -u n [,] n ) ) )
16 eqid 
 |-  ( m e. NN |-> ( A i^i ( -u m [,] m ) ) ) = ( m e. NN |-> ( A i^i ( -u m [,] m ) ) )
17 ovex 
 |-  ( -u n [,] n ) e. _V
18 17 inex2 
 |-  ( A i^i ( -u n [,] n ) ) e. _V
19 15 16 18 fvmpt 
 |-  ( n e. NN -> ( ( m e. NN |-> ( A i^i ( -u m [,] m ) ) ) ` n ) = ( A i^i ( -u n [,] n ) ) )
20 19 iuneq2i 
 |-  U_ n e. NN ( ( m e. NN |-> ( A i^i ( -u m [,] m ) ) ) ` n ) = U_ n e. NN ( A i^i ( -u n [,] n ) )
21 iunin2 
 |-  U_ n e. NN ( A i^i ( -u n [,] n ) ) = ( A i^i U_ n e. NN ( -u n [,] n ) )
22 20 21 eqtri 
 |-  U_ n e. NN ( ( m e. NN |-> ( A i^i ( -u m [,] m ) ) ) ` n ) = ( A i^i U_ n e. NN ( -u n [,] n ) )
23 simpl1 
 |-  ( ( ( A e. dom vol /\ B e. RR /\ B < ( vol ` A ) ) /\ n e. NN ) -> A e. dom vol )
24 nnre 
 |-  ( n e. NN -> n e. RR )
25 24 adantl 
 |-  ( ( ( A e. dom vol /\ B e. RR /\ B < ( vol ` A ) ) /\ n e. NN ) -> n e. RR )
26 25 renegcld 
 |-  ( ( ( A e. dom vol /\ B e. RR /\ B < ( vol ` A ) ) /\ n e. NN ) -> -u n e. RR )
27 iccmbl 
 |-  ( ( -u n e. RR /\ n e. RR ) -> ( -u n [,] n ) e. dom vol )
28 26 25 27 syl2anc 
 |-  ( ( ( A e. dom vol /\ B e. RR /\ B < ( vol ` A ) ) /\ n e. NN ) -> ( -u n [,] n ) e. dom vol )
29 inmbl 
 |-  ( ( A e. dom vol /\ ( -u n [,] n ) e. dom vol ) -> ( A i^i ( -u n [,] n ) ) e. dom vol )
30 23 28 29 syl2anc 
 |-  ( ( ( A e. dom vol /\ B e. RR /\ B < ( vol ` A ) ) /\ n e. NN ) -> ( A i^i ( -u n [,] n ) ) e. dom vol )
31 15 cbvmptv 
 |-  ( m e. NN |-> ( A i^i ( -u m [,] m ) ) ) = ( n e. NN |-> ( A i^i ( -u n [,] n ) ) )
32 30 31 fmptd 
 |-  ( ( A e. dom vol /\ B e. RR /\ B < ( vol ` A ) ) -> ( m e. NN |-> ( A i^i ( -u m [,] m ) ) ) : NN --> dom vol )
33 32 ffnd 
 |-  ( ( A e. dom vol /\ B e. RR /\ B < ( vol ` A ) ) -> ( m e. NN |-> ( A i^i ( -u m [,] m ) ) ) Fn NN )
34 fniunfv 
 |-  ( ( m e. NN |-> ( A i^i ( -u m [,] m ) ) ) Fn NN -> U_ n e. NN ( ( m e. NN |-> ( A i^i ( -u m [,] m ) ) ) ` n ) = U. ran ( m e. NN |-> ( A i^i ( -u m [,] m ) ) ) )
35 33 34 syl 
 |-  ( ( A e. dom vol /\ B e. RR /\ B < ( vol ` A ) ) -> U_ n e. NN ( ( m e. NN |-> ( A i^i ( -u m [,] m ) ) ) ` n ) = U. ran ( m e. NN |-> ( A i^i ( -u m [,] m ) ) ) )
36 mblss 
 |-  ( A e. dom vol -> A C_ RR )
37 36 3ad2ant1 
 |-  ( ( A e. dom vol /\ B e. RR /\ B < ( vol ` A ) ) -> A C_ RR )
38 37 sselda 
 |-  ( ( ( A e. dom vol /\ B e. RR /\ B < ( vol ` A ) ) /\ x e. A ) -> x e. RR )
39 recn 
 |-  ( x e. RR -> x e. CC )
40 39 abscld 
 |-  ( x e. RR -> ( abs ` x ) e. RR )
41 arch 
 |-  ( ( abs ` x ) e. RR -> E. n e. NN ( abs ` x ) < n )
42 40 41 syl 
 |-  ( x e. RR -> E. n e. NN ( abs ` x ) < n )
43 ltle 
 |-  ( ( ( abs ` x ) e. RR /\ n e. RR ) -> ( ( abs ` x ) < n -> ( abs ` x ) <_ n ) )
44 40 24 43 syl2an 
 |-  ( ( x e. RR /\ n e. NN ) -> ( ( abs ` x ) < n -> ( abs ` x ) <_ n ) )
45 id 
 |-  ( ( x e. RR /\ -u n <_ x /\ x <_ n ) -> ( x e. RR /\ -u n <_ x /\ x <_ n ) )
46 45 3expib 
 |-  ( x e. RR -> ( ( -u n <_ x /\ x <_ n ) -> ( x e. RR /\ -u n <_ x /\ x <_ n ) ) )
47 46 adantr 
 |-  ( ( x e. RR /\ n e. NN ) -> ( ( -u n <_ x /\ x <_ n ) -> ( x e. RR /\ -u n <_ x /\ x <_ n ) ) )
48 absle 
 |-  ( ( x e. RR /\ n e. RR ) -> ( ( abs ` x ) <_ n <-> ( -u n <_ x /\ x <_ n ) ) )
49 24 48 sylan2 
 |-  ( ( x e. RR /\ n e. NN ) -> ( ( abs ` x ) <_ n <-> ( -u n <_ x /\ x <_ n ) ) )
50 24 adantl 
 |-  ( ( x e. RR /\ n e. NN ) -> n e. RR )
51 50 renegcld 
 |-  ( ( x e. RR /\ n e. NN ) -> -u n e. RR )
52 elicc2 
 |-  ( ( -u n e. RR /\ n e. RR ) -> ( x e. ( -u n [,] n ) <-> ( x e. RR /\ -u n <_ x /\ x <_ n ) ) )
53 51 50 52 syl2anc 
 |-  ( ( x e. RR /\ n e. NN ) -> ( x e. ( -u n [,] n ) <-> ( x e. RR /\ -u n <_ x /\ x <_ n ) ) )
54 47 49 53 3imtr4d 
 |-  ( ( x e. RR /\ n e. NN ) -> ( ( abs ` x ) <_ n -> x e. ( -u n [,] n ) ) )
55 44 54 syld 
 |-  ( ( x e. RR /\ n e. NN ) -> ( ( abs ` x ) < n -> x e. ( -u n [,] n ) ) )
56 55 reximdva 
 |-  ( x e. RR -> ( E. n e. NN ( abs ` x ) < n -> E. n e. NN x e. ( -u n [,] n ) ) )
57 42 56 mpd 
 |-  ( x e. RR -> E. n e. NN x e. ( -u n [,] n ) )
58 38 57 syl 
 |-  ( ( ( A e. dom vol /\ B e. RR /\ B < ( vol ` A ) ) /\ x e. A ) -> E. n e. NN x e. ( -u n [,] n ) )
59 58 ex 
 |-  ( ( A e. dom vol /\ B e. RR /\ B < ( vol ` A ) ) -> ( x e. A -> E. n e. NN x e. ( -u n [,] n ) ) )
60 eliun 
 |-  ( x e. U_ n e. NN ( -u n [,] n ) <-> E. n e. NN x e. ( -u n [,] n ) )
61 59 60 imbitrrdi 
 |-  ( ( A e. dom vol /\ B e. RR /\ B < ( vol ` A ) ) -> ( x e. A -> x e. U_ n e. NN ( -u n [,] n ) ) )
62 61 ssrdv 
 |-  ( ( A e. dom vol /\ B e. RR /\ B < ( vol ` A ) ) -> A C_ U_ n e. NN ( -u n [,] n ) )
63 dfss2 
 |-  ( A C_ U_ n e. NN ( -u n [,] n ) <-> ( A i^i U_ n e. NN ( -u n [,] n ) ) = A )
64 62 63 sylib 
 |-  ( ( A e. dom vol /\ B e. RR /\ B < ( vol ` A ) ) -> ( A i^i U_ n e. NN ( -u n [,] n ) ) = A )
65 22 35 64 3eqtr3a 
 |-  ( ( A e. dom vol /\ B e. RR /\ B < ( vol ` A ) ) -> U. ran ( m e. NN |-> ( A i^i ( -u m [,] m ) ) ) = A )
66 65 fveq2d 
 |-  ( ( A e. dom vol /\ B e. RR /\ B < ( vol ` A ) ) -> ( vol ` U. ran ( m e. NN |-> ( A i^i ( -u m [,] m ) ) ) ) = ( vol ` A ) )
67 peano2re 
 |-  ( n e. RR -> ( n + 1 ) e. RR )
68 25 67 syl 
 |-  ( ( ( A e. dom vol /\ B e. RR /\ B < ( vol ` A ) ) /\ n e. NN ) -> ( n + 1 ) e. RR )
69 68 renegcld 
 |-  ( ( ( A e. dom vol /\ B e. RR /\ B < ( vol ` A ) ) /\ n e. NN ) -> -u ( n + 1 ) e. RR )
70 25 lep1d 
 |-  ( ( ( A e. dom vol /\ B e. RR /\ B < ( vol ` A ) ) /\ n e. NN ) -> n <_ ( n + 1 ) )
71 25 68 lenegd 
 |-  ( ( ( A e. dom vol /\ B e. RR /\ B < ( vol ` A ) ) /\ n e. NN ) -> ( n <_ ( n + 1 ) <-> -u ( n + 1 ) <_ -u n ) )
72 70 71 mpbid 
 |-  ( ( ( A e. dom vol /\ B e. RR /\ B < ( vol ` A ) ) /\ n e. NN ) -> -u ( n + 1 ) <_ -u n )
73 iccss 
 |-  ( ( ( -u ( n + 1 ) e. RR /\ ( n + 1 ) e. RR ) /\ ( -u ( n + 1 ) <_ -u n /\ n <_ ( n + 1 ) ) ) -> ( -u n [,] n ) C_ ( -u ( n + 1 ) [,] ( n + 1 ) ) )
74 69 68 72 70 73 syl22anc 
 |-  ( ( ( A e. dom vol /\ B e. RR /\ B < ( vol ` A ) ) /\ n e. NN ) -> ( -u n [,] n ) C_ ( -u ( n + 1 ) [,] ( n + 1 ) ) )
75 sslin 
 |-  ( ( -u n [,] n ) C_ ( -u ( n + 1 ) [,] ( n + 1 ) ) -> ( A i^i ( -u n [,] n ) ) C_ ( A i^i ( -u ( n + 1 ) [,] ( n + 1 ) ) ) )
76 74 75 syl 
 |-  ( ( ( A e. dom vol /\ B e. RR /\ B < ( vol ` A ) ) /\ n e. NN ) -> ( A i^i ( -u n [,] n ) ) C_ ( A i^i ( -u ( n + 1 ) [,] ( n + 1 ) ) ) )
77 19 adantl 
 |-  ( ( ( A e. dom vol /\ B e. RR /\ B < ( vol ` A ) ) /\ n e. NN ) -> ( ( m e. NN |-> ( A i^i ( -u m [,] m ) ) ) ` n ) = ( A i^i ( -u n [,] n ) ) )
78 peano2nn 
 |-  ( n e. NN -> ( n + 1 ) e. NN )
79 78 adantl 
 |-  ( ( ( A e. dom vol /\ B e. RR /\ B < ( vol ` A ) ) /\ n e. NN ) -> ( n + 1 ) e. NN )
80 negeq 
 |-  ( m = ( n + 1 ) -> -u m = -u ( n + 1 ) )
81 id 
 |-  ( m = ( n + 1 ) -> m = ( n + 1 ) )
82 80 81 oveq12d 
 |-  ( m = ( n + 1 ) -> ( -u m [,] m ) = ( -u ( n + 1 ) [,] ( n + 1 ) ) )
83 82 ineq2d 
 |-  ( m = ( n + 1 ) -> ( A i^i ( -u m [,] m ) ) = ( A i^i ( -u ( n + 1 ) [,] ( n + 1 ) ) ) )
84 ovex 
 |-  ( -u ( n + 1 ) [,] ( n + 1 ) ) e. _V
85 84 inex2 
 |-  ( A i^i ( -u ( n + 1 ) [,] ( n + 1 ) ) ) e. _V
86 83 16 85 fvmpt 
 |-  ( ( n + 1 ) e. NN -> ( ( m e. NN |-> ( A i^i ( -u m [,] m ) ) ) ` ( n + 1 ) ) = ( A i^i ( -u ( n + 1 ) [,] ( n + 1 ) ) ) )
87 79 86 syl 
 |-  ( ( ( A e. dom vol /\ B e. RR /\ B < ( vol ` A ) ) /\ n e. NN ) -> ( ( m e. NN |-> ( A i^i ( -u m [,] m ) ) ) ` ( n + 1 ) ) = ( A i^i ( -u ( n + 1 ) [,] ( n + 1 ) ) ) )
88 76 77 87 3sstr4d 
 |-  ( ( ( A e. dom vol /\ B e. RR /\ B < ( vol ` A ) ) /\ n e. NN ) -> ( ( m e. NN |-> ( A i^i ( -u m [,] m ) ) ) ` n ) C_ ( ( m e. NN |-> ( A i^i ( -u m [,] m ) ) ) ` ( n + 1 ) ) )
89 88 ralrimiva 
 |-  ( ( A e. dom vol /\ B e. RR /\ B < ( vol ` A ) ) -> A. n e. NN ( ( m e. NN |-> ( A i^i ( -u m [,] m ) ) ) ` n ) C_ ( ( m e. NN |-> ( A i^i ( -u m [,] m ) ) ) ` ( n + 1 ) ) )
90 volsup 
 |-  ( ( ( m e. NN |-> ( A i^i ( -u m [,] m ) ) ) : NN --> dom vol /\ A. n e. NN ( ( m e. NN |-> ( A i^i ( -u m [,] m ) ) ) ` n ) C_ ( ( m e. NN |-> ( A i^i ( -u m [,] m ) ) ) ` ( n + 1 ) ) ) -> ( vol ` U. ran ( m e. NN |-> ( A i^i ( -u m [,] m ) ) ) ) = sup ( ( vol " ran ( m e. NN |-> ( A i^i ( -u m [,] m ) ) ) ) , RR* , < ) )
91 32 89 90 syl2anc 
 |-  ( ( A e. dom vol /\ B e. RR /\ B < ( vol ` A ) ) -> ( vol ` U. ran ( m e. NN |-> ( A i^i ( -u m [,] m ) ) ) ) = sup ( ( vol " ran ( m e. NN |-> ( A i^i ( -u m [,] m ) ) ) ) , RR* , < ) )
92 66 91 eqtr3d 
 |-  ( ( A e. dom vol /\ B e. RR /\ B < ( vol ` A ) ) -> ( vol ` A ) = sup ( ( vol " ran ( m e. NN |-> ( A i^i ( -u m [,] m ) ) ) ) , RR* , < ) )
93 92 breq1d 
 |-  ( ( A e. dom vol /\ B e. RR /\ B < ( vol ` A ) ) -> ( ( vol ` A ) <_ B <-> sup ( ( vol " ran ( m e. NN |-> ( A i^i ( -u m [,] m ) ) ) ) , RR* , < ) <_ B ) )
94 imassrn 
 |-  ( vol " ran ( m e. NN |-> ( A i^i ( -u m [,] m ) ) ) ) C_ ran vol
95 frn 
 |-  ( vol : dom vol --> ( 0 [,] +oo ) -> ran vol C_ ( 0 [,] +oo ) )
96 5 95 ax-mp 
 |-  ran vol C_ ( 0 [,] +oo )
97 96 4 sstri 
 |-  ran vol C_ RR*
98 94 97 sstri 
 |-  ( vol " ran ( m e. NN |-> ( A i^i ( -u m [,] m ) ) ) ) C_ RR*
99 supxrleub 
 |-  ( ( ( vol " ran ( m e. NN |-> ( A i^i ( -u m [,] m ) ) ) ) C_ RR* /\ B e. RR* ) -> ( sup ( ( vol " ran ( m e. NN |-> ( A i^i ( -u m [,] m ) ) ) ) , RR* , < ) <_ B <-> A. n e. ( vol " ran ( m e. NN |-> ( A i^i ( -u m [,] m ) ) ) ) n <_ B ) )
100 98 3 99 sylancr 
 |-  ( ( A e. dom vol /\ B e. RR /\ B < ( vol ` A ) ) -> ( sup ( ( vol " ran ( m e. NN |-> ( A i^i ( -u m [,] m ) ) ) ) , RR* , < ) <_ B <-> A. n e. ( vol " ran ( m e. NN |-> ( A i^i ( -u m [,] m ) ) ) ) n <_ B ) )
101 ffn 
 |-  ( vol : dom vol --> ( 0 [,] +oo ) -> vol Fn dom vol )
102 5 101 ax-mp 
 |-  vol Fn dom vol
103 32 frnd 
 |-  ( ( A e. dom vol /\ B e. RR /\ B < ( vol ` A ) ) -> ran ( m e. NN |-> ( A i^i ( -u m [,] m ) ) ) C_ dom vol )
104 breq1 
 |-  ( n = ( vol ` z ) -> ( n <_ B <-> ( vol ` z ) <_ B ) )
105 104 ralima 
 |-  ( ( vol Fn dom vol /\ ran ( m e. NN |-> ( A i^i ( -u m [,] m ) ) ) C_ dom vol ) -> ( A. n e. ( vol " ran ( m e. NN |-> ( A i^i ( -u m [,] m ) ) ) ) n <_ B <-> A. z e. ran ( m e. NN |-> ( A i^i ( -u m [,] m ) ) ) ( vol ` z ) <_ B ) )
106 102 103 105 sylancr 
 |-  ( ( A e. dom vol /\ B e. RR /\ B < ( vol ` A ) ) -> ( A. n e. ( vol " ran ( m e. NN |-> ( A i^i ( -u m [,] m ) ) ) ) n <_ B <-> A. z e. ran ( m e. NN |-> ( A i^i ( -u m [,] m ) ) ) ( vol ` z ) <_ B ) )
107 fveq2 
 |-  ( z = ( ( m e. NN |-> ( A i^i ( -u m [,] m ) ) ) ` n ) -> ( vol ` z ) = ( vol ` ( ( m e. NN |-> ( A i^i ( -u m [,] m ) ) ) ` n ) ) )
108 107 breq1d 
 |-  ( z = ( ( m e. NN |-> ( A i^i ( -u m [,] m ) ) ) ` n ) -> ( ( vol ` z ) <_ B <-> ( vol ` ( ( m e. NN |-> ( A i^i ( -u m [,] m ) ) ) ` n ) ) <_ B ) )
109 108 ralrn 
 |-  ( ( m e. NN |-> ( A i^i ( -u m [,] m ) ) ) Fn NN -> ( A. z e. ran ( m e. NN |-> ( A i^i ( -u m [,] m ) ) ) ( vol ` z ) <_ B <-> A. n e. NN ( vol ` ( ( m e. NN |-> ( A i^i ( -u m [,] m ) ) ) ` n ) ) <_ B ) )
110 33 109 syl 
 |-  ( ( A e. dom vol /\ B e. RR /\ B < ( vol ` A ) ) -> ( A. z e. ran ( m e. NN |-> ( A i^i ( -u m [,] m ) ) ) ( vol ` z ) <_ B <-> A. n e. NN ( vol ` ( ( m e. NN |-> ( A i^i ( -u m [,] m ) ) ) ` n ) ) <_ B ) )
111 19 fveq2d 
 |-  ( n e. NN -> ( vol ` ( ( m e. NN |-> ( A i^i ( -u m [,] m ) ) ) ` n ) ) = ( vol ` ( A i^i ( -u n [,] n ) ) ) )
112 111 breq1d 
 |-  ( n e. NN -> ( ( vol ` ( ( m e. NN |-> ( A i^i ( -u m [,] m ) ) ) ` n ) ) <_ B <-> ( vol ` ( A i^i ( -u n [,] n ) ) ) <_ B ) )
113 112 ralbiia 
 |-  ( A. n e. NN ( vol ` ( ( m e. NN |-> ( A i^i ( -u m [,] m ) ) ) ` n ) ) <_ B <-> A. n e. NN ( vol ` ( A i^i ( -u n [,] n ) ) ) <_ B )
114 110 113 bitrdi 
 |-  ( ( A e. dom vol /\ B e. RR /\ B < ( vol ` A ) ) -> ( A. z e. ran ( m e. NN |-> ( A i^i ( -u m [,] m ) ) ) ( vol ` z ) <_ B <-> A. n e. NN ( vol ` ( A i^i ( -u n [,] n ) ) ) <_ B ) )
115 106 114 bitrd 
 |-  ( ( A e. dom vol /\ B e. RR /\ B < ( vol ` A ) ) -> ( A. n e. ( vol " ran ( m e. NN |-> ( A i^i ( -u m [,] m ) ) ) ) n <_ B <-> A. n e. NN ( vol ` ( A i^i ( -u n [,] n ) ) ) <_ B ) )
116 93 100 115 3bitrd 
 |-  ( ( A e. dom vol /\ B e. RR /\ B < ( vol ` A ) ) -> ( ( vol ` A ) <_ B <-> A. n e. NN ( vol ` ( A i^i ( -u n [,] n ) ) ) <_ B ) )
117 11 116 mtbid 
 |-  ( ( A e. dom vol /\ B e. RR /\ B < ( vol ` A ) ) -> -. A. n e. NN ( vol ` ( A i^i ( -u n [,] n ) ) ) <_ B )
118 rexnal 
 |-  ( E. n e. NN -. ( vol ` ( A i^i ( -u n [,] n ) ) ) <_ B <-> -. A. n e. NN ( vol ` ( A i^i ( -u n [,] n ) ) ) <_ B )
119 117 118 sylibr 
 |-  ( ( A e. dom vol /\ B e. RR /\ B < ( vol ` A ) ) -> E. n e. NN -. ( vol ` ( A i^i ( -u n [,] n ) ) ) <_ B )
120 3 adantr 
 |-  ( ( ( A e. dom vol /\ B e. RR /\ B < ( vol ` A ) ) /\ n e. NN ) -> B e. RR* )
121 5 ffvelcdmi 
 |-  ( ( A i^i ( -u n [,] n ) ) e. dom vol -> ( vol ` ( A i^i ( -u n [,] n ) ) ) e. ( 0 [,] +oo ) )
122 4 121 sselid 
 |-  ( ( A i^i ( -u n [,] n ) ) e. dom vol -> ( vol ` ( A i^i ( -u n [,] n ) ) ) e. RR* )
123 30 122 syl 
 |-  ( ( ( A e. dom vol /\ B e. RR /\ B < ( vol ` A ) ) /\ n e. NN ) -> ( vol ` ( A i^i ( -u n [,] n ) ) ) e. RR* )
124 xrltnle 
 |-  ( ( B e. RR* /\ ( vol ` ( A i^i ( -u n [,] n ) ) ) e. RR* ) -> ( B < ( vol ` ( A i^i ( -u n [,] n ) ) ) <-> -. ( vol ` ( A i^i ( -u n [,] n ) ) ) <_ B ) )
125 120 123 124 syl2anc 
 |-  ( ( ( A e. dom vol /\ B e. RR /\ B < ( vol ` A ) ) /\ n e. NN ) -> ( B < ( vol ` ( A i^i ( -u n [,] n ) ) ) <-> -. ( vol ` ( A i^i ( -u n [,] n ) ) ) <_ B ) )
126 125 rexbidva 
 |-  ( ( A e. dom vol /\ B e. RR /\ B < ( vol ` A ) ) -> ( E. n e. NN B < ( vol ` ( A i^i ( -u n [,] n ) ) ) <-> E. n e. NN -. ( vol ` ( A i^i ( -u n [,] n ) ) ) <_ B ) )
127 119 126 mpbird 
 |-  ( ( A e. dom vol /\ B e. RR /\ B < ( vol ` A ) ) -> E. n e. NN B < ( vol ` ( A i^i ( -u n [,] n ) ) ) )