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 ⊢φ∧x∈A→B∈V
itgcn.2 ⊢φ→x∈A⟼B∈𝐿1
itgcn.3 ⊢φ→C∈ℝ+
Assertion itgcn ⊢φ→∃d∈ℝ+∀u∈dom⁡volu⊆A∧vol⁡u<d→∫uBdx<C

Proof

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