Metamath Proof Explorer

Theorem hoidmv1lelem1

Description: The supremum of U belongs to U . This is the last part of step (a) and the whole step (b) in the proof of Lemma 114B of Fremlin1 p. 23. (Contributed by Glauco Siliprandi, 21-Nov-2020)

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

Proof

Step Hyp Ref Expression
1 hoidmv1lelem1.a 
 |-  ( ph -> A e. RR )
2 hoidmv1lelem1.b 
 |-  ( ph -> B e. RR )
3 hoidmv1lelem1.l 
 |-  ( ph -> A < B )
4 hoidmv1lelem1.c 
 |-  ( ph -> C : NN --> RR )
5 hoidmv1lelem1.d 
 |-  ( ph -> D : NN --> RR )
6 hoidmv1lelem1.r 
 |-  ( ph -> ( sum^ ` ( j e. NN |-> ( vol ` ( ( C ` j ) [,) ( D ` j ) ) ) ) ) e. RR )
7 hoidmv1lelem1.u 
 |-  U = { z e. ( A [,] B ) | ( z - A ) <_ ( sum^ ` ( j e. NN |-> ( vol ` ( ( C ` j ) [,) if ( ( D ` j ) <_ z , ( D ` j ) , z ) ) ) ) ) }
8 hoidmv1lelem1.s 
 |-  S = sup ( U , RR , < )
9 ssrab2 
 |-  { z e. ( A [,] B ) | ( z - A ) <_ ( sum^ ` ( j e. NN |-> ( vol ` ( ( C ` j ) [,) if ( ( D ` j ) <_ z , ( D ` j ) , z ) ) ) ) ) } C_ ( A [,] B )
10 7 9 eqsstri 
 |-  U C_ ( A [,] B )
11 10 a1i 
 |-  ( ph -> U C_ ( A [,] B ) )
12 1 rexrd 
 |-  ( ph -> A e. RR* )
13 2 rexrd 
 |-  ( ph -> B e. RR* )
14 1 2 3 ltled 
 |-  ( ph -> A <_ B )
15 lbicc2 
 |-  ( ( A e. RR* /\ B e. RR* /\ A <_ B ) -> A e. ( A [,] B ) )
16 12 13 14 15 syl3anc 
 |-  ( ph -> A e. ( A [,] B ) )
17 1 recnd 
 |-  ( ph -> A e. CC )
18 17 subidd 
 |-  ( ph -> ( A - A ) = 0 )
19 nfv 
 |-  F/ j ph
20 nnex 
 |-  NN e. _V
21 20 a1i 
 |-  ( ph -> NN e. _V )
22 volf 
 |-  vol : dom vol --> ( 0 [,] +oo )
23 22 a1i 
 |-  ( ( ph /\ j e. NN ) -> vol : dom vol --> ( 0 [,] +oo ) )
24 4 ffvelrnda 
 |-  ( ( ph /\ j e. NN ) -> ( C ` j ) e. RR )
25 5 ffvelrnda 
 |-  ( ( ph /\ j e. NN ) -> ( D ` j ) e. RR )
26 1 adantr 
 |-  ( ( ph /\ j e. NN ) -> A e. RR )
27 25 26 ifcld 
 |-  ( ( ph /\ j e. NN ) -> if ( ( D ` j ) <_ A , ( D ` j ) , A ) e. RR )
28 27 rexrd 
 |-  ( ( ph /\ j e. NN ) -> if ( ( D ` j ) <_ A , ( D ` j ) , A ) e. RR* )
29 icombl 
 |-  ( ( ( C ` j ) e. RR /\ if ( ( D ` j ) <_ A , ( D ` j ) , A ) e. RR* ) -> ( ( C ` j ) [,) if ( ( D ` j ) <_ A , ( D ` j ) , A ) ) e. dom vol )
30 24 28 29 syl2anc 
 |-  ( ( ph /\ j e. NN ) -> ( ( C ` j ) [,) if ( ( D ` j ) <_ A , ( D ` j ) , A ) ) e. dom vol )
31 23 30 ffvelrnd 
 |-  ( ( ph /\ j e. NN ) -> ( vol ` ( ( C ` j ) [,) if ( ( D ` j ) <_ A , ( D ` j ) , A ) ) ) e. ( 0 [,] +oo ) )
32 19 21 31 sge0ge0mpt 
 |-  ( ph -> 0 <_ ( sum^ ` ( j e. NN |-> ( vol ` ( ( C ` j ) [,) if ( ( D ` j ) <_ A , ( D ` j ) , A ) ) ) ) ) )
33 18 32 eqbrtrd 
 |-  ( ph -> ( A - A ) <_ ( sum^ ` ( j e. NN |-> ( vol ` ( ( C ` j ) [,) if ( ( D ` j ) <_ A , ( D ` j ) , A ) ) ) ) ) )
34 16 33 jca 
 |-  ( ph -> ( A e. ( A [,] B ) /\ ( A - A ) <_ ( sum^ ` ( j e. NN |-> ( vol ` ( ( C ` j ) [,) if ( ( D ` j ) <_ A , ( D ` j ) , A ) ) ) ) ) ) )
35 oveq1 
 |-  ( z = A -> ( z - A ) = ( A - A ) )
36 breq2 
 |-  ( z = A -> ( ( D ` j ) <_ z <-> ( D ` j ) <_ A ) )
37 id 
 |-  ( z = A -> z = A )
38 36 37 ifbieq2d 
 |-  ( z = A -> if ( ( D ` j ) <_ z , ( D ` j ) , z ) = if ( ( D ` j ) <_ A , ( D ` j ) , A ) )
39 38 oveq2d 
 |-  ( z = A -> ( ( C ` j ) [,) if ( ( D ` j ) <_ z , ( D ` j ) , z ) ) = ( ( C ` j ) [,) if ( ( D ` j ) <_ A , ( D ` j ) , A ) ) )
40 39 fveq2d 
 |-  ( z = A -> ( vol ` ( ( C ` j ) [,) if ( ( D ` j ) <_ z , ( D ` j ) , z ) ) ) = ( vol ` ( ( C ` j ) [,) if ( ( D ` j ) <_ A , ( D ` j ) , A ) ) ) )
41 40 mpteq2dv 
 |-  ( z = A -> ( j e. NN |-> ( vol ` ( ( C ` j ) [,) if ( ( D ` j ) <_ z , ( D ` j ) , z ) ) ) ) = ( j e. NN |-> ( vol ` ( ( C ` j ) [,) if ( ( D ` j ) <_ A , ( D ` j ) , A ) ) ) ) )
42 41 fveq2d 
 |-  ( z = A -> ( sum^ ` ( j e. NN |-> ( vol ` ( ( C ` j ) [,) if ( ( D ` j ) <_ z , ( D ` j ) , z ) ) ) ) ) = ( sum^ ` ( j e. NN |-> ( vol ` ( ( C ` j ) [,) if ( ( D ` j ) <_ A , ( D ` j ) , A ) ) ) ) ) )
43 35 42 breq12d 
 |-  ( z = A -> ( ( z - A ) <_ ( sum^ ` ( j e. NN |-> ( vol ` ( ( C ` j ) [,) if ( ( D ` j ) <_ z , ( D ` j ) , z ) ) ) ) ) <-> ( A - A ) <_ ( sum^ ` ( j e. NN |-> ( vol ` ( ( C ` j ) [,) if ( ( D ` j ) <_ A , ( D ` j ) , A ) ) ) ) ) ) )
44 43 elrab 
 |-  ( A e. { z e. ( A [,] B ) | ( z - A ) <_ ( sum^ ` ( j e. NN |-> ( vol ` ( ( C ` j ) [,) if ( ( D ` j ) <_ z , ( D ` j ) , z ) ) ) ) ) } <-> ( A e. ( A [,] B ) /\ ( A - A ) <_ ( sum^ ` ( j e. NN |-> ( vol ` ( ( C ` j ) [,) if ( ( D ` j ) <_ A , ( D ` j ) , A ) ) ) ) ) ) )
45 34 44 sylibr 
 |-  ( ph -> A e. { z e. ( A [,] B ) | ( z - A ) <_ ( sum^ ` ( j e. NN |-> ( vol ` ( ( C ` j ) [,) if ( ( D ` j ) <_ z , ( D ` j ) , z ) ) ) ) ) } )
46 45 7 eleqtrrdi 
 |-  ( ph -> A e. U )
47 46 ne0d 
 |-  ( ph -> U =/= (/) )
48 1 2 11 47 supicc 
 |-  ( ph -> sup ( U , RR , < ) e. ( A [,] B ) )
49 8 48 eqeltrid 
 |-  ( ph -> S e. ( A [,] B ) )
50 8 a1i 
 |-  ( ph -> S = sup ( U , RR , < ) )
51 nfv 
 |-  F/ z ph
52 1 2 iccssred 
 |-  ( ph -> ( A [,] B ) C_ RR )
53 11 52 sstrd 
 |-  ( ph -> U C_ RR )
54 53 sselda 
 |-  ( ( ph /\ z e. U ) -> z e. RR )
55 nfv 
 |-  F/ j ( ph /\ z e. U )
56 20 a1i 
 |-  ( ( ph /\ z e. U ) -> NN e. _V )
57 22 a1i 
 |-  ( ( ( ph /\ z e. U ) /\ j e. NN ) -> vol : dom vol --> ( 0 [,] +oo ) )
58 24 adantlr 
 |-  ( ( ( ph /\ z e. U ) /\ j e. NN ) -> ( C ` j ) e. RR )
59 25 adantlr 
 |-  ( ( ( ph /\ z e. U ) /\ j e. NN ) -> ( D ` j ) e. RR )
60 54 adantr 
 |-  ( ( ( ph /\ z e. U ) /\ j e. NN ) -> z e. RR )
61 59 60 ifcld 
 |-  ( ( ( ph /\ z e. U ) /\ j e. NN ) -> if ( ( D ` j ) <_ z , ( D ` j ) , z ) e. RR )
62 61 rexrd 
 |-  ( ( ( ph /\ z e. U ) /\ j e. NN ) -> if ( ( D ` j ) <_ z , ( D ` j ) , z ) e. RR* )
63 icombl 
 |-  ( ( ( C ` j ) e. RR /\ if ( ( D ` j ) <_ z , ( D ` j ) , z ) e. RR* ) -> ( ( C ` j ) [,) if ( ( D ` j ) <_ z , ( D ` j ) , z ) ) e. dom vol )
64 58 62 63 syl2anc 
 |-  ( ( ( ph /\ z e. U ) /\ j e. NN ) -> ( ( C ` j ) [,) if ( ( D ` j ) <_ z , ( D ` j ) , z ) ) e. dom vol )
65 57 64 ffvelrnd 
 |-  ( ( ( ph /\ z e. U ) /\ j e. NN ) -> ( vol ` ( ( C ` j ) [,) if ( ( D ` j ) <_ z , ( D ` j ) , z ) ) ) e. ( 0 [,] +oo ) )
66 55 56 65 sge0xrclmpt 
 |-  ( ( ph /\ z e. U ) -> ( sum^ ` ( j e. NN |-> ( vol ` ( ( C ` j ) [,) if ( ( D ` j ) <_ z , ( D ` j ) , z ) ) ) ) ) e. RR* )
67 pnfxr 
 |-  +oo e. RR*
68 67 a1i 
 |-  ( ( ph /\ z e. U ) -> +oo e. RR* )
69 6 rexrd 
 |-  ( ph -> ( sum^ ` ( j e. NN |-> ( vol ` ( ( C ` j ) [,) ( D ` j ) ) ) ) ) e. RR* )
70 69 adantr 
 |-  ( ( ph /\ z e. U ) -> ( sum^ ` ( j e. NN |-> ( vol ` ( ( C ` j ) [,) ( D ` j ) ) ) ) ) e. RR* )
71 25 rexrd 
 |-  ( ( ph /\ j e. NN ) -> ( D ` j ) e. RR* )
72 icombl 
 |-  ( ( ( C ` j ) e. RR /\ ( D ` j ) e. RR* ) -> ( ( C ` j ) [,) ( D ` j ) ) e. dom vol )
73 24 71 72 syl2anc 
 |-  ( ( ph /\ j e. NN ) -> ( ( C ` j ) [,) ( D ` j ) ) e. dom vol )
74 23 73 ffvelrnd 
 |-  ( ( ph /\ j e. NN ) -> ( vol ` ( ( C ` j ) [,) ( D ` j ) ) ) e. ( 0 [,] +oo ) )
75 74 adantlr 
 |-  ( ( ( ph /\ z e. U ) /\ j e. NN ) -> ( vol ` ( ( C ` j ) [,) ( D ` j ) ) ) e. ( 0 [,] +oo ) )
76 73 adantlr 
 |-  ( ( ( ph /\ z e. U ) /\ j e. NN ) -> ( ( C ` j ) [,) ( D ` j ) ) e. dom vol )
77 24 rexrd 
 |-  ( ( ph /\ j e. NN ) -> ( C ` j ) e. RR* )
78 77 adantlr 
 |-  ( ( ( ph /\ z e. U ) /\ j e. NN ) -> ( C ` j ) e. RR* )
79 71 adantlr 
 |-  ( ( ( ph /\ z e. U ) /\ j e. NN ) -> ( D ` j ) e. RR* )
80 24 leidd 
 |-  ( ( ph /\ j e. NN ) -> ( C ` j ) <_ ( C ` j ) )
81 80 adantlr 
 |-  ( ( ( ph /\ z e. U ) /\ j e. NN ) -> ( C ` j ) <_ ( C ` j ) )
82 min1 
 |-  ( ( ( D ` j ) e. RR /\ z e. RR ) -> if ( ( D ` j ) <_ z , ( D ` j ) , z ) <_ ( D ` j ) )
83 59 60 82 syl2anc 
 |-  ( ( ( ph /\ z e. U ) /\ j e. NN ) -> if ( ( D ` j ) <_ z , ( D ` j ) , z ) <_ ( D ` j ) )
84 icossico 
 |-  ( ( ( ( C ` j ) e. RR* /\ ( D ` j ) e. RR* ) /\ ( ( C ` j ) <_ ( C ` j ) /\ if ( ( D ` j ) <_ z , ( D ` j ) , z ) <_ ( D ` j ) ) ) -> ( ( C ` j ) [,) if ( ( D ` j ) <_ z , ( D ` j ) , z ) ) C_ ( ( C ` j ) [,) ( D ` j ) ) )
85 78 79 81 83 84 syl22anc 
 |-  ( ( ( ph /\ z e. U ) /\ j e. NN ) -> ( ( C ` j ) [,) if ( ( D ` j ) <_ z , ( D ` j ) , z ) ) C_ ( ( C ` j ) [,) ( D ` j ) ) )
86 volss 
 |-  ( ( ( ( C ` j ) [,) if ( ( D ` j ) <_ z , ( D ` j ) , z ) ) e. dom vol /\ ( ( C ` j ) [,) ( D ` j ) ) e. dom vol /\ ( ( C ` j ) [,) if ( ( D ` j ) <_ z , ( D ` j ) , z ) ) C_ ( ( C ` j ) [,) ( D ` j ) ) ) -> ( vol ` ( ( C ` j ) [,) if ( ( D ` j ) <_ z , ( D ` j ) , z ) ) ) <_ ( vol ` ( ( C ` j ) [,) ( D ` j ) ) ) )
87 64 76 85 86 syl3anc 
 |-  ( ( ( ph /\ z e. U ) /\ j e. NN ) -> ( vol ` ( ( C ` j ) [,) if ( ( D ` j ) <_ z , ( D ` j ) , z ) ) ) <_ ( vol ` ( ( C ` j ) [,) ( D ` j ) ) ) )
88 55 56 65 75 87 sge0lempt 
 |-  ( ( ph /\ z e. U ) -> ( sum^ ` ( j e. NN |-> ( vol ` ( ( C ` j ) [,) if ( ( D ` j ) <_ z , ( D ` j ) , z ) ) ) ) ) <_ ( sum^ ` ( j e. NN |-> ( vol ` ( ( C ` j ) [,) ( D ` j ) ) ) ) ) )
89 6 ltpnfd 
 |-  ( ph -> ( sum^ ` ( j e. NN |-> ( vol ` ( ( C ` j ) [,) ( D ` j ) ) ) ) ) < +oo )
90 89 adantr 
 |-  ( ( ph /\ z e. U ) -> ( sum^ ` ( j e. NN |-> ( vol ` ( ( C ` j ) [,) ( D ` j ) ) ) ) ) < +oo )
91 66 70 68 88 90 xrlelttrd 
 |-  ( ( ph /\ z e. U ) -> ( sum^ ` ( j e. NN |-> ( vol ` ( ( C ` j ) [,) if ( ( D ` j ) <_ z , ( D ` j ) , z ) ) ) ) ) < +oo )
92 66 68 91 xrltned 
 |-  ( ( ph /\ z e. U ) -> ( sum^ ` ( j e. NN |-> ( vol ` ( ( C ` j ) [,) if ( ( D ` j ) <_ z , ( D ` j ) , z ) ) ) ) ) =/= +oo )
93 92 neneqd 
 |-  ( ( ph /\ z e. U ) -> -. ( sum^ ` ( j e. NN |-> ( vol ` ( ( C ` j ) [,) if ( ( D ` j ) <_ z , ( D ` j ) , z ) ) ) ) ) = +oo )
94 eqid 
 |-  ( j e. NN |-> ( vol ` ( ( C ` j ) [,) if ( ( D ` j ) <_ z , ( D ` j ) , z ) ) ) ) = ( j e. NN |-> ( vol ` ( ( C ` j ) [,) if ( ( D ` j ) <_ z , ( D ` j ) , z ) ) ) )
95 65 94 fmptd 
 |-  ( ( ph /\ z e. U ) -> ( j e. NN |-> ( vol ` ( ( C ` j ) [,) if ( ( D ` j ) <_ z , ( D ` j ) , z ) ) ) ) : NN --> ( 0 [,] +oo ) )
96 56 95 sge0repnf 
 |-  ( ( ph /\ z e. U ) -> ( ( sum^ ` ( j e. NN |-> ( vol ` ( ( C ` j ) [,) if ( ( D ` j ) <_ z , ( D ` j ) , z ) ) ) ) ) e. RR <-> -. ( sum^ ` ( j e. NN |-> ( vol ` ( ( C ` j ) [,) if ( ( D ` j ) <_ z , ( D ` j ) , z ) ) ) ) ) = +oo ) )
97 93 96 mpbird 
 |-  ( ( ph /\ z e. U ) -> ( sum^ ` ( j e. NN |-> ( vol ` ( ( C ` j ) [,) if ( ( D ` j ) <_ z , ( D ` j ) , z ) ) ) ) ) e. RR )
98 1 adantr 
 |-  ( ( ph /\ z e. U ) -> A e. RR )
99 97 98 readdcld 
 |-  ( ( ph /\ z e. U ) -> ( ( sum^ ` ( j e. NN |-> ( vol ` ( ( C ` j ) [,) if ( ( D ` j ) <_ z , ( D ` j ) , z ) ) ) ) ) + A ) e. RR )
100 52 49 sseldd 
 |-  ( ph -> S e. RR )
101 100 adantr 
 |-  ( ( ph /\ j e. NN ) -> S e. RR )
102 25 101 ifcld 
 |-  ( ( ph /\ j e. NN ) -> if ( ( D ` j ) <_ S , ( D ` j ) , S ) e. RR )
103 102 rexrd 
 |-  ( ( ph /\ j e. NN ) -> if ( ( D ` j ) <_ S , ( D ` j ) , S ) e. RR* )
104 icombl 
 |-  ( ( ( C ` j ) e. RR /\ if ( ( D ` j ) <_ S , ( D ` j ) , S ) e. RR* ) -> ( ( C ` j ) [,) if ( ( D ` j ) <_ S , ( D ` j ) , S ) ) e. dom vol )
105 24 103 104 syl2anc 
 |-  ( ( ph /\ j e. NN ) -> ( ( C ` j ) [,) if ( ( D ` j ) <_ S , ( D ` j ) , S ) ) e. dom vol )
106 23 105 ffvelrnd 
 |-  ( ( ph /\ j e. NN ) -> ( vol ` ( ( C ` j ) [,) if ( ( D ` j ) <_ S , ( D ` j ) , S ) ) ) e. ( 0 [,] +oo ) )
107 19 21 106 sge0xrclmpt 
 |-  ( ph -> ( sum^ ` ( j e. NN |-> ( vol ` ( ( C ` j ) [,) if ( ( D ` j ) <_ S , ( D ` j ) , S ) ) ) ) ) e. RR* )
108 67 a1i 
 |-  ( ph -> +oo e. RR* )
109 min1 
 |-  ( ( ( D ` j ) e. RR /\ S e. RR ) -> if ( ( D ` j ) <_ S , ( D ` j ) , S ) <_ ( D ` j ) )
110 25 101 109 syl2anc 
 |-  ( ( ph /\ j e. NN ) -> if ( ( D ` j ) <_ S , ( D ` j ) , S ) <_ ( D ` j ) )
111 icossico 
 |-  ( ( ( ( C ` j ) e. RR* /\ ( D ` j ) e. RR* ) /\ ( ( C ` j ) <_ ( C ` j ) /\ if ( ( D ` j ) <_ S , ( D ` j ) , S ) <_ ( D ` j ) ) ) -> ( ( C ` j ) [,) if ( ( D ` j ) <_ S , ( D ` j ) , S ) ) C_ ( ( C ` j ) [,) ( D ` j ) ) )
112 77 71 80 110 111 syl22anc 
 |-  ( ( ph /\ j e. NN ) -> ( ( C ` j ) [,) if ( ( D ` j ) <_ S , ( D ` j ) , S ) ) C_ ( ( C ` j ) [,) ( D ` j ) ) )
113 volss 
 |-  ( ( ( ( C ` j ) [,) if ( ( D ` j ) <_ S , ( D ` j ) , S ) ) e. dom vol /\ ( ( C ` j ) [,) ( D ` j ) ) e. dom vol /\ ( ( C ` j ) [,) if ( ( D ` j ) <_ S , ( D ` j ) , S ) ) C_ ( ( C ` j ) [,) ( D ` j ) ) ) -> ( vol ` ( ( C ` j ) [,) if ( ( D ` j ) <_ S , ( D ` j ) , S ) ) ) <_ ( vol ` ( ( C ` j ) [,) ( D ` j ) ) ) )
114 105 73 112 113 syl3anc 
 |-  ( ( ph /\ j e. NN ) -> ( vol ` ( ( C ` j ) [,) if ( ( D ` j ) <_ S , ( D ` j ) , S ) ) ) <_ ( vol ` ( ( C ` j ) [,) ( D ` j ) ) ) )
115 19 21 106 74 114 sge0lempt 
 |-  ( ph -> ( sum^ ` ( j e. NN |-> ( vol ` ( ( C ` j ) [,) if ( ( D ` j ) <_ S , ( D ` j ) , S ) ) ) ) ) <_ ( sum^ ` ( j e. NN |-> ( vol ` ( ( C ` j ) [,) ( D ` j ) ) ) ) ) )
116 107 69 108 115 89 xrlelttrd 
 |-  ( ph -> ( sum^ ` ( j e. NN |-> ( vol ` ( ( C ` j ) [,) if ( ( D ` j ) <_ S , ( D ` j ) , S ) ) ) ) ) < +oo )
117 107 108 116 xrltned 
 |-  ( ph -> ( sum^ ` ( j e. NN |-> ( vol ` ( ( C ` j ) [,) if ( ( D ` j ) <_ S , ( D ` j ) , S ) ) ) ) ) =/= +oo )
118 117 neneqd 
 |-  ( ph -> -. ( sum^ ` ( j e. NN |-> ( vol ` ( ( C ` j ) [,) if ( ( D ` j ) <_ S , ( D ` j ) , S ) ) ) ) ) = +oo )
119 eqid 
 |-  ( j e. NN |-> ( vol ` ( ( C ` j ) [,) if ( ( D ` j ) <_ S , ( D ` j ) , S ) ) ) ) = ( j e. NN |-> ( vol ` ( ( C ` j ) [,) if ( ( D ` j ) <_ S , ( D ` j ) , S ) ) ) )
120 106 119 fmptd 
 |-  ( ph -> ( j e. NN |-> ( vol ` ( ( C ` j ) [,) if ( ( D ` j ) <_ S , ( D ` j ) , S ) ) ) ) : NN --> ( 0 [,] +oo ) )
121 21 120 sge0repnf 
 |-  ( ph -> ( ( sum^ ` ( j e. NN |-> ( vol ` ( ( C ` j ) [,) if ( ( D ` j ) <_ S , ( D ` j ) , S ) ) ) ) ) e. RR <-> -. ( sum^ ` ( j e. NN |-> ( vol ` ( ( C ` j ) [,) if ( ( D ` j ) <_ S , ( D ` j ) , S ) ) ) ) ) = +oo ) )
122 118 121 mpbird 
 |-  ( ph -> ( sum^ ` ( j e. NN |-> ( vol ` ( ( C ` j ) [,) if ( ( D ` j ) <_ S , ( D ` j ) , S ) ) ) ) ) e. RR )
123 122 1 readdcld 
 |-  ( ph -> ( ( sum^ ` ( j e. NN |-> ( vol ` ( ( C ` j ) [,) if ( ( D ` j ) <_ S , ( D ` j ) , S ) ) ) ) ) + A ) e. RR )
124 123 adantr 
 |-  ( ( ph /\ z e. U ) -> ( ( sum^ ` ( j e. NN |-> ( vol ` ( ( C ` j ) [,) if ( ( D ` j ) <_ S , ( D ` j ) , S ) ) ) ) ) + A ) e. RR )
125 7 eleq2i 
 |-  ( z e. U <-> z e. { z e. ( A [,] B ) | ( z - A ) <_ ( sum^ ` ( j e. NN |-> ( vol ` ( ( C ` j ) [,) if ( ( D ` j ) <_ z , ( D ` j ) , z ) ) ) ) ) } )
126 125 biimpi 
 |-  ( z e. U -> z e. { z e. ( A [,] B ) | ( z - A ) <_ ( sum^ ` ( j e. NN |-> ( vol ` ( ( C ` j ) [,) if ( ( D ` j ) <_ z , ( D ` j ) , z ) ) ) ) ) } )
127 126 adantl 
 |-  ( ( ph /\ z e. U ) -> z e. { z e. ( A [,] B ) | ( z - A ) <_ ( sum^ ` ( j e. NN |-> ( vol ` ( ( C ` j ) [,) if ( ( D ` j ) <_ z , ( D ` j ) , z ) ) ) ) ) } )
128 rabid 
 |-  ( z e. { 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^ ` ( j e. NN |-> ( vol ` ( ( C ` j ) [,) if ( ( D ` j ) <_ z , ( D ` j ) , z ) ) ) ) ) ) )
129 127 128 sylib 
 |-  ( ( ph /\ z e. U ) -> ( z e. ( A [,] B ) /\ ( z - A ) <_ ( sum^ ` ( j e. NN |-> ( vol ` ( ( C ` j ) [,) if ( ( D ` j ) <_ z , ( D ` j ) , z ) ) ) ) ) ) )
130 129 simprd 
 |-  ( ( ph /\ z e. U ) -> ( z - A ) <_ ( sum^ ` ( j e. NN |-> ( vol ` ( ( C ` j ) [,) if ( ( D ` j ) <_ z , ( D ` j ) , z ) ) ) ) ) )
131 54 98 97 lesubaddd 
 |-  ( ( ph /\ z e. U ) -> ( ( z - A ) <_ ( sum^ ` ( j e. NN |-> ( vol ` ( ( C ` j ) [,) if ( ( D ` j ) <_ z , ( D ` j ) , z ) ) ) ) ) <-> z <_ ( ( sum^ ` ( j e. NN |-> ( vol ` ( ( C ` j ) [,) if ( ( D ` j ) <_ z , ( D ` j ) , z ) ) ) ) ) + A ) ) )
132 130 131 mpbid 
 |-  ( ( ph /\ z e. U ) -> z <_ ( ( sum^ ` ( j e. NN |-> ( vol ` ( ( C ` j ) [,) if ( ( D ` j ) <_ z , ( D ` j ) , z ) ) ) ) ) + A ) )
133 122 adantr 
 |-  ( ( ph /\ z e. U ) -> ( sum^ ` ( j e. NN |-> ( vol ` ( ( C ` j ) [,) if ( ( D ` j ) <_ S , ( D ` j ) , S ) ) ) ) ) e. RR )
134 106 adantlr 
 |-  ( ( ( ph /\ z e. U ) /\ j e. NN ) -> ( vol ` ( ( C ` j ) [,) if ( ( D ` j ) <_ S , ( D ` j ) , S ) ) ) e. ( 0 [,] +oo ) )
135 105 adantlr 
 |-  ( ( ( ph /\ z e. U ) /\ j e. NN ) -> ( ( C ` j ) [,) if ( ( D ` j ) <_ S , ( D ` j ) , S ) ) e. dom vol )
136 103 adantlr 
 |-  ( ( ( ph /\ z e. U ) /\ j e. NN ) -> if ( ( D ` j ) <_ S , ( D ` j ) , S ) e. RR* )
137 61 adantr 
 |-  ( ( ( ( ph /\ z e. U ) /\ j e. NN ) /\ ( D ` j ) <_ z ) -> if ( ( D ` j ) <_ z , ( D ` j ) , z ) e. RR )
138 eqidd 
 |-  ( ( ( ( ph /\ z e. U ) /\ j e. NN ) /\ ( D ` j ) <_ z ) -> ( D ` j ) = ( D ` j ) )
139 iftrue 
 |-  ( ( D ` j ) <_ z -> if ( ( D ` j ) <_ z , ( D ` j ) , z ) = ( D ` j ) )
140 139 adantl 
 |-  ( ( ( ( ph /\ z e. U ) /\ j e. NN ) /\ ( D ` j ) <_ z ) -> if ( ( D ` j ) <_ z , ( D ` j ) , z ) = ( D ` j ) )
141 59 adantr 
 |-  ( ( ( ( ph /\ z e. U ) /\ j e. NN ) /\ ( D ` j ) <_ z ) -> ( D ` j ) e. RR )
142 60 adantr 
 |-  ( ( ( ( ph /\ z e. U ) /\ j e. NN ) /\ ( D ` j ) <_ z ) -> z e. RR )
143 100 ad3antrrr 
 |-  ( ( ( ( ph /\ z e. U ) /\ j e. NN ) /\ ( D ` j ) <_ z ) -> S e. RR )
144 simpr 
 |-  ( ( ( ( ph /\ z e. U ) /\ j e. NN ) /\ ( D ` j ) <_ z ) -> ( D ` j ) <_ z )
145 53 adantr 
 |-  ( ( ph /\ z e. U ) -> U C_ RR )
146 47 adantr 
 |-  ( ( ph /\ z e. U ) -> U =/= (/) )
147 1 2 jca 
 |-  ( ph -> ( A e. RR /\ B e. RR ) )
148 iccsupr 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ U C_ ( A [,] B ) /\ A e. U ) -> ( U C_ RR /\ U =/= (/) /\ E. x e. RR A. y e. U y <_ x ) )
149 147 11 46 148 syl3anc 
 |-  ( ph -> ( U C_ RR /\ U =/= (/) /\ E. x e. RR A. y e. U y <_ x ) )
150 149 simp3d 
 |-  ( ph -> E. x e. RR A. y e. U y <_ x )
151 150 adantr 
 |-  ( ( ph /\ z e. U ) -> E. x e. RR A. y e. U y <_ x )
152 127 125 sylibr 
 |-  ( ( ph /\ z e. U ) -> z e. U )
153 suprub 
 |-  ( ( ( U C_ RR /\ U =/= (/) /\ E. x e. RR A. y e. U y <_ x ) /\ z e. U ) -> z <_ sup ( U , RR , < ) )
154 145 146 151 152 153 syl31anc 
 |-  ( ( ph /\ z e. U ) -> z <_ sup ( U , RR , < ) )
155 154 8 breqtrrdi 
 |-  ( ( ph /\ z e. U ) -> z <_ S )
156 155 ad2antrr 
 |-  ( ( ( ( ph /\ z e. U ) /\ j e. NN ) /\ ( D ` j ) <_ z ) -> z <_ S )
157 141 142 143 144 156 letrd 
 |-  ( ( ( ( ph /\ z e. U ) /\ j e. NN ) /\ ( D ` j ) <_ z ) -> ( D ` j ) <_ S )
158 157 iftrued 
 |-  ( ( ( ( ph /\ z e. U ) /\ j e. NN ) /\ ( D ` j ) <_ z ) -> if ( ( D ` j ) <_ S , ( D ` j ) , S ) = ( D ` j ) )
159 138 140 158 3eqtr4d 
 |-  ( ( ( ( ph /\ z e. U ) /\ j e. NN ) /\ ( D ` j ) <_ z ) -> if ( ( D ` j ) <_ z , ( D ` j ) , z ) = if ( ( D ` j ) <_ S , ( D ` j ) , S ) )
160 137 159 eqled 
 |-  ( ( ( ( ph /\ z e. U ) /\ j e. NN ) /\ ( D ` j ) <_ z ) -> if ( ( D ` j ) <_ z , ( D ` j ) , z ) <_ if ( ( D ` j ) <_ S , ( D ` j ) , S ) )
161 60 adantr 
 |-  ( ( ( ( ph /\ z e. U ) /\ j e. NN ) /\ -. ( D ` j ) <_ z ) -> z e. RR )
162 59 adantr 
 |-  ( ( ( ( ph /\ z e. U ) /\ j e. NN ) /\ -. ( D ` j ) <_ z ) -> ( D ` j ) e. RR )
163 simpr 
 |-  ( ( ( ( ph /\ z e. U ) /\ j e. NN ) /\ -. ( D ` j ) <_ z ) -> -. ( D ` j ) <_ z )
164 161 162 ltnled 
 |-  ( ( ( ( ph /\ z e. U ) /\ j e. NN ) /\ -. ( D ` j ) <_ z ) -> ( z < ( D ` j ) <-> -. ( D ` j ) <_ z ) )
165 163 164 mpbird 
 |-  ( ( ( ( ph /\ z e. U ) /\ j e. NN ) /\ -. ( D ` j ) <_ z ) -> z < ( D ` j ) )
166 161 162 165 ltled 
 |-  ( ( ( ( ph /\ z e. U ) /\ j e. NN ) /\ -. ( D ` j ) <_ z ) -> z <_ ( D ` j ) )
167 166 adantr 
 |-  ( ( ( ( ( ph /\ z e. U ) /\ j e. NN ) /\ -. ( D ` j ) <_ z ) /\ ( D ` j ) <_ S ) -> z <_ ( D ` j ) )
168 iffalse 
 |-  ( -. ( D ` j ) <_ z -> if ( ( D ` j ) <_ z , ( D ` j ) , z ) = z )
169 168 ad2antlr 
 |-  ( ( ( ( ( ph /\ z e. U ) /\ j e. NN ) /\ -. ( D ` j ) <_ z ) /\ ( D ` j ) <_ S ) -> if ( ( D ` j ) <_ z , ( D ` j ) , z ) = z )
170 iftrue 
 |-  ( ( D ` j ) <_ S -> if ( ( D ` j ) <_ S , ( D ` j ) , S ) = ( D ` j ) )
171 170 adantl 
 |-  ( ( ( ( ( ph /\ z e. U ) /\ j e. NN ) /\ -. ( D ` j ) <_ z ) /\ ( D ` j ) <_ S ) -> if ( ( D ` j ) <_ S , ( D ` j ) , S ) = ( D ` j ) )
172 169 171 breq12d 
 |-  ( ( ( ( ( ph /\ z e. U ) /\ j e. NN ) /\ -. ( D ` j ) <_ z ) /\ ( D ` j ) <_ S ) -> ( if ( ( D ` j ) <_ z , ( D ` j ) , z ) <_ if ( ( D ` j ) <_ S , ( D ` j ) , S ) <-> z <_ ( D ` j ) ) )
173 167 172 mpbird 
 |-  ( ( ( ( ( ph /\ z e. U ) /\ j e. NN ) /\ -. ( D ` j ) <_ z ) /\ ( D ` j ) <_ S ) -> if ( ( D ` j ) <_ z , ( D ` j ) , z ) <_ if ( ( D ` j ) <_ S , ( D ` j ) , S ) )
174 155 ad3antrrr 
 |-  ( ( ( ( ( ph /\ z e. U ) /\ j e. NN ) /\ -. ( D ` j ) <_ z ) /\ -. ( D ` j ) <_ S ) -> z <_ S )
175 168 ad2antlr 
 |-  ( ( ( ( ( ph /\ z e. U ) /\ j e. NN ) /\ -. ( D ` j ) <_ z ) /\ -. ( D ` j ) <_ S ) -> if ( ( D ` j ) <_ z , ( D ` j ) , z ) = z )
176 iffalse 
 |-  ( -. ( D ` j ) <_ S -> if ( ( D ` j ) <_ S , ( D ` j ) , S ) = S )
177 176 adantl 
 |-  ( ( ( ( ( ph /\ z e. U ) /\ j e. NN ) /\ -. ( D ` j ) <_ z ) /\ -. ( D ` j ) <_ S ) -> if ( ( D ` j ) <_ S , ( D ` j ) , S ) = S )
178 175 177 breq12d 
 |-  ( ( ( ( ( ph /\ z e. U ) /\ j e. NN ) /\ -. ( D ` j ) <_ z ) /\ -. ( D ` j ) <_ S ) -> ( if ( ( D ` j ) <_ z , ( D ` j ) , z ) <_ if ( ( D ` j ) <_ S , ( D ` j ) , S ) <-> z <_ S ) )
179 174 178 mpbird 
 |-  ( ( ( ( ( ph /\ z e. U ) /\ j e. NN ) /\ -. ( D ` j ) <_ z ) /\ -. ( D ` j ) <_ S ) -> if ( ( D ` j ) <_ z , ( D ` j ) , z ) <_ if ( ( D ` j ) <_ S , ( D ` j ) , S ) )
180 173 179 pm2.61dan 
 |-  ( ( ( ( ph /\ z e. U ) /\ j e. NN ) /\ -. ( D ` j ) <_ z ) -> if ( ( D ` j ) <_ z , ( D ` j ) , z ) <_ if ( ( D ` j ) <_ S , ( D ` j ) , S ) )
181 160 180 pm2.61dan 
 |-  ( ( ( ph /\ z e. U ) /\ j e. NN ) -> if ( ( D ` j ) <_ z , ( D ` j ) , z ) <_ if ( ( D ` j ) <_ S , ( D ` j ) , S ) )
182 icossico 
 |-  ( ( ( ( C ` j ) e. RR* /\ if ( ( D ` j ) <_ S , ( D ` j ) , S ) e. RR* ) /\ ( ( C ` j ) <_ ( C ` j ) /\ if ( ( D ` j ) <_ z , ( D ` j ) , z ) <_ if ( ( D ` j ) <_ S , ( D ` j ) , S ) ) ) -> ( ( C ` j ) [,) if ( ( D ` j ) <_ z , ( D ` j ) , z ) ) C_ ( ( C ` j ) [,) if ( ( D ` j ) <_ S , ( D ` j ) , S ) ) )
183 78 136 81 181 182 syl22anc 
 |-  ( ( ( ph /\ z e. U ) /\ j e. NN ) -> ( ( C ` j ) [,) if ( ( D ` j ) <_ z , ( D ` j ) , z ) ) C_ ( ( C ` j ) [,) if ( ( D ` j ) <_ S , ( D ` j ) , S ) ) )
184 volss 
 |-  ( ( ( ( C ` j ) [,) if ( ( D ` j ) <_ z , ( D ` j ) , z ) ) e. dom vol /\ ( ( C ` j ) [,) if ( ( D ` j ) <_ S , ( D ` j ) , S ) ) e. dom vol /\ ( ( C ` j ) [,) if ( ( D ` j ) <_ z , ( D ` j ) , z ) ) C_ ( ( C ` j ) [,) if ( ( D ` j ) <_ S , ( D ` j ) , S ) ) ) -> ( vol ` ( ( C ` j ) [,) if ( ( D ` j ) <_ z , ( D ` j ) , z ) ) ) <_ ( vol ` ( ( C ` j ) [,) if ( ( D ` j ) <_ S , ( D ` j ) , S ) ) ) )
185 64 135 183 184 syl3anc 
 |-  ( ( ( ph /\ z e. U ) /\ j e. NN ) -> ( vol ` ( ( C ` j ) [,) if ( ( D ` j ) <_ z , ( D ` j ) , z ) ) ) <_ ( vol ` ( ( C ` j ) [,) if ( ( D ` j ) <_ S , ( D ` j ) , S ) ) ) )
186 55 56 65 134 185 sge0lempt 
 |-  ( ( ph /\ z e. U ) -> ( sum^ ` ( j e. NN |-> ( vol ` ( ( C ` j ) [,) if ( ( D ` j ) <_ z , ( D ` j ) , z ) ) ) ) ) <_ ( sum^ ` ( j e. NN |-> ( vol ` ( ( C ` j ) [,) if ( ( D ` j ) <_ S , ( D ` j ) , S ) ) ) ) ) )
187 97 133 98 186 leadd1dd 
 |-  ( ( ph /\ z e. U ) -> ( ( sum^ ` ( j e. NN |-> ( vol ` ( ( C ` j ) [,) if ( ( D ` j ) <_ z , ( D ` j ) , z ) ) ) ) ) + A ) <_ ( ( sum^ ` ( j e. NN |-> ( vol ` ( ( C ` j ) [,) if ( ( D ` j ) <_ S , ( D ` j ) , S ) ) ) ) ) + A ) )
188 54 99 124 132 187 letrd 
 |-  ( ( ph /\ z e. U ) -> z <_ ( ( sum^ ` ( j e. NN |-> ( vol ` ( ( C ` j ) [,) if ( ( D ` j ) <_ S , ( D ` j ) , S ) ) ) ) ) + A ) )
189 188 ex 
 |-  ( ph -> ( z e. U -> z <_ ( ( sum^ ` ( j e. NN |-> ( vol ` ( ( C ` j ) [,) if ( ( D ` j ) <_ S , ( D ` j ) , S ) ) ) ) ) + A ) ) )
190 51 189 ralrimi 
 |-  ( ph -> A. z e. U z <_ ( ( sum^ ` ( j e. NN |-> ( vol ` ( ( C ` j ) [,) if ( ( D ` j ) <_ S , ( D ` j ) , S ) ) ) ) ) + A ) )
191 suprleub 
 |-  ( ( ( U C_ RR /\ U =/= (/) /\ E. x e. RR A. y e. U y <_ x ) /\ ( ( sum^ ` ( j e. NN |-> ( vol ` ( ( C ` j ) [,) if ( ( D ` j ) <_ S , ( D ` j ) , S ) ) ) ) ) + A ) e. RR ) -> ( sup ( U , RR , < ) <_ ( ( sum^ ` ( j e. NN |-> ( vol ` ( ( C ` j ) [,) if ( ( D ` j ) <_ S , ( D ` j ) , S ) ) ) ) ) + A ) <-> A. z e. U z <_ ( ( sum^ ` ( j e. NN |-> ( vol ` ( ( C ` j ) [,) if ( ( D ` j ) <_ S , ( D ` j ) , S ) ) ) ) ) + A ) ) )
192 53 47 150 123 191 syl31anc 
 |-  ( ph -> ( sup ( U , RR , < ) <_ ( ( sum^ ` ( j e. NN |-> ( vol ` ( ( C ` j ) [,) if ( ( D ` j ) <_ S , ( D ` j ) , S ) ) ) ) ) + A ) <-> A. z e. U z <_ ( ( sum^ ` ( j e. NN |-> ( vol ` ( ( C ` j ) [,) if ( ( D ` j ) <_ S , ( D ` j ) , S ) ) ) ) ) + A ) ) )
193 190 192 mpbird 
 |-  ( ph -> sup ( U , RR , < ) <_ ( ( sum^ ` ( j e. NN |-> ( vol ` ( ( C ` j ) [,) if ( ( D ` j ) <_ S , ( D ` j ) , S ) ) ) ) ) + A ) )
194 50 193 eqbrtrd 
 |-  ( ph -> S <_ ( ( sum^ ` ( j e. NN |-> ( vol ` ( ( C ` j ) [,) if ( ( D ` j ) <_ S , ( D ` j ) , S ) ) ) ) ) + A ) )
195 100 1 122 lesubaddd 
 |-  ( ph -> ( ( S - A ) <_ ( sum^ ` ( j e. NN |-> ( vol ` ( ( C ` j ) [,) if ( ( D ` j ) <_ S , ( D ` j ) , S ) ) ) ) ) <-> S <_ ( ( sum^ ` ( j e. NN |-> ( vol ` ( ( C ` j ) [,) if ( ( D ` j ) <_ S , ( D ` j ) , S ) ) ) ) ) + A ) ) )
196 194 195 mpbird 
 |-  ( ph -> ( S - A ) <_ ( sum^ ` ( j e. NN |-> ( vol ` ( ( C ` j ) [,) if ( ( D ` j ) <_ S , ( D ` j ) , S ) ) ) ) ) )
197 49 196 jca 
 |-  ( ph -> ( S e. ( A [,] B ) /\ ( S - A ) <_ ( sum^ ` ( j e. NN |-> ( vol ` ( ( C ` j ) [,) if ( ( D ` j ) <_ S , ( D ` j ) , S ) ) ) ) ) ) )
198 oveq1 
 |-  ( z = S -> ( z - A ) = ( S - A ) )
199 breq2 
 |-  ( z = S -> ( ( D ` j ) <_ z <-> ( D ` j ) <_ S ) )
200 id 
 |-  ( z = S -> z = S )
201 199 200 ifbieq2d 
 |-  ( z = S -> if ( ( D ` j ) <_ z , ( D ` j ) , z ) = if ( ( D ` j ) <_ S , ( D ` j ) , S ) )
202 201 oveq2d 
 |-  ( z = S -> ( ( C ` j ) [,) if ( ( D ` j ) <_ z , ( D ` j ) , z ) ) = ( ( C ` j ) [,) if ( ( D ` j ) <_ S , ( D ` j ) , S ) ) )
203 202 fveq2d 
 |-  ( z = S -> ( vol ` ( ( C ` j ) [,) if ( ( D ` j ) <_ z , ( D ` j ) , z ) ) ) = ( vol ` ( ( C ` j ) [,) if ( ( D ` j ) <_ S , ( D ` j ) , S ) ) ) )
204 203 mpteq2dv 
 |-  ( z = S -> ( j e. NN |-> ( vol ` ( ( C ` j ) [,) if ( ( D ` j ) <_ z , ( D ` j ) , z ) ) ) ) = ( j e. NN |-> ( vol ` ( ( C ` j ) [,) if ( ( D ` j ) <_ S , ( D ` j ) , S ) ) ) ) )
205 204 fveq2d 
 |-  ( z = S -> ( sum^ ` ( j e. NN |-> ( vol ` ( ( C ` j ) [,) if ( ( D ` j ) <_ z , ( D ` j ) , z ) ) ) ) ) = ( sum^ ` ( j e. NN |-> ( vol ` ( ( C ` j ) [,) if ( ( D ` j ) <_ S , ( D ` j ) , S ) ) ) ) ) )
206 198 205 breq12d 
 |-  ( z = S -> ( ( z - A ) <_ ( sum^ ` ( j e. NN |-> ( vol ` ( ( C ` j ) [,) if ( ( D ` j ) <_ z , ( D ` j ) , z ) ) ) ) ) <-> ( S - A ) <_ ( sum^ ` ( j e. NN |-> ( vol ` ( ( C ` j ) [,) if ( ( D ` j ) <_ S , ( D ` j ) , S ) ) ) ) ) ) )
207 206 elrab 
 |-  ( S e. { z e. ( A [,] B ) | ( z - A ) <_ ( sum^ ` ( j e. NN |-> ( vol ` ( ( C ` j ) [,) if ( ( D ` j ) <_ z , ( D ` j ) , z ) ) ) ) ) } <-> ( S e. ( A [,] B ) /\ ( S - A ) <_ ( sum^ ` ( j e. NN |-> ( vol ` ( ( C ` j ) [,) if ( ( D ` j ) <_ S , ( D ` j ) , S ) ) ) ) ) ) )
208 197 207 sylibr 
 |-  ( ph -> S e. { z e. ( A [,] B ) | ( z - A ) <_ ( sum^ ` ( j e. NN |-> ( vol ` ( ( C ` j ) [,) if ( ( D ` j ) <_ z , ( D ` j ) , z ) ) ) ) ) } )
209 208 7 eleqtrrdi 
 |-  ( ph -> S e. U )
210 209 46 150 3jca 
 |-  ( ph -> ( S e. U /\ A e. U /\ E. x e. RR A. y e. U y <_ x ) )