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 ffvelcdmda 
 |-  ( ( ph /\ j e. NN ) -> ( C ` j ) e. RR )
25 5 ffvelcdmda 
 |-  ( ( 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 ffvelcdmd 
 |-  ( ( 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 ffvelcdmd 
 |-  ( ( ( 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 ffvelcdmd 
 |-  ( ( 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 ffvelcdmd 
 |-  ( ( 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 bilani 
 |-  ( ( 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 ) ) ) ) ) } )
127 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 ) ) ) ) ) ) )
128 126 127 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 ) ) ) ) ) ) )
129 128 simprd 
 |-  ( ( ph /\ z e. U ) -> ( z - A ) <_ ( sum^ ` ( j e. NN |-> ( vol ` ( ( C ` j ) [,) if ( ( D ` j ) <_ z , ( D ` j ) , z ) ) ) ) ) )
130 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 ) ) )
131 129 130 mpbid 
 |-  ( ( ph /\ z e. U ) -> z <_ ( ( sum^ ` ( j e. NN |-> ( vol ` ( ( C ` j ) [,) if ( ( D ` j ) <_ z , ( D ` j ) , z ) ) ) ) ) + A ) )
132 122 adantr 
 |-  ( ( ph /\ z e. U ) -> ( sum^ ` ( j e. NN |-> ( vol ` ( ( C ` j ) [,) if ( ( D ` j ) <_ S , ( D ` j ) , S ) ) ) ) ) e. RR )
133 106 adantlr 
 |-  ( ( ( ph /\ z e. U ) /\ j e. NN ) -> ( vol ` ( ( C ` j ) [,) if ( ( D ` j ) <_ S , ( D ` j ) , S ) ) ) e. ( 0 [,] +oo ) )
134 105 adantlr 
 |-  ( ( ( ph /\ z e. U ) /\ j e. NN ) -> ( ( C ` j ) [,) if ( ( D ` j ) <_ S , ( D ` j ) , S ) ) e. dom vol )
135 103 adantlr 
 |-  ( ( ( ph /\ z e. U ) /\ j e. NN ) -> if ( ( D ` j ) <_ S , ( D ` j ) , S ) e. RR* )
136 61 adantr 
 |-  ( ( ( ( ph /\ z e. U ) /\ j e. NN ) /\ ( D ` j ) <_ z ) -> if ( ( D ` j ) <_ z , ( D ` j ) , z ) e. RR )
137 eqidd 
 |-  ( ( ( ( ph /\ z e. U ) /\ j e. NN ) /\ ( D ` j ) <_ z ) -> ( D ` j ) = ( D ` j ) )
138 iftrue 
 |-  ( ( D ` j ) <_ z -> if ( ( D ` j ) <_ z , ( D ` j ) , z ) = ( D ` j ) )
139 138 adantl 
 |-  ( ( ( ( ph /\ z e. U ) /\ j e. NN ) /\ ( D ` j ) <_ z ) -> if ( ( D ` j ) <_ z , ( D ` j ) , z ) = ( D ` j ) )
140 59 adantr 
 |-  ( ( ( ( ph /\ z e. U ) /\ j e. NN ) /\ ( D ` j ) <_ z ) -> ( D ` j ) e. RR )
141 60 adantr 
 |-  ( ( ( ( ph /\ z e. U ) /\ j e. NN ) /\ ( D ` j ) <_ z ) -> z e. RR )
142 100 ad3antrrr 
 |-  ( ( ( ( ph /\ z e. U ) /\ j e. NN ) /\ ( D ` j ) <_ z ) -> S e. RR )
143 simpr 
 |-  ( ( ( ( ph /\ z e. U ) /\ j e. NN ) /\ ( D ` j ) <_ z ) -> ( D ` j ) <_ z )
144 53 adantr 
 |-  ( ( ph /\ z e. U ) -> U C_ RR )
145 47 adantr 
 |-  ( ( ph /\ z e. U ) -> U =/= (/) )
146 1 2 jca 
 |-  ( ph -> ( A e. RR /\ B e. RR ) )
147 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 ) )
148 146 11 46 147 syl3anc 
 |-  ( ph -> ( U C_ RR /\ U =/= (/) /\ E. x e. RR A. y e. U y <_ x ) )
149 148 simp3d 
 |-  ( ph -> E. x e. RR A. y e. U y <_ x )
150 149 adantr 
 |-  ( ( ph /\ z e. U ) -> E. x e. RR A. y e. U y <_ x )
151 126 125 sylibr 
 |-  ( ( ph /\ z e. U ) -> z e. U )
152 suprub 
 |-  ( ( ( U C_ RR /\ U =/= (/) /\ E. x e. RR A. y e. U y <_ x ) /\ z e. U ) -> z <_ sup ( U , RR , < ) )
153 144 145 150 151 152 syl31anc 
 |-  ( ( ph /\ z e. U ) -> z <_ sup ( U , RR , < ) )
154 153 8 breqtrrdi 
 |-  ( ( ph /\ z e. U ) -> z <_ S )
155 154 ad2antrr 
 |-  ( ( ( ( ph /\ z e. U ) /\ j e. NN ) /\ ( D ` j ) <_ z ) -> z <_ S )
156 140 141 142 143 155 letrd 
 |-  ( ( ( ( ph /\ z e. U ) /\ j e. NN ) /\ ( D ` j ) <_ z ) -> ( D ` j ) <_ S )
157 156 iftrued 
 |-  ( ( ( ( ph /\ z e. U ) /\ j e. NN ) /\ ( D ` j ) <_ z ) -> if ( ( D ` j ) <_ S , ( D ` j ) , S ) = ( D ` j ) )
158 137 139 157 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 ) )
159 136 158 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 ) )
160 60 adantr 
 |-  ( ( ( ( ph /\ z e. U ) /\ j e. NN ) /\ -. ( D ` j ) <_ z ) -> z e. RR )
161 59 adantr 
 |-  ( ( ( ( ph /\ z e. U ) /\ j e. NN ) /\ -. ( D ` j ) <_ z ) -> ( D ` j ) e. RR )
162 simpr 
 |-  ( ( ( ( ph /\ z e. U ) /\ j e. NN ) /\ -. ( D ` j ) <_ z ) -> -. ( D ` j ) <_ z )
163 160 161 ltnled 
 |-  ( ( ( ( ph /\ z e. U ) /\ j e. NN ) /\ -. ( D ` j ) <_ z ) -> ( z < ( D ` j ) <-> -. ( D ` j ) <_ z ) )
164 162 163 mpbird 
 |-  ( ( ( ( ph /\ z e. U ) /\ j e. NN ) /\ -. ( D ` j ) <_ z ) -> z < ( D ` j ) )
165 160 161 164 ltled 
 |-  ( ( ( ( ph /\ z e. U ) /\ j e. NN ) /\ -. ( D ` j ) <_ z ) -> z <_ ( D ` j ) )
166 165 adantr 
 |-  ( ( ( ( ( ph /\ z e. U ) /\ j e. NN ) /\ -. ( D ` j ) <_ z ) /\ ( D ` j ) <_ S ) -> z <_ ( D ` j ) )
167 iffalse 
 |-  ( -. ( D ` j ) <_ z -> if ( ( D ` j ) <_ z , ( D ` j ) , z ) = z )
168 167 ad2antlr 
 |-  ( ( ( ( ( ph /\ z e. U ) /\ j e. NN ) /\ -. ( D ` j ) <_ z ) /\ ( D ` j ) <_ S ) -> if ( ( D ` j ) <_ z , ( D ` j ) , z ) = z )
169 iftrue 
 |-  ( ( D ` j ) <_ S -> if ( ( D ` j ) <_ S , ( D ` j ) , S ) = ( D ` j ) )
170 169 adantl 
 |-  ( ( ( ( ( ph /\ z e. U ) /\ j e. NN ) /\ -. ( D ` j ) <_ z ) /\ ( D ` j ) <_ S ) -> if ( ( D ` j ) <_ S , ( D ` j ) , S ) = ( D ` j ) )
171 168 170 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 ) ) )
172 166 171 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 ) )
173 154 ad3antrrr 
 |-  ( ( ( ( ( ph /\ z e. U ) /\ j e. NN ) /\ -. ( D ` j ) <_ z ) /\ -. ( D ` j ) <_ S ) -> z <_ S )
174 167 ad2antlr 
 |-  ( ( ( ( ( ph /\ z e. U ) /\ j e. NN ) /\ -. ( D ` j ) <_ z ) /\ -. ( D ` j ) <_ S ) -> if ( ( D ` j ) <_ z , ( D ` j ) , z ) = z )
175 iffalse 
 |-  ( -. ( D ` j ) <_ S -> if ( ( D ` j ) <_ S , ( D ` j ) , S ) = S )
176 175 adantl 
 |-  ( ( ( ( ( ph /\ z e. U ) /\ j e. NN ) /\ -. ( D ` j ) <_ z ) /\ -. ( D ` j ) <_ S ) -> if ( ( D ` j ) <_ S , ( D ` j ) , S ) = S )
177 174 176 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 ) )
178 173 177 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 ) )
179 172 178 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 ) )
180 159 179 pm2.61dan 
 |-  ( ( ( ph /\ z e. U ) /\ j e. NN ) -> if ( ( D ` j ) <_ z , ( D ` j ) , z ) <_ if ( ( D ` j ) <_ S , ( D ` j ) , S ) )
181 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 ) ) )
182 78 135 81 180 181 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 ) ) )
183 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 ) ) ) )
184 64 134 182 183 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 ) ) ) )
185 55 56 65 133 184 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 ) ) ) ) ) )
186 97 132 98 185 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 ) )
187 54 99 124 131 186 letrd 
 |-  ( ( ph /\ z e. U ) -> z <_ ( ( sum^ ` ( j e. NN |-> ( vol ` ( ( C ` j ) [,) if ( ( D ` j ) <_ S , ( D ` j ) , S ) ) ) ) ) + A ) )
188 187 ex 
 |-  ( ph -> ( z e. U -> z <_ ( ( sum^ ` ( j e. NN |-> ( vol ` ( ( C ` j ) [,) if ( ( D ` j ) <_ S , ( D ` j ) , S ) ) ) ) ) + A ) ) )
189 51 188 ralrimi 
 |-  ( ph -> A. z e. U z <_ ( ( sum^ ` ( j e. NN |-> ( vol ` ( ( C ` j ) [,) if ( ( D ` j ) <_ S , ( D ` j ) , S ) ) ) ) ) + A ) )
190 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 ) ) )
191 53 47 149 123 190 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 ) ) )
192 189 191 mpbird 
 |-  ( ph -> sup ( U , RR , < ) <_ ( ( sum^ ` ( j e. NN |-> ( vol ` ( ( C ` j ) [,) if ( ( D ` j ) <_ S , ( D ` j ) , S ) ) ) ) ) + A ) )
193 50 192 eqbrtrd 
 |-  ( ph -> S <_ ( ( sum^ ` ( j e. NN |-> ( vol ` ( ( C ` j ) [,) if ( ( D ` j ) <_ S , ( D ` j ) , S ) ) ) ) ) + A ) )
194 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 ) ) )
195 193 194 mpbird 
 |-  ( ph -> ( S - A ) <_ ( sum^ ` ( j e. NN |-> ( vol ` ( ( C ` j ) [,) if ( ( D ` j ) <_ S , ( D ` j ) , S ) ) ) ) ) )
196 49 195 jca 
 |-  ( ph -> ( S e. ( A [,] B ) /\ ( S - A ) <_ ( sum^ ` ( j e. NN |-> ( vol ` ( ( C ` j ) [,) if ( ( D ` j ) <_ S , ( D ` j ) , S ) ) ) ) ) ) )
197 oveq1 
 |-  ( z = S -> ( z - A ) = ( S - A ) )
198 breq2 
 |-  ( z = S -> ( ( D ` j ) <_ z <-> ( D ` j ) <_ S ) )
199 id 
 |-  ( z = S -> z = S )
200 198 199 ifbieq2d 
 |-  ( z = S -> if ( ( D ` j ) <_ z , ( D ` j ) , z ) = if ( ( D ` j ) <_ S , ( D ` j ) , S ) )
201 200 oveq2d 
 |-  ( z = S -> ( ( C ` j ) [,) if ( ( D ` j ) <_ z , ( D ` j ) , z ) ) = ( ( C ` j ) [,) if ( ( D ` j ) <_ S , ( D ` j ) , S ) ) )
202 201 fveq2d 
 |-  ( z = S -> ( vol ` ( ( C ` j ) [,) if ( ( D ` j ) <_ z , ( D ` j ) , z ) ) ) = ( vol ` ( ( C ` j ) [,) if ( ( D ` j ) <_ S , ( D ` j ) , S ) ) ) )
203 202 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 ) ) ) ) )
204 203 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 ) ) ) ) ) )
205 197 204 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 ) ) ) ) ) ) )
206 205 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 ) ) ) ) ) ) )
207 196 206 sylibr 
 |-  ( ph -> S e. { z e. ( A [,] B ) | ( z - A ) <_ ( sum^ ` ( j e. NN |-> ( vol ` ( ( C ` j ) [,) if ( ( D ` j ) <_ z , ( D ` j ) , z ) ) ) ) ) } )
208 207 7 eleqtrrdi 
 |-  ( ph -> S e. U )
209 208 46 149 3jca 
 |-  ( ph -> ( S e. U /\ A e. U /\ E. x e. RR A. y e. U y <_ x ) )