Metamath Proof Explorer

Theorem volivth

Description: The Intermediate Value Theorem for the Lebesgue volume function. For any positive B <_ ( volA ) , there is a measurable subset of A whose volume is B . (Contributed by Mario Carneiro, 30-Aug-2014)

Ref Expression
Assertion volivth 
|- ( ( A e. dom vol /\ B e. ( 0 [,] ( vol ` A ) ) ) -> E. x e. dom vol ( x C_ A /\ ( vol ` x ) = B ) )

Proof

Step Hyp Ref Expression
1 simpll 
 |-  ( ( ( A e. dom vol /\ B e. ( 0 [,] ( vol ` A ) ) ) /\ B < ( vol ` A ) ) -> A e. dom vol )
2 mnfxr 
 |-  -oo e. RR*
3 2 a1i 
 |-  ( ( ( A e. dom vol /\ B e. ( 0 [,] ( vol ` A ) ) ) /\ B < ( vol ` A ) ) -> -oo e. RR* )
4 iccssxr 
 |-  ( 0 [,] ( vol ` A ) ) C_ RR*
5 simpr 
 |-  ( ( A e. dom vol /\ B e. ( 0 [,] ( vol ` A ) ) ) -> B e. ( 0 [,] ( vol ` A ) ) )
6 4 5 sseldi 
 |-  ( ( A e. dom vol /\ B e. ( 0 [,] ( vol ` A ) ) ) -> B e. RR* )
7 6 adantr 
 |-  ( ( ( A e. dom vol /\ B e. ( 0 [,] ( vol ` A ) ) ) /\ B < ( vol ` A ) ) -> B e. RR* )
8 iccssxr 
 |-  ( 0 [,] +oo ) C_ RR*
9 volf 
 |-  vol : dom vol --> ( 0 [,] +oo )
10 9 ffvelrni 
 |-  ( A e. dom vol -> ( vol ` A ) e. ( 0 [,] +oo ) )
11 8 10 sseldi 
 |-  ( A e. dom vol -> ( vol ` A ) e. RR* )
12 11 adantr 
 |-  ( ( A e. dom vol /\ B e. ( 0 [,] ( vol ` A ) ) ) -> ( vol ` A ) e. RR* )
13 12 adantr 
 |-  ( ( ( A e. dom vol /\ B e. ( 0 [,] ( vol ` A ) ) ) /\ B < ( vol ` A ) ) -> ( vol ` A ) e. RR* )
14 0xr 
 |-  0 e. RR*
15 elicc1 
 |-  ( ( 0 e. RR* /\ ( vol ` A ) e. RR* ) -> ( B e. ( 0 [,] ( vol ` A ) ) <-> ( B e. RR* /\ 0 <_ B /\ B <_ ( vol ` A ) ) ) )
16 14 12 15 sylancr 
 |-  ( ( A e. dom vol /\ B e. ( 0 [,] ( vol ` A ) ) ) -> ( B e. ( 0 [,] ( vol ` A ) ) <-> ( B e. RR* /\ 0 <_ B /\ B <_ ( vol ` A ) ) ) )
17 5 16 mpbid 
 |-  ( ( A e. dom vol /\ B e. ( 0 [,] ( vol ` A ) ) ) -> ( B e. RR* /\ 0 <_ B /\ B <_ ( vol ` A ) ) )
18 17 simp2d 
 |-  ( ( A e. dom vol /\ B e. ( 0 [,] ( vol ` A ) ) ) -> 0 <_ B )
19 18 adantr 
 |-  ( ( ( A e. dom vol /\ B e. ( 0 [,] ( vol ` A ) ) ) /\ B < ( vol ` A ) ) -> 0 <_ B )
20 mnflt0 
 |-  -oo < 0
21 xrltletr 
 |-  ( ( -oo e. RR* /\ 0 e. RR* /\ B e. RR* ) -> ( ( -oo < 0 /\ 0 <_ B ) -> -oo < B ) )
22 20 21 mpani 
 |-  ( ( -oo e. RR* /\ 0 e. RR* /\ B e. RR* ) -> ( 0 <_ B -> -oo < B ) )
23 2 14 22 mp3an12 
 |-  ( B e. RR* -> ( 0 <_ B -> -oo < B ) )
24 7 19 23 sylc 
 |-  ( ( ( A e. dom vol /\ B e. ( 0 [,] ( vol ` A ) ) ) /\ B < ( vol ` A ) ) -> -oo < B )
25 simpr 
 |-  ( ( ( A e. dom vol /\ B e. ( 0 [,] ( vol ` A ) ) ) /\ B < ( vol ` A ) ) -> B < ( vol ` A ) )
26 xrre2 
 |-  ( ( ( -oo e. RR* /\ B e. RR* /\ ( vol ` A ) e. RR* ) /\ ( -oo < B /\ B < ( vol ` A ) ) ) -> B e. RR )
27 3 7 13 24 25 26 syl32anc 
 |-  ( ( ( A e. dom vol /\ B e. ( 0 [,] ( vol ` A ) ) ) /\ B < ( vol ` A ) ) -> B e. RR )
28 volsup2 
 |-  ( ( A e. dom vol /\ B e. RR /\ B < ( vol ` A ) ) -> E. n e. NN B < ( vol ` ( A i^i ( -u n [,] n ) ) ) )
29 1 27 25 28 syl3anc 
 |-  ( ( ( A e. dom vol /\ B e. ( 0 [,] ( vol ` A ) ) ) /\ B < ( vol ` A ) ) -> E. n e. NN B < ( vol ` ( A i^i ( -u n [,] n ) ) ) )
30 nnre 
 |-  ( n e. NN -> n e. RR )
31 30 ad2antrl 
 |-  ( ( ( ( A e. dom vol /\ B e. ( 0 [,] ( vol ` A ) ) ) /\ B < ( vol ` A ) ) /\ ( n e. NN /\ B < ( vol ` ( A i^i ( -u n [,] n ) ) ) ) ) -> n e. RR )
32 31 renegcld 
 |-  ( ( ( ( A e. dom vol /\ B e. ( 0 [,] ( vol ` A ) ) ) /\ B < ( vol ` A ) ) /\ ( n e. NN /\ B < ( vol ` ( A i^i ( -u n [,] n ) ) ) ) ) -> -u n e. RR )
33 27 adantr 
 |-  ( ( ( ( A e. dom vol /\ B e. ( 0 [,] ( vol ` A ) ) ) /\ B < ( vol ` A ) ) /\ ( n e. NN /\ B < ( vol ` ( A i^i ( -u n [,] n ) ) ) ) ) -> B e. RR )
34 0red 
 |-  ( ( ( ( A e. dom vol /\ B e. ( 0 [,] ( vol ` A ) ) ) /\ B < ( vol ` A ) ) /\ ( n e. NN /\ B < ( vol ` ( A i^i ( -u n [,] n ) ) ) ) ) -> 0 e. RR )
35 nngt0 
 |-  ( n e. NN -> 0 < n )
36 35 ad2antrl 
 |-  ( ( ( ( A e. dom vol /\ B e. ( 0 [,] ( vol ` A ) ) ) /\ B < ( vol ` A ) ) /\ ( n e. NN /\ B < ( vol ` ( A i^i ( -u n [,] n ) ) ) ) ) -> 0 < n )
37 31 lt0neg2d 
 |-  ( ( ( ( A e. dom vol /\ B e. ( 0 [,] ( vol ` A ) ) ) /\ B < ( vol ` A ) ) /\ ( n e. NN /\ B < ( vol ` ( A i^i ( -u n [,] n ) ) ) ) ) -> ( 0 < n <-> -u n < 0 ) )
38 36 37 mpbid 
 |-  ( ( ( ( A e. dom vol /\ B e. ( 0 [,] ( vol ` A ) ) ) /\ B < ( vol ` A ) ) /\ ( n e. NN /\ B < ( vol ` ( A i^i ( -u n [,] n ) ) ) ) ) -> -u n < 0 )
39 32 34 31 38 36 lttrd 
 |-  ( ( ( ( A e. dom vol /\ B e. ( 0 [,] ( vol ` A ) ) ) /\ B < ( vol ` A ) ) /\ ( n e. NN /\ B < ( vol ` ( A i^i ( -u n [,] n ) ) ) ) ) -> -u n < n )
40 iccssre 
 |-  ( ( -u n e. RR /\ n e. RR ) -> ( -u n [,] n ) C_ RR )
41 32 31 40 syl2anc 
 |-  ( ( ( ( A e. dom vol /\ B e. ( 0 [,] ( vol ` A ) ) ) /\ B < ( vol ` A ) ) /\ ( n e. NN /\ B < ( vol ` ( A i^i ( -u n [,] n ) ) ) ) ) -> ( -u n [,] n ) C_ RR )
42 ax-resscn 
 |-  RR C_ CC
43 ssid 
 |-  CC C_ CC
44 cncfss 
 |-  ( ( RR C_ CC /\ CC C_ CC ) -> ( RR -cn-> RR ) C_ ( RR -cn-> CC ) )
45 42 43 44 mp2an 
 |-  ( RR -cn-> RR ) C_ ( RR -cn-> CC )
46 1 adantr 
 |-  ( ( ( ( A e. dom vol /\ B e. ( 0 [,] ( vol ` A ) ) ) /\ B < ( vol ` A ) ) /\ ( n e. NN /\ B < ( vol ` ( A i^i ( -u n [,] n ) ) ) ) ) -> A e. dom vol )
47 eqid 
 |-  ( y e. RR |-> ( vol ` ( A i^i ( -u n [,] y ) ) ) ) = ( y e. RR |-> ( vol ` ( A i^i ( -u n [,] y ) ) ) )
48 47 volcn 
 |-  ( ( A e. dom vol /\ -u n e. RR ) -> ( y e. RR |-> ( vol ` ( A i^i ( -u n [,] y ) ) ) ) e. ( RR -cn-> RR ) )
49 46 32 48 syl2anc 
 |-  ( ( ( ( A e. dom vol /\ B e. ( 0 [,] ( vol ` A ) ) ) /\ B < ( vol ` A ) ) /\ ( n e. NN /\ B < ( vol ` ( A i^i ( -u n [,] n ) ) ) ) ) -> ( y e. RR |-> ( vol ` ( A i^i ( -u n [,] y ) ) ) ) e. ( RR -cn-> RR ) )
50 45 49 sseldi 
 |-  ( ( ( ( A e. dom vol /\ B e. ( 0 [,] ( vol ` A ) ) ) /\ B < ( vol ` A ) ) /\ ( n e. NN /\ B < ( vol ` ( A i^i ( -u n [,] n ) ) ) ) ) -> ( y e. RR |-> ( vol ` ( A i^i ( -u n [,] y ) ) ) ) e. ( RR -cn-> CC ) )
51 41 sselda 
 |-  ( ( ( ( ( A e. dom vol /\ B e. ( 0 [,] ( vol ` A ) ) ) /\ B < ( vol ` A ) ) /\ ( n e. NN /\ B < ( vol ` ( A i^i ( -u n [,] n ) ) ) ) ) /\ u e. ( -u n [,] n ) ) -> u e. RR )
52 cncff 
 |-  ( ( y e. RR |-> ( vol ` ( A i^i ( -u n [,] y ) ) ) ) e. ( RR -cn-> RR ) -> ( y e. RR |-> ( vol ` ( A i^i ( -u n [,] y ) ) ) ) : RR --> RR )
53 49 52 syl 
 |-  ( ( ( ( A e. dom vol /\ B e. ( 0 [,] ( vol ` A ) ) ) /\ B < ( vol ` A ) ) /\ ( n e. NN /\ B < ( vol ` ( A i^i ( -u n [,] n ) ) ) ) ) -> ( y e. RR |-> ( vol ` ( A i^i ( -u n [,] y ) ) ) ) : RR --> RR )
54 53 ffvelrnda 
 |-  ( ( ( ( ( A e. dom vol /\ B e. ( 0 [,] ( vol ` A ) ) ) /\ B < ( vol ` A ) ) /\ ( n e. NN /\ B < ( vol ` ( A i^i ( -u n [,] n ) ) ) ) ) /\ u e. RR ) -> ( ( y e. RR |-> ( vol ` ( A i^i ( -u n [,] y ) ) ) ) ` u ) e. RR )
55 51 54 syldan 
 |-  ( ( ( ( ( A e. dom vol /\ B e. ( 0 [,] ( vol ` A ) ) ) /\ B < ( vol ` A ) ) /\ ( n e. NN /\ B < ( vol ` ( A i^i ( -u n [,] n ) ) ) ) ) /\ u e. ( -u n [,] n ) ) -> ( ( y e. RR |-> ( vol ` ( A i^i ( -u n [,] y ) ) ) ) ` u ) e. RR )
56 oveq2 
 |-  ( y = -u n -> ( -u n [,] y ) = ( -u n [,] -u n ) )
57 56 ineq2d 
 |-  ( y = -u n -> ( A i^i ( -u n [,] y ) ) = ( A i^i ( -u n [,] -u n ) ) )
58 57 fveq2d 
 |-  ( y = -u n -> ( vol ` ( A i^i ( -u n [,] y ) ) ) = ( vol ` ( A i^i ( -u n [,] -u n ) ) ) )
59 fvex 
 |-  ( vol ` ( A i^i ( -u n [,] -u n ) ) ) e. _V
60 58 47 59 fvmpt 
 |-  ( -u n e. RR -> ( ( y e. RR |-> ( vol ` ( A i^i ( -u n [,] y ) ) ) ) ` -u n ) = ( vol ` ( A i^i ( -u n [,] -u n ) ) ) )
61 32 60 syl 
 |-  ( ( ( ( A e. dom vol /\ B e. ( 0 [,] ( vol ` A ) ) ) /\ B < ( vol ` A ) ) /\ ( n e. NN /\ B < ( vol ` ( A i^i ( -u n [,] n ) ) ) ) ) -> ( ( y e. RR |-> ( vol ` ( A i^i ( -u n [,] y ) ) ) ) ` -u n ) = ( vol ` ( A i^i ( -u n [,] -u n ) ) ) )
62 inss2 
 |-  ( A i^i ( -u n [,] -u n ) ) C_ ( -u n [,] -u n )
63 32 rexrd 
 |-  ( ( ( ( A e. dom vol /\ B e. ( 0 [,] ( vol ` A ) ) ) /\ B < ( vol ` A ) ) /\ ( n e. NN /\ B < ( vol ` ( A i^i ( -u n [,] n ) ) ) ) ) -> -u n e. RR* )
64 iccid 
 |-  ( -u n e. RR* -> ( -u n [,] -u n ) = { -u n } )
65 63 64 syl 
 |-  ( ( ( ( A e. dom vol /\ B e. ( 0 [,] ( vol ` A ) ) ) /\ B < ( vol ` A ) ) /\ ( n e. NN /\ B < ( vol ` ( A i^i ( -u n [,] n ) ) ) ) ) -> ( -u n [,] -u n ) = { -u n } )
66 62 65 sseqtrid 
 |-  ( ( ( ( A e. dom vol /\ B e. ( 0 [,] ( vol ` A ) ) ) /\ B < ( vol ` A ) ) /\ ( n e. NN /\ B < ( vol ` ( A i^i ( -u n [,] n ) ) ) ) ) -> ( A i^i ( -u n [,] -u n ) ) C_ { -u n } )
67 32 snssd 
 |-  ( ( ( ( A e. dom vol /\ B e. ( 0 [,] ( vol ` A ) ) ) /\ B < ( vol ` A ) ) /\ ( n e. NN /\ B < ( vol ` ( A i^i ( -u n [,] n ) ) ) ) ) -> { -u n } C_ RR )
68 66 67 sstrd 
 |-  ( ( ( ( A e. dom vol /\ B e. ( 0 [,] ( vol ` A ) ) ) /\ B < ( vol ` A ) ) /\ ( n e. NN /\ B < ( vol ` ( A i^i ( -u n [,] n ) ) ) ) ) -> ( A i^i ( -u n [,] -u n ) ) C_ RR )
69 ovolsn 
 |-  ( -u n e. RR -> ( vol* ` { -u n } ) = 0 )
70 32 69 syl 
 |-  ( ( ( ( A e. dom vol /\ B e. ( 0 [,] ( vol ` A ) ) ) /\ B < ( vol ` A ) ) /\ ( n e. NN /\ B < ( vol ` ( A i^i ( -u n [,] n ) ) ) ) ) -> ( vol* ` { -u n } ) = 0 )
71 ovolssnul 
 |-  ( ( ( A i^i ( -u n [,] -u n ) ) C_ { -u n } /\ { -u n } C_ RR /\ ( vol* ` { -u n } ) = 0 ) -> ( vol* ` ( A i^i ( -u n [,] -u n ) ) ) = 0 )
72 66 67 70 71 syl3anc 
 |-  ( ( ( ( A e. dom vol /\ B e. ( 0 [,] ( vol ` A ) ) ) /\ B < ( vol ` A ) ) /\ ( n e. NN /\ B < ( vol ` ( A i^i ( -u n [,] n ) ) ) ) ) -> ( vol* ` ( A i^i ( -u n [,] -u n ) ) ) = 0 )
73 nulmbl 
 |-  ( ( ( A i^i ( -u n [,] -u n ) ) C_ RR /\ ( vol* ` ( A i^i ( -u n [,] -u n ) ) ) = 0 ) -> ( A i^i ( -u n [,] -u n ) ) e. dom vol )
74 68 72 73 syl2anc 
 |-  ( ( ( ( A e. dom vol /\ B e. ( 0 [,] ( vol ` A ) ) ) /\ B < ( vol ` A ) ) /\ ( n e. NN /\ B < ( vol ` ( A i^i ( -u n [,] n ) ) ) ) ) -> ( A i^i ( -u n [,] -u n ) ) e. dom vol )
75 mblvol 
 |-  ( ( A i^i ( -u n [,] -u n ) ) e. dom vol -> ( vol ` ( A i^i ( -u n [,] -u n ) ) ) = ( vol* ` ( A i^i ( -u n [,] -u n ) ) ) )
76 74 75 syl 
 |-  ( ( ( ( A e. dom vol /\ B e. ( 0 [,] ( vol ` A ) ) ) /\ B < ( vol ` A ) ) /\ ( n e. NN /\ B < ( vol ` ( A i^i ( -u n [,] n ) ) ) ) ) -> ( vol ` ( A i^i ( -u n [,] -u n ) ) ) = ( vol* ` ( A i^i ( -u n [,] -u n ) ) ) )
77 61 76 72 3eqtrd 
 |-  ( ( ( ( A e. dom vol /\ B e. ( 0 [,] ( vol ` A ) ) ) /\ B < ( vol ` A ) ) /\ ( n e. NN /\ B < ( vol ` ( A i^i ( -u n [,] n ) ) ) ) ) -> ( ( y e. RR |-> ( vol ` ( A i^i ( -u n [,] y ) ) ) ) ` -u n ) = 0 )
78 19 adantr 
 |-  ( ( ( ( A e. dom vol /\ B e. ( 0 [,] ( vol ` A ) ) ) /\ B < ( vol ` A ) ) /\ ( n e. NN /\ B < ( vol ` ( A i^i ( -u n [,] n ) ) ) ) ) -> 0 <_ B )
79 77 78 eqbrtrd 
 |-  ( ( ( ( A e. dom vol /\ B e. ( 0 [,] ( vol ` A ) ) ) /\ B < ( vol ` A ) ) /\ ( n e. NN /\ B < ( vol ` ( A i^i ( -u n [,] n ) ) ) ) ) -> ( ( y e. RR |-> ( vol ` ( A i^i ( -u n [,] y ) ) ) ) ` -u n ) <_ B )
80 7 adantr 
 |-  ( ( ( ( A e. dom vol /\ B e. ( 0 [,] ( vol ` A ) ) ) /\ B < ( vol ` A ) ) /\ ( n e. NN /\ B < ( vol ` ( A i^i ( -u n [,] n ) ) ) ) ) -> B e. RR* )
81 iccmbl 
 |-  ( ( -u n e. RR /\ n e. RR ) -> ( -u n [,] n ) e. dom vol )
82 32 31 81 syl2anc 
 |-  ( ( ( ( A e. dom vol /\ B e. ( 0 [,] ( vol ` A ) ) ) /\ B < ( vol ` A ) ) /\ ( n e. NN /\ B < ( vol ` ( A i^i ( -u n [,] n ) ) ) ) ) -> ( -u n [,] n ) e. dom vol )
83 inmbl 
 |-  ( ( A e. dom vol /\ ( -u n [,] n ) e. dom vol ) -> ( A i^i ( -u n [,] n ) ) e. dom vol )
84 46 82 83 syl2anc 
 |-  ( ( ( ( A e. dom vol /\ B e. ( 0 [,] ( vol ` A ) ) ) /\ B < ( vol ` A ) ) /\ ( n e. NN /\ B < ( vol ` ( A i^i ( -u n [,] n ) ) ) ) ) -> ( A i^i ( -u n [,] n ) ) e. dom vol )
85 9 ffvelrni 
 |-  ( ( A i^i ( -u n [,] n ) ) e. dom vol -> ( vol ` ( A i^i ( -u n [,] n ) ) ) e. ( 0 [,] +oo ) )
86 8 85 sseldi 
 |-  ( ( A i^i ( -u n [,] n ) ) e. dom vol -> ( vol ` ( A i^i ( -u n [,] n ) ) ) e. RR* )
87 84 86 syl 
 |-  ( ( ( ( A e. dom vol /\ B e. ( 0 [,] ( vol ` A ) ) ) /\ B < ( vol ` A ) ) /\ ( n e. NN /\ B < ( vol ` ( A i^i ( -u n [,] n ) ) ) ) ) -> ( vol ` ( A i^i ( -u n [,] n ) ) ) e. RR* )
88 simprr 
 |-  ( ( ( ( A e. dom vol /\ B e. ( 0 [,] ( vol ` A ) ) ) /\ B < ( vol ` A ) ) /\ ( n e. NN /\ B < ( vol ` ( A i^i ( -u n [,] n ) ) ) ) ) -> B < ( vol ` ( A i^i ( -u n [,] n ) ) ) )
89 80 87 88 xrltled 
 |-  ( ( ( ( A e. dom vol /\ B e. ( 0 [,] ( vol ` A ) ) ) /\ B < ( vol ` A ) ) /\ ( n e. NN /\ B < ( vol ` ( A i^i ( -u n [,] n ) ) ) ) ) -> B <_ ( vol ` ( A i^i ( -u n [,] n ) ) ) )
90 oveq2 
 |-  ( y = n -> ( -u n [,] y ) = ( -u n [,] n ) )
91 90 ineq2d 
 |-  ( y = n -> ( A i^i ( -u n [,] y ) ) = ( A i^i ( -u n [,] n ) ) )
92 91 fveq2d 
 |-  ( y = n -> ( vol ` ( A i^i ( -u n [,] y ) ) ) = ( vol ` ( A i^i ( -u n [,] n ) ) ) )
93 fvex 
 |-  ( vol ` ( A i^i ( -u n [,] n ) ) ) e. _V
94 92 47 93 fvmpt 
 |-  ( n e. RR -> ( ( y e. RR |-> ( vol ` ( A i^i ( -u n [,] y ) ) ) ) ` n ) = ( vol ` ( A i^i ( -u n [,] n ) ) ) )
95 31 94 syl 
 |-  ( ( ( ( A e. dom vol /\ B e. ( 0 [,] ( vol ` A ) ) ) /\ B < ( vol ` A ) ) /\ ( n e. NN /\ B < ( vol ` ( A i^i ( -u n [,] n ) ) ) ) ) -> ( ( y e. RR |-> ( vol ` ( A i^i ( -u n [,] y ) ) ) ) ` n ) = ( vol ` ( A i^i ( -u n [,] n ) ) ) )
96 89 95 breqtrrd 
 |-  ( ( ( ( A e. dom vol /\ B e. ( 0 [,] ( vol ` A ) ) ) /\ B < ( vol ` A ) ) /\ ( n e. NN /\ B < ( vol ` ( A i^i ( -u n [,] n ) ) ) ) ) -> B <_ ( ( y e. RR |-> ( vol ` ( A i^i ( -u n [,] y ) ) ) ) ` n ) )
97 79 96 jca 
 |-  ( ( ( ( A e. dom vol /\ B e. ( 0 [,] ( vol ` A ) ) ) /\ B < ( vol ` A ) ) /\ ( n e. NN /\ B < ( vol ` ( A i^i ( -u n [,] n ) ) ) ) ) -> ( ( ( y e. RR |-> ( vol ` ( A i^i ( -u n [,] y ) ) ) ) ` -u n ) <_ B /\ B <_ ( ( y e. RR |-> ( vol ` ( A i^i ( -u n [,] y ) ) ) ) ` n ) ) )
98 32 31 33 39 41 50 55 97 ivthle 
 |-  ( ( ( ( A e. dom vol /\ B e. ( 0 [,] ( vol ` A ) ) ) /\ B < ( vol ` A ) ) /\ ( n e. NN /\ B < ( vol ` ( A i^i ( -u n [,] n ) ) ) ) ) -> E. z e. ( -u n [,] n ) ( ( y e. RR |-> ( vol ` ( A i^i ( -u n [,] y ) ) ) ) ` z ) = B )
99 41 sselda 
 |-  ( ( ( ( ( A e. dom vol /\ B e. ( 0 [,] ( vol ` A ) ) ) /\ B < ( vol ` A ) ) /\ ( n e. NN /\ B < ( vol ` ( A i^i ( -u n [,] n ) ) ) ) ) /\ z e. ( -u n [,] n ) ) -> z e. RR )
100 oveq2 
 |-  ( y = z -> ( -u n [,] y ) = ( -u n [,] z ) )
101 100 ineq2d 
 |-  ( y = z -> ( A i^i ( -u n [,] y ) ) = ( A i^i ( -u n [,] z ) ) )
102 101 fveq2d 
 |-  ( y = z -> ( vol ` ( A i^i ( -u n [,] y ) ) ) = ( vol ` ( A i^i ( -u n [,] z ) ) ) )
103 fvex 
 |-  ( vol ` ( A i^i ( -u n [,] z ) ) ) e. _V
104 102 47 103 fvmpt 
 |-  ( z e. RR -> ( ( y e. RR |-> ( vol ` ( A i^i ( -u n [,] y ) ) ) ) ` z ) = ( vol ` ( A i^i ( -u n [,] z ) ) ) )
105 99 104 syl 
 |-  ( ( ( ( ( A e. dom vol /\ B e. ( 0 [,] ( vol ` A ) ) ) /\ B < ( vol ` A ) ) /\ ( n e. NN /\ B < ( vol ` ( A i^i ( -u n [,] n ) ) ) ) ) /\ z e. ( -u n [,] n ) ) -> ( ( y e. RR |-> ( vol ` ( A i^i ( -u n [,] y ) ) ) ) ` z ) = ( vol ` ( A i^i ( -u n [,] z ) ) ) )
106 105 eqeq1d 
 |-  ( ( ( ( ( A e. dom vol /\ B e. ( 0 [,] ( vol ` A ) ) ) /\ B < ( vol ` A ) ) /\ ( n e. NN /\ B < ( vol ` ( A i^i ( -u n [,] n ) ) ) ) ) /\ z e. ( -u n [,] n ) ) -> ( ( ( y e. RR |-> ( vol ` ( A i^i ( -u n [,] y ) ) ) ) ` z ) = B <-> ( vol ` ( A i^i ( -u n [,] z ) ) ) = B ) )
107 46 adantr 
 |-  ( ( ( ( ( A e. dom vol /\ B e. ( 0 [,] ( vol ` A ) ) ) /\ B < ( vol ` A ) ) /\ ( n e. NN /\ B < ( vol ` ( A i^i ( -u n [,] n ) ) ) ) ) /\ ( z e. ( -u n [,] n ) /\ ( vol ` ( A i^i ( -u n [,] z ) ) ) = B ) ) -> A e. dom vol )
108 32 adantr 
 |-  ( ( ( ( ( A e. dom vol /\ B e. ( 0 [,] ( vol ` A ) ) ) /\ B < ( vol ` A ) ) /\ ( n e. NN /\ B < ( vol ` ( A i^i ( -u n [,] n ) ) ) ) ) /\ ( z e. ( -u n [,] n ) /\ ( vol ` ( A i^i ( -u n [,] z ) ) ) = B ) ) -> -u n e. RR )
109 99 adantrr 
 |-  ( ( ( ( ( A e. dom vol /\ B e. ( 0 [,] ( vol ` A ) ) ) /\ B < ( vol ` A ) ) /\ ( n e. NN /\ B < ( vol ` ( A i^i ( -u n [,] n ) ) ) ) ) /\ ( z e. ( -u n [,] n ) /\ ( vol ` ( A i^i ( -u n [,] z ) ) ) = B ) ) -> z e. RR )
110 iccmbl 
 |-  ( ( -u n e. RR /\ z e. RR ) -> ( -u n [,] z ) e. dom vol )
111 108 109 110 syl2anc 
 |-  ( ( ( ( ( A e. dom vol /\ B e. ( 0 [,] ( vol ` A ) ) ) /\ B < ( vol ` A ) ) /\ ( n e. NN /\ B < ( vol ` ( A i^i ( -u n [,] n ) ) ) ) ) /\ ( z e. ( -u n [,] n ) /\ ( vol ` ( A i^i ( -u n [,] z ) ) ) = B ) ) -> ( -u n [,] z ) e. dom vol )
112 inmbl 
 |-  ( ( A e. dom vol /\ ( -u n [,] z ) e. dom vol ) -> ( A i^i ( -u n [,] z ) ) e. dom vol )
113 107 111 112 syl2anc 
 |-  ( ( ( ( ( A e. dom vol /\ B e. ( 0 [,] ( vol ` A ) ) ) /\ B < ( vol ` A ) ) /\ ( n e. NN /\ B < ( vol ` ( A i^i ( -u n [,] n ) ) ) ) ) /\ ( z e. ( -u n [,] n ) /\ ( vol ` ( A i^i ( -u n [,] z ) ) ) = B ) ) -> ( A i^i ( -u n [,] z ) ) e. dom vol )
114 inss1 
 |-  ( A i^i ( -u n [,] z ) ) C_ A
115 114 a1i 
 |-  ( ( ( ( ( A e. dom vol /\ B e. ( 0 [,] ( vol ` A ) ) ) /\ B < ( vol ` A ) ) /\ ( n e. NN /\ B < ( vol ` ( A i^i ( -u n [,] n ) ) ) ) ) /\ ( z e. ( -u n [,] n ) /\ ( vol ` ( A i^i ( -u n [,] z ) ) ) = B ) ) -> ( A i^i ( -u n [,] z ) ) C_ A )
116 simprr 
 |-  ( ( ( ( ( A e. dom vol /\ B e. ( 0 [,] ( vol ` A ) ) ) /\ B < ( vol ` A ) ) /\ ( n e. NN /\ B < ( vol ` ( A i^i ( -u n [,] n ) ) ) ) ) /\ ( z e. ( -u n [,] n ) /\ ( vol ` ( A i^i ( -u n [,] z ) ) ) = B ) ) -> ( vol ` ( A i^i ( -u n [,] z ) ) ) = B )
117 sseq1 
 |-  ( x = ( A i^i ( -u n [,] z ) ) -> ( x C_ A <-> ( A i^i ( -u n [,] z ) ) C_ A ) )
118 fveqeq2 
 |-  ( x = ( A i^i ( -u n [,] z ) ) -> ( ( vol ` x ) = B <-> ( vol ` ( A i^i ( -u n [,] z ) ) ) = B ) )
119 117 118 anbi12d 
 |-  ( x = ( A i^i ( -u n [,] z ) ) -> ( ( x C_ A /\ ( vol ` x ) = B ) <-> ( ( A i^i ( -u n [,] z ) ) C_ A /\ ( vol ` ( A i^i ( -u n [,] z ) ) ) = B ) ) )
120 119 rspcev 
 |-  ( ( ( A i^i ( -u n [,] z ) ) e. dom vol /\ ( ( A i^i ( -u n [,] z ) ) C_ A /\ ( vol ` ( A i^i ( -u n [,] z ) ) ) = B ) ) -> E. x e. dom vol ( x C_ A /\ ( vol ` x ) = B ) )
121 113 115 116 120 syl12anc 
 |-  ( ( ( ( ( A e. dom vol /\ B e. ( 0 [,] ( vol ` A ) ) ) /\ B < ( vol ` A ) ) /\ ( n e. NN /\ B < ( vol ` ( A i^i ( -u n [,] n ) ) ) ) ) /\ ( z e. ( -u n [,] n ) /\ ( vol ` ( A i^i ( -u n [,] z ) ) ) = B ) ) -> E. x e. dom vol ( x C_ A /\ ( vol ` x ) = B ) )
122 121 expr 
 |-  ( ( ( ( ( A e. dom vol /\ B e. ( 0 [,] ( vol ` A ) ) ) /\ B < ( vol ` A ) ) /\ ( n e. NN /\ B < ( vol ` ( A i^i ( -u n [,] n ) ) ) ) ) /\ z e. ( -u n [,] n ) ) -> ( ( vol ` ( A i^i ( -u n [,] z ) ) ) = B -> E. x e. dom vol ( x C_ A /\ ( vol ` x ) = B ) ) )
123 106 122 sylbid 
 |-  ( ( ( ( ( A e. dom vol /\ B e. ( 0 [,] ( vol ` A ) ) ) /\ B < ( vol ` A ) ) /\ ( n e. NN /\ B < ( vol ` ( A i^i ( -u n [,] n ) ) ) ) ) /\ z e. ( -u n [,] n ) ) -> ( ( ( y e. RR |-> ( vol ` ( A i^i ( -u n [,] y ) ) ) ) ` z ) = B -> E. x e. dom vol ( x C_ A /\ ( vol ` x ) = B ) ) )
124 123 rexlimdva 
 |-  ( ( ( ( A e. dom vol /\ B e. ( 0 [,] ( vol ` A ) ) ) /\ B < ( vol ` A ) ) /\ ( n e. NN /\ B < ( vol ` ( A i^i ( -u n [,] n ) ) ) ) ) -> ( E. z e. ( -u n [,] n ) ( ( y e. RR |-> ( vol ` ( A i^i ( -u n [,] y ) ) ) ) ` z ) = B -> E. x e. dom vol ( x C_ A /\ ( vol ` x ) = B ) ) )
125 98 124 mpd 
 |-  ( ( ( ( A e. dom vol /\ B e. ( 0 [,] ( vol ` A ) ) ) /\ B < ( vol ` A ) ) /\ ( n e. NN /\ B < ( vol ` ( A i^i ( -u n [,] n ) ) ) ) ) -> E. x e. dom vol ( x C_ A /\ ( vol ` x ) = B ) )
126 29 125 rexlimddv 
 |-  ( ( ( A e. dom vol /\ B e. ( 0 [,] ( vol ` A ) ) ) /\ B < ( vol ` A ) ) -> E. x e. dom vol ( x C_ A /\ ( vol ` x ) = B ) )
127 simpll 
 |-  ( ( ( A e. dom vol /\ B e. ( 0 [,] ( vol ` A ) ) ) /\ B = ( vol ` A ) ) -> A e. dom vol )
128 ssid 
 |-  A C_ A
129 128 a1i 
 |-  ( ( ( A e. dom vol /\ B e. ( 0 [,] ( vol ` A ) ) ) /\ B = ( vol ` A ) ) -> A C_ A )
130 simpr 
 |-  ( ( ( A e. dom vol /\ B e. ( 0 [,] ( vol ` A ) ) ) /\ B = ( vol ` A ) ) -> B = ( vol ` A ) )
131 130 eqcomd 
 |-  ( ( ( A e. dom vol /\ B e. ( 0 [,] ( vol ` A ) ) ) /\ B = ( vol ` A ) ) -> ( vol ` A ) = B )
132 sseq1 
 |-  ( x = A -> ( x C_ A <-> A C_ A ) )
133 fveqeq2 
 |-  ( x = A -> ( ( vol ` x ) = B <-> ( vol ` A ) = B ) )
134 132 133 anbi12d 
 |-  ( x = A -> ( ( x C_ A /\ ( vol ` x ) = B ) <-> ( A C_ A /\ ( vol ` A ) = B ) ) )
135 134 rspcev 
 |-  ( ( A e. dom vol /\ ( A C_ A /\ ( vol ` A ) = B ) ) -> E. x e. dom vol ( x C_ A /\ ( vol ` x ) = B ) )
136 127 129 131 135 syl12anc 
 |-  ( ( ( A e. dom vol /\ B e. ( 0 [,] ( vol ` A ) ) ) /\ B = ( vol ` A ) ) -> E. x e. dom vol ( x C_ A /\ ( vol ` x ) = B ) )
137 17 simp3d 
 |-  ( ( A e. dom vol /\ B e. ( 0 [,] ( vol ` A ) ) ) -> B <_ ( vol ` A ) )
138 xrleloe 
 |-  ( ( B e. RR* /\ ( vol ` A ) e. RR* ) -> ( B <_ ( vol ` A ) <-> ( B < ( vol ` A ) \/ B = ( vol ` A ) ) ) )
139 6 12 138 syl2anc 
 |-  ( ( A e. dom vol /\ B e. ( 0 [,] ( vol ` A ) ) ) -> ( B <_ ( vol ` A ) <-> ( B < ( vol ` A ) \/ B = ( vol ` A ) ) ) )
140 137 139 mpbid 
 |-  ( ( A e. dom vol /\ B e. ( 0 [,] ( vol ` A ) ) ) -> ( B < ( vol ` A ) \/ B = ( vol ` A ) ) )
141 126 136 140 mpjaodan 
 |-  ( ( A e. dom vol /\ B e. ( 0 [,] ( vol ` A ) ) ) -> E. x e. dom vol ( x C_ A /\ ( vol ` x ) = B ) )