Metamath Proof Explorer

Theorem hoidmv1lelem3

Description: The dimensional volume of a 1-dimensional half-open interval is less than or equal the generalized sum of the dimensional volumes of countable half-open intervals that cover it. This is the nonempty, finite generalized sum, sub case in Lemma 114B of Fremlin1 p. 23. (Contributed by Glauco Siliprandi, 21-Nov-2020)

Ref Expression
Hypotheses hoidmv1lelem3.a 
|- ( ph -> A e. RR )
hoidmv1lelem3.b 
|- ( ph -> B e. RR )
hoidmv1lelem3.l 
|- ( ph -> A < B )
hoidmv1lelem3.c 
|- ( ph -> C : NN --> RR )
hoidmv1lelem3.d 
|- ( ph -> D : NN --> RR )
hoidmv1lelem3.x 
|- ( ph -> ( A [,) B ) C_ U_ j e. NN ( ( C ` j ) [,) ( D ` j ) ) )
hoidmv1lelem3.r 
|- ( ph -> ( sum^ ` ( j e. NN |-> ( vol ` ( ( C ` j ) [,) ( D ` j ) ) ) ) ) e. RR )
hoidmv1lelem3.u 
|- U = { z e. ( A [,] B ) | ( z - A ) <_ ( sum^ ` ( j e. NN |-> ( vol ` ( ( C ` j ) [,) if ( ( D ` j ) <_ z , ( D ` j ) , z ) ) ) ) ) }
hoidmv1lelem3.s 
|- S = sup ( U , RR , < )
Assertion hoidmv1lelem3 
|- ( ph -> ( B - A ) <_ ( sum^ ` ( j e. NN |-> ( vol ` ( ( C ` j ) [,) ( D ` j ) ) ) ) ) )

Proof

Step Hyp Ref Expression
1 hoidmv1lelem3.a 
 |-  ( ph -> A e. RR )
2 hoidmv1lelem3.b 
 |-  ( ph -> B e. RR )
3 hoidmv1lelem3.l 
 |-  ( ph -> A < B )
4 hoidmv1lelem3.c 
 |-  ( ph -> C : NN --> RR )
5 hoidmv1lelem3.d 
 |-  ( ph -> D : NN --> RR )
6 hoidmv1lelem3.x 
 |-  ( ph -> ( A [,) B ) C_ U_ j e. NN ( ( C ` j ) [,) ( D ` j ) ) )
7 hoidmv1lelem3.r 
 |-  ( ph -> ( sum^ ` ( j e. NN |-> ( vol ` ( ( C ` j ) [,) ( D ` j ) ) ) ) ) e. RR )
8 hoidmv1lelem3.u 
 |-  U = { z e. ( A [,] B ) | ( z - A ) <_ ( sum^ ` ( j e. NN |-> ( vol ` ( ( C ` j ) [,) if ( ( D ` j ) <_ z , ( D ` j ) , z ) ) ) ) ) }
9 hoidmv1lelem3.s 
 |-  S = sup ( U , RR , < )
10 2 1 resubcld 
 |-  ( ph -> ( B - A ) e. RR )
11 nnex 
 |-  NN e. _V
12 11 a1i 
 |-  ( ph -> NN e. _V )
13 icossicc 
 |-  ( 0 [,) +oo ) C_ ( 0 [,] +oo )
14 0xr 
 |-  0 e. RR*
15 14 a1i 
 |-  ( ( ph /\ j e. NN ) -> 0 e. RR* )
16 pnfxr 
 |-  +oo e. RR*
17 16 a1i 
 |-  ( ( ph /\ j e. NN ) -> +oo e. RR* )
18 4 ffvelrnda 
 |-  ( ( ph /\ j e. NN ) -> ( C ` j ) e. RR )
19 5 ffvelrnda 
 |-  ( ( ph /\ j e. NN ) -> ( D ` j ) e. RR )
20 2 adantr 
 |-  ( ( ph /\ j e. NN ) -> B e. RR )
21 19 20 ifcld 
 |-  ( ( ph /\ j e. NN ) -> if ( ( D ` j ) <_ B , ( D ` j ) , B ) e. RR )
22 volicore 
 |-  ( ( ( C ` j ) e. RR /\ if ( ( D ` j ) <_ B , ( D ` j ) , B ) e. RR ) -> ( vol ` ( ( C ` j ) [,) if ( ( D ` j ) <_ B , ( D ` j ) , B ) ) ) e. RR )
23 18 21 22 syl2anc 
 |-  ( ( ph /\ j e. NN ) -> ( vol ` ( ( C ` j ) [,) if ( ( D ` j ) <_ B , ( D ` j ) , B ) ) ) e. RR )
24 23 rexrd 
 |-  ( ( ph /\ j e. NN ) -> ( vol ` ( ( C ` j ) [,) if ( ( D ` j ) <_ B , ( D ` j ) , B ) ) ) e. RR* )
25 21 rexrd 
 |-  ( ( ph /\ j e. NN ) -> if ( ( D ` j ) <_ B , ( D ` j ) , B ) e. RR* )
26 icombl 
 |-  ( ( ( C ` j ) e. RR /\ if ( ( D ` j ) <_ B , ( D ` j ) , B ) e. RR* ) -> ( ( C ` j ) [,) if ( ( D ` j ) <_ B , ( D ` j ) , B ) ) e. dom vol )
27 18 25 26 syl2anc 
 |-  ( ( ph /\ j e. NN ) -> ( ( C ` j ) [,) if ( ( D ` j ) <_ B , ( D ` j ) , B ) ) e. dom vol )
28 volge0 
 |-  ( ( ( C ` j ) [,) if ( ( D ` j ) <_ B , ( D ` j ) , B ) ) e. dom vol -> 0 <_ ( vol ` ( ( C ` j ) [,) if ( ( D ` j ) <_ B , ( D ` j ) , B ) ) ) )
29 27 28 syl 
 |-  ( ( ph /\ j e. NN ) -> 0 <_ ( vol ` ( ( C ` j ) [,) if ( ( D ` j ) <_ B , ( D ` j ) , B ) ) ) )
30 23 ltpnfd 
 |-  ( ( ph /\ j e. NN ) -> ( vol ` ( ( C ` j ) [,) if ( ( D ` j ) <_ B , ( D ` j ) , B ) ) ) < +oo )
31 15 17 24 29 30 elicod 
 |-  ( ( ph /\ j e. NN ) -> ( vol ` ( ( C ` j ) [,) if ( ( D ` j ) <_ B , ( D ` j ) , B ) ) ) e. ( 0 [,) +oo ) )
32 13 31 sselid 
 |-  ( ( ph /\ j e. NN ) -> ( vol ` ( ( C ` j ) [,) if ( ( D ` j ) <_ B , ( D ` j ) , B ) ) ) e. ( 0 [,] +oo ) )
33 eqid 
 |-  ( j e. NN |-> ( vol ` ( ( C ` j ) [,) if ( ( D ` j ) <_ B , ( D ` j ) , B ) ) ) ) = ( j e. NN |-> ( vol ` ( ( C ` j ) [,) if ( ( D ` j ) <_ B , ( D ` j ) , B ) ) ) )
34 32 33 fmptd 
 |-  ( ph -> ( j e. NN |-> ( vol ` ( ( C ` j ) [,) if ( ( D ` j ) <_ B , ( D ` j ) , B ) ) ) ) : NN --> ( 0 [,] +oo ) )
35 12 34 sge0xrcl 
 |-  ( ph -> ( sum^ ` ( j e. NN |-> ( vol ` ( ( C ` j ) [,) if ( ( D ` j ) <_ B , ( D ` j ) , B ) ) ) ) ) e. RR* )
36 16 a1i 
 |-  ( ph -> +oo e. RR* )
37 7 rexrd 
 |-  ( ph -> ( sum^ ` ( j e. NN |-> ( vol ` ( ( C ` j ) [,) ( D ` j ) ) ) ) ) e. RR* )
38 nfv 
 |-  F/ j ph
39 volf 
 |-  vol : dom vol --> ( 0 [,] +oo )
40 39 a1i 
 |-  ( ( ph /\ j e. NN ) -> vol : dom vol --> ( 0 [,] +oo ) )
41 19 rexrd 
 |-  ( ( ph /\ j e. NN ) -> ( D ` j ) e. RR* )
42 icombl 
 |-  ( ( ( C ` j ) e. RR /\ ( D ` j ) e. RR* ) -> ( ( C ` j ) [,) ( D ` j ) ) e. dom vol )
43 18 41 42 syl2anc 
 |-  ( ( ph /\ j e. NN ) -> ( ( C ` j ) [,) ( D ` j ) ) e. dom vol )
44 40 43 ffvelrnd 
 |-  ( ( ph /\ j e. NN ) -> ( vol ` ( ( C ` j ) [,) ( D ` j ) ) ) e. ( 0 [,] +oo ) )
45 18 rexrd 
 |-  ( ( ph /\ j e. NN ) -> ( C ` j ) e. RR* )
46 18 leidd 
 |-  ( ( ph /\ j e. NN ) -> ( C ` j ) <_ ( C ` j ) )
47 min1 
 |-  ( ( ( D ` j ) e. RR /\ B e. RR ) -> if ( ( D ` j ) <_ B , ( D ` j ) , B ) <_ ( D ` j ) )
48 19 20 47 syl2anc 
 |-  ( ( ph /\ j e. NN ) -> if ( ( D ` j ) <_ B , ( D ` j ) , B ) <_ ( D ` j ) )
49 icossico 
 |-  ( ( ( ( C ` j ) e. RR* /\ ( D ` j ) e. RR* ) /\ ( ( C ` j ) <_ ( C ` j ) /\ if ( ( D ` j ) <_ B , ( D ` j ) , B ) <_ ( D ` j ) ) ) -> ( ( C ` j ) [,) if ( ( D ` j ) <_ B , ( D ` j ) , B ) ) C_ ( ( C ` j ) [,) ( D ` j ) ) )
50 45 41 46 48 49 syl22anc 
 |-  ( ( ph /\ j e. NN ) -> ( ( C ` j ) [,) if ( ( D ` j ) <_ B , ( D ` j ) , B ) ) C_ ( ( C ` j ) [,) ( D ` j ) ) )
51 volss 
 |-  ( ( ( ( C ` j ) [,) if ( ( D ` j ) <_ B , ( D ` j ) , B ) ) e. dom vol /\ ( ( C ` j ) [,) ( D ` j ) ) e. dom vol /\ ( ( C ` j ) [,) if ( ( D ` j ) <_ B , ( D ` j ) , B ) ) C_ ( ( C ` j ) [,) ( D ` j ) ) ) -> ( vol ` ( ( C ` j ) [,) if ( ( D ` j ) <_ B , ( D ` j ) , B ) ) ) <_ ( vol ` ( ( C ` j ) [,) ( D ` j ) ) ) )
52 27 43 50 51 syl3anc 
 |-  ( ( ph /\ j e. NN ) -> ( vol ` ( ( C ` j ) [,) if ( ( D ` j ) <_ B , ( D ` j ) , B ) ) ) <_ ( vol ` ( ( C ` j ) [,) ( D ` j ) ) ) )
53 38 12 32 44 52 sge0lempt 
 |-  ( ph -> ( sum^ ` ( j e. NN |-> ( vol ` ( ( C ` j ) [,) if ( ( D ` j ) <_ B , ( D ` j ) , B ) ) ) ) ) <_ ( sum^ ` ( j e. NN |-> ( vol ` ( ( C ` j ) [,) ( D ` j ) ) ) ) ) )
54 7 ltpnfd 
 |-  ( ph -> ( sum^ ` ( j e. NN |-> ( vol ` ( ( C ` j ) [,) ( D ` j ) ) ) ) ) < +oo )
55 35 37 36 53 54 xrlelttrd 
 |-  ( ph -> ( sum^ ` ( j e. NN |-> ( vol ` ( ( C ` j ) [,) if ( ( D ` j ) <_ B , ( D ` j ) , B ) ) ) ) ) < +oo )
56 35 36 55 xrltned 
 |-  ( ph -> ( sum^ ` ( j e. NN |-> ( vol ` ( ( C ` j ) [,) if ( ( D ` j ) <_ B , ( D ` j ) , B ) ) ) ) ) =/= +oo )
57 56 neneqd 
 |-  ( ph -> -. ( sum^ ` ( j e. NN |-> ( vol ` ( ( C ` j ) [,) if ( ( D ` j ) <_ B , ( D ` j ) , B ) ) ) ) ) = +oo )
58 12 34 sge0repnf 
 |-  ( ph -> ( ( sum^ ` ( j e. NN |-> ( vol ` ( ( C ` j ) [,) if ( ( D ` j ) <_ B , ( D ` j ) , B ) ) ) ) ) e. RR <-> -. ( sum^ ` ( j e. NN |-> ( vol ` ( ( C ` j ) [,) if ( ( D ` j ) <_ B , ( D ` j ) , B ) ) ) ) ) = +oo ) )
59 57 58 mpbird 
 |-  ( ph -> ( sum^ ` ( j e. NN |-> ( vol ` ( ( C ` j ) [,) if ( ( D ` j ) <_ B , ( D ` j ) , B ) ) ) ) ) e. RR )
60 2 rexrd 
 |-  ( ph -> B e. RR* )
61 1 2 iccssred 
 |-  ( ph -> ( A [,] B ) C_ RR )
62 ssrab2 
 |-  { z e. ( A [,] B ) | ( z - A ) <_ ( sum^ ` ( j e. NN |-> ( vol ` ( ( C ` j ) [,) if ( ( D ` j ) <_ z , ( D ` j ) , z ) ) ) ) ) } C_ ( A [,] B )
63 8 62 eqsstri 
 |-  U C_ ( A [,] B )
64 1 2 3 4 5 7 8 9 hoidmv1lelem1 
 |-  ( ph -> ( S e. U /\ A e. U /\ E. x e. RR A. y e. U y <_ x ) )
65 64 simp1d 
 |-  ( ph -> S e. U )
66 63 65 sselid 
 |-  ( ph -> S e. ( A [,] B ) )
67 61 66 sseldd 
 |-  ( ph -> S e. RR )
68 67 rexrd 
 |-  ( ph -> S e. RR* )
69 simpl 
 |-  ( ( ph /\ -. B <_ S ) -> ph )
70 simpr 
 |-  ( ( ph /\ -. B <_ S ) -> -. B <_ S )
71 69 67 syl 
 |-  ( ( ph /\ -. B <_ S ) -> S e. RR )
72 69 2 syl 
 |-  ( ( ph /\ -. B <_ S ) -> B e. RR )
73 71 72 ltnled 
 |-  ( ( ph /\ -. B <_ S ) -> ( S < B <-> -. B <_ S ) )
74 70 73 mpbird 
 |-  ( ( ph /\ -. B <_ S ) -> S < B )
75 6 adantr 
 |-  ( ( ph /\ S < B ) -> ( A [,) B ) C_ U_ j e. NN ( ( C ` j ) [,) ( D ` j ) ) )
76 1 rexrd 
 |-  ( ph -> A e. RR* )
77 76 adantr 
 |-  ( ( ph /\ S < B ) -> A e. RR* )
78 60 adantr 
 |-  ( ( ph /\ S < B ) -> B e. RR* )
79 68 adantr 
 |-  ( ( ph /\ S < B ) -> S e. RR* )
80 63 61 sstrid 
 |-  ( ph -> U C_ RR )
81 65 ne0d 
 |-  ( ph -> U =/= (/) )
82 64 simp3d 
 |-  ( ph -> E. x e. RR A. y e. U y <_ x )
83 64 simp2d 
 |-  ( ph -> A e. U )
84 suprub 
 |-  ( ( ( U C_ RR /\ U =/= (/) /\ E. x e. RR A. y e. U y <_ x ) /\ A e. U ) -> A <_ sup ( U , RR , < ) )
85 80 81 82 83 84 syl31anc 
 |-  ( ph -> A <_ sup ( U , RR , < ) )
86 85 9 breqtrrdi 
 |-  ( ph -> A <_ S )
87 86 adantr 
 |-  ( ( ph /\ S < B ) -> A <_ S )
88 simpr 
 |-  ( ( ph /\ S < B ) -> S < B )
89 77 78 79 87 88 elicod 
 |-  ( ( ph /\ S < B ) -> S e. ( A [,) B ) )
90 75 89 sseldd 
 |-  ( ( ph /\ S < B ) -> S e. U_ j e. NN ( ( C ` j ) [,) ( D ` j ) ) )
91 eliun 
 |-  ( S e. U_ j e. NN ( ( C ` j ) [,) ( D ` j ) ) <-> E. j e. NN S e. ( ( C ` j ) [,) ( D ` j ) ) )
92 90 91 sylib 
 |-  ( ( ph /\ S < B ) -> E. j e. NN S e. ( ( C ` j ) [,) ( D ` j ) ) )
93 1 adantr 
 |-  ( ( ph /\ S < B ) -> A e. RR )
94 93 3ad2ant1 
 |-  ( ( ( ph /\ S < B ) /\ j e. NN /\ S e. ( ( C ` j ) [,) ( D ` j ) ) ) -> A e. RR )
95 2 adantr 
 |-  ( ( ph /\ S < B ) -> B e. RR )
96 95 3ad2ant1 
 |-  ( ( ( ph /\ S < B ) /\ j e. NN /\ S e. ( ( C ` j ) [,) ( D ` j ) ) ) -> B e. RR )
97 4 adantr 
 |-  ( ( ph /\ S < B ) -> C : NN --> RR )
98 97 3ad2ant1 
 |-  ( ( ( ph /\ S < B ) /\ j e. NN /\ S e. ( ( C ` j ) [,) ( D ` j ) ) ) -> C : NN --> RR )
99 5 adantr 
 |-  ( ( ph /\ S < B ) -> D : NN --> RR )
100 99 3ad2ant1 
 |-  ( ( ( ph /\ S < B ) /\ j e. NN /\ S e. ( ( C ` j ) [,) ( D ` j ) ) ) -> D : NN --> RR )
101 fveq2 
 |-  ( i = j -> ( C ` i ) = ( C ` j ) )
102 fveq2 
 |-  ( i = j -> ( D ` i ) = ( D ` j ) )
103 101 102 oveq12d 
 |-  ( i = j -> ( ( C ` i ) [,) ( D ` i ) ) = ( ( C ` j ) [,) ( D ` j ) ) )
104 103 fveq2d 
 |-  ( i = j -> ( vol ` ( ( C ` i ) [,) ( D ` i ) ) ) = ( vol ` ( ( C ` j ) [,) ( D ` j ) ) ) )
105 104 cbvmptv 
 |-  ( i e. NN |-> ( vol ` ( ( C ` i ) [,) ( D ` i ) ) ) ) = ( j e. NN |-> ( vol ` ( ( C ` j ) [,) ( D ` j ) ) ) )
106 105 fveq2i 
 |-  ( sum^ ` ( i e. NN |-> ( vol ` ( ( C ` i ) [,) ( D ` i ) ) ) ) ) = ( sum^ ` ( j e. NN |-> ( vol ` ( ( C ` j ) [,) ( D ` j ) ) ) ) )
107 106 7 eqeltrid 
 |-  ( ph -> ( sum^ ` ( i e. NN |-> ( vol ` ( ( C ` i ) [,) ( D ` i ) ) ) ) ) e. RR )
108 107 adantr 
 |-  ( ( ph /\ S < B ) -> ( sum^ ` ( i e. NN |-> ( vol ` ( ( C ` i ) [,) ( D ` i ) ) ) ) ) e. RR )
109 108 3ad2ant1 
 |-  ( ( ( ph /\ S < B ) /\ j e. NN /\ S e. ( ( C ` j ) [,) ( D ` j ) ) ) -> ( sum^ ` ( i e. NN |-> ( vol ` ( ( C ` i ) [,) ( D ` i ) ) ) ) ) e. RR )
110 102 breq1d 
 |-  ( i = j -> ( ( D ` i ) <_ z <-> ( D ` j ) <_ z ) )
111 110 102 ifbieq1d 
 |-  ( i = j -> if ( ( D ` i ) <_ z , ( D ` i ) , z ) = if ( ( D ` j ) <_ z , ( D ` j ) , z ) )
112 101 111 oveq12d 
 |-  ( i = j -> ( ( C ` i ) [,) if ( ( D ` i ) <_ z , ( D ` i ) , z ) ) = ( ( C ` j ) [,) if ( ( D ` j ) <_ z , ( D ` j ) , z ) ) )
113 112 fveq2d 
 |-  ( i = j -> ( vol ` ( ( C ` i ) [,) if ( ( D ` i ) <_ z , ( D ` i ) , z ) ) ) = ( vol ` ( ( C ` j ) [,) if ( ( D ` j ) <_ z , ( D ` j ) , z ) ) ) )
114 113 cbvmptv 
 |-  ( i e. NN |-> ( vol ` ( ( C ` i ) [,) if ( ( D ` i ) <_ z , ( D ` i ) , z ) ) ) ) = ( j e. NN |-> ( vol ` ( ( C ` j ) [,) if ( ( D ` j ) <_ z , ( D ` j ) , z ) ) ) )
115 114 eqcomi 
 |-  ( j e. NN |-> ( vol ` ( ( C ` j ) [,) if ( ( D ` j ) <_ z , ( D ` j ) , z ) ) ) ) = ( i e. NN |-> ( vol ` ( ( C ` i ) [,) if ( ( D ` i ) <_ z , ( D ` i ) , z ) ) ) )
116 115 fveq2i 
 |-  ( sum^ ` ( j e. NN |-> ( vol ` ( ( C ` j ) [,) if ( ( D ` j ) <_ z , ( D ` j ) , z ) ) ) ) ) = ( sum^ ` ( i e. NN |-> ( vol ` ( ( C ` i ) [,) if ( ( D ` i ) <_ z , ( D ` i ) , z ) ) ) ) )
117 116 breq2i 
 |-  ( ( z - A ) <_ ( sum^ ` ( j e. NN |-> ( vol ` ( ( C ` j ) [,) if ( ( D ` j ) <_ z , ( D ` j ) , z ) ) ) ) ) <-> ( z - A ) <_ ( sum^ ` ( i e. NN |-> ( vol ` ( ( C ` i ) [,) if ( ( D ` i ) <_ z , ( D ` i ) , z ) ) ) ) ) )
118 117 rabbii 
 |-  { z e. ( A [,] B ) | ( z - A ) <_ ( sum^ ` ( j e. NN |-> ( vol ` ( ( C ` j ) [,) if ( ( D ` j ) <_ z , ( D ` j ) , z ) ) ) ) ) } = { z e. ( A [,] B ) | ( z - A ) <_ ( sum^ ` ( i e. NN |-> ( vol ` ( ( C ` i ) [,) if ( ( D ` i ) <_ z , ( D ` i ) , z ) ) ) ) ) }
119 8 118 eqtri 
 |-  U = { z e. ( A [,] B ) | ( z - A ) <_ ( sum^ ` ( i e. NN |-> ( vol ` ( ( C ` i ) [,) if ( ( D ` i ) <_ z , ( D ` i ) , z ) ) ) ) ) }
120 65 adantr 
 |-  ( ( ph /\ S < B ) -> S e. U )
121 120 3ad2ant1 
 |-  ( ( ( ph /\ S < B ) /\ j e. NN /\ S e. ( ( C ` j ) [,) ( D ` j ) ) ) -> S e. U )
122 87 3ad2ant1 
 |-  ( ( ( ph /\ S < B ) /\ j e. NN /\ S e. ( ( C ` j ) [,) ( D ` j ) ) ) -> A <_ S )
123 88 3ad2ant1 
 |-  ( ( ( ph /\ S < B ) /\ j e. NN /\ S e. ( ( C ` j ) [,) ( D ` j ) ) ) -> S < B )
124 simp2 
 |-  ( ( ( ph /\ S < B ) /\ j e. NN /\ S e. ( ( C ` j ) [,) ( D ` j ) ) ) -> j e. NN )
125 simp3 
 |-  ( ( ( ph /\ S < B ) /\ j e. NN /\ S e. ( ( C ` j ) [,) ( D ` j ) ) ) -> S e. ( ( C ` j ) [,) ( D ` j ) ) )
126 eqid 
 |-  if ( ( D ` j ) <_ B , ( D ` j ) , B ) = if ( ( D ` j ) <_ B , ( D ` j ) , B )
127 94 96 98 100 109 119 121 122 123 124 125 126 hoidmv1lelem2 
 |-  ( ( ( ph /\ S < B ) /\ j e. NN /\ S e. ( ( C ` j ) [,) ( D ` j ) ) ) -> E. u e. U S < u )
128 127 3exp 
 |-  ( ( ph /\ S < B ) -> ( j e. NN -> ( S e. ( ( C ` j ) [,) ( D ` j ) ) -> E. u e. U S < u ) ) )
129 128 rexlimdv 
 |-  ( ( ph /\ S < B ) -> ( E. j e. NN S e. ( ( C ` j ) [,) ( D ` j ) ) -> E. u e. U S < u ) )
130 92 129 mpd 
 |-  ( ( ph /\ S < B ) -> E. u e. U S < u )
131 69 74 130 syl2anc 
 |-  ( ( ph /\ -. B <_ S ) -> E. u e. U S < u )
132 61 adantr 
 |-  ( ( ph /\ u e. U ) -> ( A [,] B ) C_ RR )
133 63 132 sstrid 
 |-  ( ( ph /\ u e. U ) -> U C_ RR )
134 81 adantr 
 |-  ( ( ph /\ u e. U ) -> U =/= (/) )
135 1 2 jca 
 |-  ( ph -> ( A e. RR /\ B e. RR ) )
136 135 adantr 
 |-  ( ( ph /\ u e. U ) -> ( A e. RR /\ B e. RR ) )
137 63 a1i 
 |-  ( ( ph /\ u e. U ) -> U C_ ( A [,] B ) )
138 65 adantr 
 |-  ( ( ph /\ u e. U ) -> S e. U )
139 iccsupr 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ U C_ ( A [,] B ) /\ S e. U ) -> ( U C_ RR /\ U =/= (/) /\ E. x e. RR A. y e. U y <_ x ) )
140 136 137 138 139 syl3anc 
 |-  ( ( ph /\ u e. U ) -> ( U C_ RR /\ U =/= (/) /\ E. x e. RR A. y e. U y <_ x ) )
141 140 simp3d 
 |-  ( ( ph /\ u e. U ) -> E. x e. RR A. y e. U y <_ x )
142 simpr 
 |-  ( ( ph /\ u e. U ) -> u e. U )
143 suprub 
 |-  ( ( ( U C_ RR /\ U =/= (/) /\ E. x e. RR A. y e. U y <_ x ) /\ u e. U ) -> u <_ sup ( U , RR , < ) )
144 133 134 141 142 143 syl31anc 
 |-  ( ( ph /\ u e. U ) -> u <_ sup ( U , RR , < ) )
145 144 9 breqtrrdi 
 |-  ( ( ph /\ u e. U ) -> u <_ S )
146 145 ralrimiva 
 |-  ( ph -> A. u e. U u <_ S )
147 63 sseli 
 |-  ( u e. U -> u e. ( A [,] B ) )
148 147 adantl 
 |-  ( ( ph /\ u e. U ) -> u e. ( A [,] B ) )
149 132 148 sseldd 
 |-  ( ( ph /\ u e. U ) -> u e. RR )
150 67 adantr 
 |-  ( ( ph /\ u e. U ) -> S e. RR )
151 149 150 lenltd 
 |-  ( ( ph /\ u e. U ) -> ( u <_ S <-> -. S < u ) )
152 151 ralbidva 
 |-  ( ph -> ( A. u e. U u <_ S <-> A. u e. U -. S < u ) )
153 146 152 mpbid 
 |-  ( ph -> A. u e. U -. S < u )
154 ralnex 
 |-  ( A. u e. U -. S < u <-> -. E. u e. U S < u )
155 153 154 sylib 
 |-  ( ph -> -. E. u e. U S < u )
156 155 adantr 
 |-  ( ( ph /\ -. B <_ S ) -> -. E. u e. U S < u )
157 131 156 condan 
 |-  ( ph -> B <_ S )
158 iccleub 
 |-  ( ( A e. RR* /\ B e. RR* /\ S e. ( A [,] B ) ) -> S <_ B )
159 76 60 66 158 syl3anc 
 |-  ( ph -> S <_ B )
160 60 68 157 159 xrletrid 
 |-  ( ph -> B = S )
161 160 65 eqeltrd 
 |-  ( ph -> B e. U )
162 161 8 eleqtrdi 
 |-  ( ph -> B e. { z e. ( A [,] B ) | ( z - A ) <_ ( sum^ ` ( j e. NN |-> ( vol ` ( ( C ` j ) [,) if ( ( D ` j ) <_ z , ( D ` j ) , z ) ) ) ) ) } )
163 oveq1 
 |-  ( z = B -> ( z - A ) = ( B - A ) )
164 breq2 
 |-  ( z = B -> ( ( D ` j ) <_ z <-> ( D ` j ) <_ B ) )
165 id 
 |-  ( z = B -> z = B )
166 164 165 ifbieq2d 
 |-  ( z = B -> if ( ( D ` j ) <_ z , ( D ` j ) , z ) = if ( ( D ` j ) <_ B , ( D ` j ) , B ) )
167 166 oveq2d 
 |-  ( z = B -> ( ( C ` j ) [,) if ( ( D ` j ) <_ z , ( D ` j ) , z ) ) = ( ( C ` j ) [,) if ( ( D ` j ) <_ B , ( D ` j ) , B ) ) )
168 167 fveq2d 
 |-  ( z = B -> ( vol ` ( ( C ` j ) [,) if ( ( D ` j ) <_ z , ( D ` j ) , z ) ) ) = ( vol ` ( ( C ` j ) [,) if ( ( D ` j ) <_ B , ( D ` j ) , B ) ) ) )
169 168 mpteq2dv 
 |-  ( z = B -> ( j e. NN |-> ( vol ` ( ( C ` j ) [,) if ( ( D ` j ) <_ z , ( D ` j ) , z ) ) ) ) = ( j e. NN |-> ( vol ` ( ( C ` j ) [,) if ( ( D ` j ) <_ B , ( D ` j ) , B ) ) ) ) )
170 169 fveq2d 
 |-  ( z = B -> ( sum^ ` ( j e. NN |-> ( vol ` ( ( C ` j ) [,) if ( ( D ` j ) <_ z , ( D ` j ) , z ) ) ) ) ) = ( sum^ ` ( j e. NN |-> ( vol ` ( ( C ` j ) [,) if ( ( D ` j ) <_ B , ( D ` j ) , B ) ) ) ) ) )
171 163 170 breq12d 
 |-  ( z = B -> ( ( z - A ) <_ ( sum^ ` ( j e. NN |-> ( vol ` ( ( C ` j ) [,) if ( ( D ` j ) <_ z , ( D ` j ) , z ) ) ) ) ) <-> ( B - A ) <_ ( sum^ ` ( j e. NN |-> ( vol ` ( ( C ` j ) [,) if ( ( D ` j ) <_ B , ( D ` j ) , B ) ) ) ) ) ) )
172 171 elrab 
 |-  ( B e. { z e. ( A [,] B ) | ( z - A ) <_ ( sum^ ` ( j e. NN |-> ( vol ` ( ( C ` j ) [,) if ( ( D ` j ) <_ z , ( D ` j ) , z ) ) ) ) ) } <-> ( B e. ( A [,] B ) /\ ( B - A ) <_ ( sum^ ` ( j e. NN |-> ( vol ` ( ( C ` j ) [,) if ( ( D ` j ) <_ B , ( D ` j ) , B ) ) ) ) ) ) )
173 162 172 sylib 
 |-  ( ph -> ( B e. ( A [,] B ) /\ ( B - A ) <_ ( sum^ ` ( j e. NN |-> ( vol ` ( ( C ` j ) [,) if ( ( D ` j ) <_ B , ( D ` j ) , B ) ) ) ) ) ) )
174 173 simprd 
 |-  ( ph -> ( B - A ) <_ ( sum^ ` ( j e. NN |-> ( vol ` ( ( C ` j ) [,) if ( ( D ` j ) <_ B , ( D ` j ) , B ) ) ) ) ) )
175 10 59 7 174 53 letrd 
 |-  ( ph -> ( B - A ) <_ ( sum^ ` ( j e. NN |-> ( vol ` ( ( C ` j ) [,) ( D ` j ) ) ) ) ) )