This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem itgcn

Description: Transfer itg2cn to the full Lebesgue integral. (Contributed by Mario Carneiro, 1-Sep-2014)

Ref Expression
Hypotheses itgcn.1 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ 𝑉 )
itgcn.2 ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ 𝐿1 )
itgcn.3 ⊢ ( 𝜑 → 𝐶 ∈ ℝ+ )
Assertion itgcn ( 𝜑 → ∃ 𝑑 ∈ ℝ+ ∀ 𝑢 ∈ dom vol ( ( 𝑢 ⊆ 𝐴 ∧ ( vol ‘ 𝑢 ) < 𝑑 ) → ∫ 𝑢 ( abs ‘ 𝐵 ) d 𝑥 < 𝐶 ) )

Proof

Step Hyp Ref Expression
1 itgcn.1 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ 𝑉 )
2 itgcn.2 ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ 𝐿1 )
3 itgcn.3 ⊢ ( 𝜑 → 𝐶 ∈ ℝ+ )
4 iblmbf ⊢ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ 𝐿1 → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ MblFn )
5 2 4 syl ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ MblFn )
6 5 1 mbfmptcl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ℂ )
7 6 abscld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( abs ‘ 𝐵 ) ∈ ℝ )
8 6 absge0d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 0 ≤ ( abs ‘ 𝐵 ) )
9 elrege0 ⊢ ( ( abs ‘ 𝐵 ) ∈ ( 0 [,) +∞ ) ↔ ( ( abs ‘ 𝐵 ) ∈ ℝ ∧ 0 ≤ ( abs ‘ 𝐵 ) ) )
10 7 8 9 sylanbrc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( abs ‘ 𝐵 ) ∈ ( 0 [,) +∞ ) )
11 0e0icopnf ⊢ 0 ∈ ( 0 [,) +∞ )
12 11 a1i ⊢ ( ( 𝜑 ∧ ¬ 𝑥 ∈ 𝐴 ) → 0 ∈ ( 0 [,) +∞ ) )
13 10 12 ifclda ⊢ ( 𝜑 → if ( 𝑥 ∈ 𝐴 , ( abs ‘ 𝐵 ) , 0 ) ∈ ( 0 [,) +∞ ) )
14 13 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → if ( 𝑥 ∈ 𝐴 , ( abs ‘ 𝐵 ) , 0 ) ∈ ( 0 [,) +∞ ) )
15 14 fmpttd ⊢ ( 𝜑 → ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , ( abs ‘ 𝐵 ) , 0 ) ) : ℝ ⟶ ( 0 [,) +∞ ) )
16 5 1 mbfdm2 ⊢ ( 𝜑 → 𝐴 ∈ dom vol )
17 mblss ⊢ ( 𝐴 ∈ dom vol → 𝐴 ⊆ ℝ )
18 16 17 syl ⊢ ( 𝜑 → 𝐴 ⊆ ℝ )
19 rembl ⊢ ℝ ∈ dom vol
20 19 a1i ⊢ ( 𝜑 → ℝ ∈ dom vol )
21 13 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → if ( 𝑥 ∈ 𝐴 , ( abs ‘ 𝐵 ) , 0 ) ∈ ( 0 [,) +∞ ) )
22 eldifn ⊢ ( 𝑥 ∈ ( ℝ ∖ 𝐴 ) → ¬ 𝑥 ∈ 𝐴 )
23 22 adantl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ℝ ∖ 𝐴 ) ) → ¬ 𝑥 ∈ 𝐴 )
24 23 iffalsed ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ℝ ∖ 𝐴 ) ) → if ( 𝑥 ∈ 𝐴 , ( abs ‘ 𝐵 ) , 0 ) = 0 )
25 iftrue ⊢ ( 𝑥 ∈ 𝐴 → if ( 𝑥 ∈ 𝐴 , ( abs ‘ 𝐵 ) , 0 ) = ( abs ‘ 𝐵 ) )
26 25 mpteq2ia ⊢ ( 𝑥 ∈ 𝐴 ↦ if ( 𝑥 ∈ 𝐴 , ( abs ‘ 𝐵 ) , 0 ) ) = ( 𝑥 ∈ 𝐴 ↦ ( abs ‘ 𝐵 ) )
27 1 2 iblabs ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ ( abs ‘ 𝐵 ) ) ∈ 𝐿1 )
28 7 8 iblpos ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐴 ↦ ( abs ‘ 𝐵 ) ) ∈ 𝐿1 ↔ ( ( 𝑥 ∈ 𝐴 ↦ ( abs ‘ 𝐵 ) ) ∈ MblFn ∧ ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , ( abs ‘ 𝐵 ) , 0 ) ) ) ∈ ℝ ) ) )
29 27 28 mpbid ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐴 ↦ ( abs ‘ 𝐵 ) ) ∈ MblFn ∧ ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , ( abs ‘ 𝐵 ) , 0 ) ) ) ∈ ℝ ) )
30 29 simpld ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ ( abs ‘ 𝐵 ) ) ∈ MblFn )
31 26 30 eqeltrid ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ if ( 𝑥 ∈ 𝐴 , ( abs ‘ 𝐵 ) , 0 ) ) ∈ MblFn )
32 18 20 21 24 31 mbfss ⊢ ( 𝜑 → ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , ( abs ‘ 𝐵 ) , 0 ) ) ∈ MblFn )
33 29 simprd ⊢ ( 𝜑 → ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , ( abs ‘ 𝐵 ) , 0 ) ) ) ∈ ℝ )
34 15 32 33 3 itg2cn ⊢ ( 𝜑 → ∃ 𝑑 ∈ ℝ+ ∀ 𝑢 ∈ dom vol ( ( vol ‘ 𝑢 ) < 𝑑 → ( ∫2 ‘ ( 𝑦 ∈ ℝ ↦ if ( 𝑦 ∈ 𝑢 , ( ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , ( abs ‘ 𝐵 ) , 0 ) ) ‘ 𝑦 ) , 0 ) ) ) < 𝐶 ) )
35 simprr ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ 𝑢 ⊆ 𝐴 ) ) → 𝑢 ⊆ 𝐴 )
36 35 sselda ⊢ ( ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ 𝑢 ⊆ 𝐴 ) ) ∧ 𝑥 ∈ 𝑢 ) → 𝑥 ∈ 𝐴 )
37 6 adantlr ⊢ ( ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ 𝑢 ⊆ 𝐴 ) ) ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ℂ )
38 36 37 syldan ⊢ ( ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ 𝑢 ⊆ 𝐴 ) ) ∧ 𝑥 ∈ 𝑢 ) → 𝐵 ∈ ℂ )
39 38 abscld ⊢ ( ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ 𝑢 ⊆ 𝐴 ) ) ∧ 𝑥 ∈ 𝑢 ) → ( abs ‘ 𝐵 ) ∈ ℝ )
40 simprl ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ 𝑢 ⊆ 𝐴 ) ) → 𝑢 ∈ dom vol )
41 37 abscld ⊢ ( ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ 𝑢 ⊆ 𝐴 ) ) ∧ 𝑥 ∈ 𝐴 ) → ( abs ‘ 𝐵 ) ∈ ℝ )
42 27 adantr ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ 𝑢 ⊆ 𝐴 ) ) → ( 𝑥 ∈ 𝐴 ↦ ( abs ‘ 𝐵 ) ) ∈ 𝐿1 )
43 35 40 41 42 iblss ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ 𝑢 ⊆ 𝐴 ) ) → ( 𝑥 ∈ 𝑢 ↦ ( abs ‘ 𝐵 ) ) ∈ 𝐿1 )
44 38 absge0d ⊢ ( ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ 𝑢 ⊆ 𝐴 ) ) ∧ 𝑥 ∈ 𝑢 ) → 0 ≤ ( abs ‘ 𝐵 ) )
45 39 43 44 itgposval ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ 𝑢 ⊆ 𝐴 ) ) → ∫ 𝑢 ( abs ‘ 𝐵 ) d 𝑥 = ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝑢 , ( abs ‘ 𝐵 ) , 0 ) ) ) )
46 35 sseld ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ 𝑢 ⊆ 𝐴 ) ) → ( 𝑥 ∈ 𝑢 → 𝑥 ∈ 𝐴 ) )
47 46 pm4.71d ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ 𝑢 ⊆ 𝐴 ) ) → ( 𝑥 ∈ 𝑢 ↔ ( 𝑥 ∈ 𝑢 ∧ 𝑥 ∈ 𝐴 ) ) )
48 47 ifbid ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ 𝑢 ⊆ 𝐴 ) ) → if ( 𝑥 ∈ 𝑢 , ( abs ‘ 𝐵 ) , 0 ) = if ( ( 𝑥 ∈ 𝑢 ∧ 𝑥 ∈ 𝐴 ) , ( abs ‘ 𝐵 ) , 0 ) )
49 ifan ⊢ if ( ( 𝑥 ∈ 𝑢 ∧ 𝑥 ∈ 𝐴 ) , ( abs ‘ 𝐵 ) , 0 ) = if ( 𝑥 ∈ 𝑢 , if ( 𝑥 ∈ 𝐴 , ( abs ‘ 𝐵 ) , 0 ) , 0 )
50 48 49 eqtrdi ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ 𝑢 ⊆ 𝐴 ) ) → if ( 𝑥 ∈ 𝑢 , ( abs ‘ 𝐵 ) , 0 ) = if ( 𝑥 ∈ 𝑢 , if ( 𝑥 ∈ 𝐴 , ( abs ‘ 𝐵 ) , 0 ) , 0 ) )
51 50 mpteq2dv ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ 𝑢 ⊆ 𝐴 ) ) → ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝑢 , ( abs ‘ 𝐵 ) , 0 ) ) = ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝑢 , if ( 𝑥 ∈ 𝐴 , ( abs ‘ 𝐵 ) , 0 ) , 0 ) ) )
52 51 fveq2d ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ 𝑢 ⊆ 𝐴 ) ) → ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝑢 , ( abs ‘ 𝐵 ) , 0 ) ) ) = ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝑢 , if ( 𝑥 ∈ 𝐴 , ( abs ‘ 𝐵 ) , 0 ) , 0 ) ) ) )
53 45 52 eqtrd ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ 𝑢 ⊆ 𝐴 ) ) → ∫ 𝑢 ( abs ‘ 𝐵 ) d 𝑥 = ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝑢 , if ( 𝑥 ∈ 𝐴 , ( abs ‘ 𝐵 ) , 0 ) , 0 ) ) ) )
54 nfv ⊢ Ⅎ 𝑥 𝑦 ∈ 𝑢
55 nffvmpt1 ⊢ Ⅎ 𝑥 ( ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , ( abs ‘ 𝐵 ) , 0 ) ) ‘ 𝑦 )
56 nfcv ⊢ Ⅎ 𝑥 0
57 54 55 56 nfif ⊢ Ⅎ 𝑥 if ( 𝑦 ∈ 𝑢 , ( ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , ( abs ‘ 𝐵 ) , 0 ) ) ‘ 𝑦 ) , 0 )
58 nfcv ⊢ Ⅎ 𝑦 if ( 𝑥 ∈ 𝑢 , ( ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , ( abs ‘ 𝐵 ) , 0 ) ) ‘ 𝑥 ) , 0 )
59 elequ1 ⊢ ( 𝑦 = 𝑥 → ( 𝑦 ∈ 𝑢 ↔ 𝑥 ∈ 𝑢 ) )
60 fveq2 ⊢ ( 𝑦 = 𝑥 → ( ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , ( abs ‘ 𝐵 ) , 0 ) ) ‘ 𝑦 ) = ( ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , ( abs ‘ 𝐵 ) , 0 ) ) ‘ 𝑥 ) )
61 59 60 ifbieq1d ⊢ ( 𝑦 = 𝑥 → if ( 𝑦 ∈ 𝑢 , ( ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , ( abs ‘ 𝐵 ) , 0 ) ) ‘ 𝑦 ) , 0 ) = if ( 𝑥 ∈ 𝑢 , ( ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , ( abs ‘ 𝐵 ) , 0 ) ) ‘ 𝑥 ) , 0 ) )
62 57 58 61 cbvmpt ⊢ ( 𝑦 ∈ ℝ ↦ if ( 𝑦 ∈ 𝑢 , ( ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , ( abs ‘ 𝐵 ) , 0 ) ) ‘ 𝑦 ) , 0 ) ) = ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝑢 , ( ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , ( abs ‘ 𝐵 ) , 0 ) ) ‘ 𝑥 ) , 0 ) )
63 fvex ⊢ ( abs ‘ 𝐵 ) ∈ V
64 c0ex ⊢ 0 ∈ V
65 63 64 ifex ⊢ if ( 𝑥 ∈ 𝐴 , ( abs ‘ 𝐵 ) , 0 ) ∈ V
66 eqid ⊢ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , ( abs ‘ 𝐵 ) , 0 ) ) = ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , ( abs ‘ 𝐵 ) , 0 ) )
67 66 fvmpt2 ⊢ ( ( 𝑥 ∈ ℝ ∧ if ( 𝑥 ∈ 𝐴 , ( abs ‘ 𝐵 ) , 0 ) ∈ V ) → ( ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , ( abs ‘ 𝐵 ) , 0 ) ) ‘ 𝑥 ) = if ( 𝑥 ∈ 𝐴 , ( abs ‘ 𝐵 ) , 0 ) )
68 65 67 mpan2 ⊢ ( 𝑥 ∈ ℝ → ( ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , ( abs ‘ 𝐵 ) , 0 ) ) ‘ 𝑥 ) = if ( 𝑥 ∈ 𝐴 , ( abs ‘ 𝐵 ) , 0 ) )
69 68 ifeq1d ⊢ ( 𝑥 ∈ ℝ → if ( 𝑥 ∈ 𝑢 , ( ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , ( abs ‘ 𝐵 ) , 0 ) ) ‘ 𝑥 ) , 0 ) = if ( 𝑥 ∈ 𝑢 , if ( 𝑥 ∈ 𝐴 , ( abs ‘ 𝐵 ) , 0 ) , 0 ) )
70 69 mpteq2ia ⊢ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝑢 , ( ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , ( abs ‘ 𝐵 ) , 0 ) ) ‘ 𝑥 ) , 0 ) ) = ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝑢 , if ( 𝑥 ∈ 𝐴 , ( abs ‘ 𝐵 ) , 0 ) , 0 ) )
71 62 70 eqtri ⊢ ( 𝑦 ∈ ℝ ↦ if ( 𝑦 ∈ 𝑢 , ( ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , ( abs ‘ 𝐵 ) , 0 ) ) ‘ 𝑦 ) , 0 ) ) = ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝑢 , if ( 𝑥 ∈ 𝐴 , ( abs ‘ 𝐵 ) , 0 ) , 0 ) )
72 71 fveq2i ⊢ ( ∫2 ‘ ( 𝑦 ∈ ℝ ↦ if ( 𝑦 ∈ 𝑢 , ( ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , ( abs ‘ 𝐵 ) , 0 ) ) ‘ 𝑦 ) , 0 ) ) ) = ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝑢 , if ( 𝑥 ∈ 𝐴 , ( abs ‘ 𝐵 ) , 0 ) , 0 ) ) )
73 53 72 eqtr4di ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ 𝑢 ⊆ 𝐴 ) ) → ∫ 𝑢 ( abs ‘ 𝐵 ) d 𝑥 = ( ∫2 ‘ ( 𝑦 ∈ ℝ ↦ if ( 𝑦 ∈ 𝑢 , ( ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , ( abs ‘ 𝐵 ) , 0 ) ) ‘ 𝑦 ) , 0 ) ) ) )
74 73 breq1d ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ 𝑢 ⊆ 𝐴 ) ) → ( ∫ 𝑢 ( abs ‘ 𝐵 ) d 𝑥 < 𝐶 ↔ ( ∫2 ‘ ( 𝑦 ∈ ℝ ↦ if ( 𝑦 ∈ 𝑢 , ( ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , ( abs ‘ 𝐵 ) , 0 ) ) ‘ 𝑦 ) , 0 ) ) ) < 𝐶 ) )
75 74 biimprd ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ 𝑢 ⊆ 𝐴 ) ) → ( ( ∫2 ‘ ( 𝑦 ∈ ℝ ↦ if ( 𝑦 ∈ 𝑢 , ( ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , ( abs ‘ 𝐵 ) , 0 ) ) ‘ 𝑦 ) , 0 ) ) ) < 𝐶 → ∫ 𝑢 ( abs ‘ 𝐵 ) d 𝑥 < 𝐶 ) )
76 75 imim2d ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ 𝑢 ⊆ 𝐴 ) ) → ( ( ( vol ‘ 𝑢 ) < 𝑑 → ( ∫2 ‘ ( 𝑦 ∈ ℝ ↦ if ( 𝑦 ∈ 𝑢 , ( ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , ( abs ‘ 𝐵 ) , 0 ) ) ‘ 𝑦 ) , 0 ) ) ) < 𝐶 ) → ( ( vol ‘ 𝑢 ) < 𝑑 → ∫ 𝑢 ( abs ‘ 𝐵 ) d 𝑥 < 𝐶 ) ) )
77 76 expr ⊢ ( ( 𝜑 ∧ 𝑢 ∈ dom vol ) → ( 𝑢 ⊆ 𝐴 → ( ( ( vol ‘ 𝑢 ) < 𝑑 → ( ∫2 ‘ ( 𝑦 ∈ ℝ ↦ if ( 𝑦 ∈ 𝑢 , ( ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , ( abs ‘ 𝐵 ) , 0 ) ) ‘ 𝑦 ) , 0 ) ) ) < 𝐶 ) → ( ( vol ‘ 𝑢 ) < 𝑑 → ∫ 𝑢 ( abs ‘ 𝐵 ) d 𝑥 < 𝐶 ) ) ) )
78 77 com23 ⊢ ( ( 𝜑 ∧ 𝑢 ∈ dom vol ) → ( ( ( vol ‘ 𝑢 ) < 𝑑 → ( ∫2 ‘ ( 𝑦 ∈ ℝ ↦ if ( 𝑦 ∈ 𝑢 , ( ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , ( abs ‘ 𝐵 ) , 0 ) ) ‘ 𝑦 ) , 0 ) ) ) < 𝐶 ) → ( 𝑢 ⊆ 𝐴 → ( ( vol ‘ 𝑢 ) < 𝑑 → ∫ 𝑢 ( abs ‘ 𝐵 ) d 𝑥 < 𝐶 ) ) ) )
79 78 imp4a ⊢ ( ( 𝜑 ∧ 𝑢 ∈ dom vol ) → ( ( ( vol ‘ 𝑢 ) < 𝑑 → ( ∫2 ‘ ( 𝑦 ∈ ℝ ↦ if ( 𝑦 ∈ 𝑢 , ( ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , ( abs ‘ 𝐵 ) , 0 ) ) ‘ 𝑦 ) , 0 ) ) ) < 𝐶 ) → ( ( 𝑢 ⊆ 𝐴 ∧ ( vol ‘ 𝑢 ) < 𝑑 ) → ∫ 𝑢 ( abs ‘ 𝐵 ) d 𝑥 < 𝐶 ) ) )
80 79 ralimdva ⊢ ( 𝜑 → ( ∀ 𝑢 ∈ dom vol ( ( vol ‘ 𝑢 ) < 𝑑 → ( ∫2 ‘ ( 𝑦 ∈ ℝ ↦ if ( 𝑦 ∈ 𝑢 , ( ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , ( abs ‘ 𝐵 ) , 0 ) ) ‘ 𝑦 ) , 0 ) ) ) < 𝐶 ) → ∀ 𝑢 ∈ dom vol ( ( 𝑢 ⊆ 𝐴 ∧ ( vol ‘ 𝑢 ) < 𝑑 ) → ∫ 𝑢 ( abs ‘ 𝐵 ) d 𝑥 < 𝐶 ) ) )
81 80 reximdv ⊢ ( 𝜑 → ( ∃ 𝑑 ∈ ℝ+ ∀ 𝑢 ∈ dom vol ( ( vol ‘ 𝑢 ) < 𝑑 → ( ∫2 ‘ ( 𝑦 ∈ ℝ ↦ if ( 𝑦 ∈ 𝑢 , ( ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , ( abs ‘ 𝐵 ) , 0 ) ) ‘ 𝑦 ) , 0 ) ) ) < 𝐶 ) → ∃ 𝑑 ∈ ℝ+ ∀ 𝑢 ∈ dom vol ( ( 𝑢 ⊆ 𝐴 ∧ ( vol ‘ 𝑢 ) < 𝑑 ) → ∫ 𝑢 ( abs ‘ 𝐵 ) d 𝑥 < 𝐶 ) ) )
82 34 81 mpd ⊢ ( 𝜑 → ∃ 𝑑 ∈ ℝ+ ∀ 𝑢 ∈ dom vol ( ( 𝑢 ⊆ 𝐴 ∧ ( vol ‘ 𝑢 ) < 𝑑 ) → ∫ 𝑢 ( abs ‘ 𝐵 ) d 𝑥 < 𝐶 ) )