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 ( 𝜑𝐴 ∈ ℝ )
hoidmv1lelem1.b ( 𝜑𝐵 ∈ ℝ )
hoidmv1lelem1.l ( 𝜑𝐴 < 𝐵 )
hoidmv1lelem1.c ( 𝜑𝐶 : ℕ ⟶ ℝ )
hoidmv1lelem1.d ( 𝜑𝐷 : ℕ ⟶ ℝ )
hoidmv1lelem1.r ( 𝜑 → ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( vol ‘ ( ( 𝐶𝑗 ) [,) ( 𝐷𝑗 ) ) ) ) ) ∈ ℝ )
hoidmv1lelem1.u 𝑈 = { 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ∣ ( 𝑧𝐴 ) ≤ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( vol ‘ ( ( 𝐶𝑗 ) [,) if ( ( 𝐷𝑗 ) ≤ 𝑧 , ( 𝐷𝑗 ) , 𝑧 ) ) ) ) ) }
hoidmv1lelem1.s 𝑆 = sup ( 𝑈 , ℝ , < )
Assertion hoidmv1lelem1 ( 𝜑 → ( 𝑆𝑈𝐴𝑈 ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦𝑈 𝑦𝑥 ) )

Proof

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