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 sseldi
 |-  ( ( 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 sseldi
 |-  ( 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 ) ) ) ) ) )