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 ffvelrni
 |-  ( 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 syl6ibr
 |-  ( ( 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 df-ss
 |-  ( 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 ffvelrni
 |-  ( ( 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 ) ) ) )