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

Proof

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