Metamath Proof Explorer

Theorem mbflim

Description: The pointwise limit of a sequence of measurable functions is measurable. (Contributed by Mario Carneiro, 7-Sep-2014)

Ref Expression
Hypotheses mbflim.1 ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
mbflim.2 ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
mbflim.4 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝑛 ∈ 𝑍 ↦ 𝐵 ) ⇝ 𝐶 )
mbflim.5 ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ MblFn )
mbflim.6 ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ 𝐴 ) ) → 𝐵 ∈ 𝑉 )
Assertion mbflim ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ∈ MblFn )

Proof

Step Hyp Ref Expression
1 mbflim.1 ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
2 mbflim.2 ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
3 mbflim.4 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝑛 ∈ 𝑍 ↦ 𝐵 ) ⇝ 𝐶 )
4 mbflim.5 ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ MblFn )
5 mbflim.6 ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ 𝐴 ) ) → 𝐵 ∈ 𝑉 )
6 1 fvexi ⊢ 𝑍 ∈ V
7 6 mptex ⊢ ( 𝑛 ∈ 𝑍 ↦ ( ℜ ‘ 𝐵 ) ) ∈ V
8 7 a1i ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝑛 ∈ 𝑍 ↦ ( ℜ ‘ 𝐵 ) ) ∈ V )
9 2 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝑀 ∈ ℤ )
10 5 anassrs ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ 𝑉 )
11 4 10 mbfmptcl ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ℂ )
12 11 an32s ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑛 ∈ 𝑍 ) → 𝐵 ∈ ℂ )
13 12 fmpttd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝑛 ∈ 𝑍 ↦ 𝐵 ) : 𝑍 ⟶ ℂ )
14 13 ffvelrnda ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑘 ∈ 𝑍 ) → ( ( 𝑛 ∈ 𝑍 ↦ 𝐵 ) ‘ 𝑘 ) ∈ ℂ )
15 simpr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑛 ∈ 𝑍 ) → 𝑛 ∈ 𝑍 )
16 12 recld ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑛 ∈ 𝑍 ) → ( ℜ ‘ 𝐵 ) ∈ ℝ )
17 eqid ⊢ ( 𝑛 ∈ 𝑍 ↦ ( ℜ ‘ 𝐵 ) ) = ( 𝑛 ∈ 𝑍 ↦ ( ℜ ‘ 𝐵 ) )
18 17 fvmpt2 ⊢ ( ( 𝑛 ∈ 𝑍 ∧ ( ℜ ‘ 𝐵 ) ∈ ℝ ) → ( ( 𝑛 ∈ 𝑍 ↦ ( ℜ ‘ 𝐵 ) ) ‘ 𝑛 ) = ( ℜ ‘ 𝐵 ) )
19 15 16 18 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑛 ∈ 𝑍 ) → ( ( 𝑛 ∈ 𝑍 ↦ ( ℜ ‘ 𝐵 ) ) ‘ 𝑛 ) = ( ℜ ‘ 𝐵 ) )
20 eqid ⊢ ( 𝑛 ∈ 𝑍 ↦ 𝐵 ) = ( 𝑛 ∈ 𝑍 ↦ 𝐵 )
21 20 fvmpt2 ⊢ ( ( 𝑛 ∈ 𝑍 ∧ 𝐵 ∈ ℂ ) → ( ( 𝑛 ∈ 𝑍 ↦ 𝐵 ) ‘ 𝑛 ) = 𝐵 )
22 15 12 21 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑛 ∈ 𝑍 ) → ( ( 𝑛 ∈ 𝑍 ↦ 𝐵 ) ‘ 𝑛 ) = 𝐵 )
23 22 fveq2d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑛 ∈ 𝑍 ) → ( ℜ ‘ ( ( 𝑛 ∈ 𝑍 ↦ 𝐵 ) ‘ 𝑛 ) ) = ( ℜ ‘ 𝐵 ) )
24 19 23 eqtr4d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑛 ∈ 𝑍 ) → ( ( 𝑛 ∈ 𝑍 ↦ ( ℜ ‘ 𝐵 ) ) ‘ 𝑛 ) = ( ℜ ‘ ( ( 𝑛 ∈ 𝑍 ↦ 𝐵 ) ‘ 𝑛 ) ) )
25 24 ralrimiva ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ∀ 𝑛 ∈ 𝑍 ( ( 𝑛 ∈ 𝑍 ↦ ( ℜ ‘ 𝐵 ) ) ‘ 𝑛 ) = ( ℜ ‘ ( ( 𝑛 ∈ 𝑍 ↦ 𝐵 ) ‘ 𝑛 ) ) )
26 nffvmpt1 ⊢ Ⅎ 𝑛 ( ( 𝑛 ∈ 𝑍 ↦ ( ℜ ‘ 𝐵 ) ) ‘ 𝑘 )
27 nfcv ⊢ Ⅎ 𝑛 ℜ
28 nffvmpt1 ⊢ Ⅎ 𝑛 ( ( 𝑛 ∈ 𝑍 ↦ 𝐵 ) ‘ 𝑘 )
29 27 28 nffv ⊢ Ⅎ 𝑛 ( ℜ ‘ ( ( 𝑛 ∈ 𝑍 ↦ 𝐵 ) ‘ 𝑘 ) )
30 26 29 nfeq ⊢ Ⅎ 𝑛 ( ( 𝑛 ∈ 𝑍 ↦ ( ℜ ‘ 𝐵 ) ) ‘ 𝑘 ) = ( ℜ ‘ ( ( 𝑛 ∈ 𝑍 ↦ 𝐵 ) ‘ 𝑘 ) )
31 nfv ⊢ Ⅎ 𝑘 ( ( 𝑛 ∈ 𝑍 ↦ ( ℜ ‘ 𝐵 ) ) ‘ 𝑛 ) = ( ℜ ‘ ( ( 𝑛 ∈ 𝑍 ↦ 𝐵 ) ‘ 𝑛 ) )
32 fveq2 ⊢ ( 𝑘 = 𝑛 → ( ( 𝑛 ∈ 𝑍 ↦ ( ℜ ‘ 𝐵 ) ) ‘ 𝑘 ) = ( ( 𝑛 ∈ 𝑍 ↦ ( ℜ ‘ 𝐵 ) ) ‘ 𝑛 ) )
33 2fveq3 ⊢ ( 𝑘 = 𝑛 → ( ℜ ‘ ( ( 𝑛 ∈ 𝑍 ↦ 𝐵 ) ‘ 𝑘 ) ) = ( ℜ ‘ ( ( 𝑛 ∈ 𝑍 ↦ 𝐵 ) ‘ 𝑛 ) ) )
34 32 33 eqeq12d ⊢ ( 𝑘 = 𝑛 → ( ( ( 𝑛 ∈ 𝑍 ↦ ( ℜ ‘ 𝐵 ) ) ‘ 𝑘 ) = ( ℜ ‘ ( ( 𝑛 ∈ 𝑍 ↦ 𝐵 ) ‘ 𝑘 ) ) ↔ ( ( 𝑛 ∈ 𝑍 ↦ ( ℜ ‘ 𝐵 ) ) ‘ 𝑛 ) = ( ℜ ‘ ( ( 𝑛 ∈ 𝑍 ↦ 𝐵 ) ‘ 𝑛 ) ) ) )
35 30 31 34 cbvralw ⊢ ( ∀ 𝑘 ∈ 𝑍 ( ( 𝑛 ∈ 𝑍 ↦ ( ℜ ‘ 𝐵 ) ) ‘ 𝑘 ) = ( ℜ ‘ ( ( 𝑛 ∈ 𝑍 ↦ 𝐵 ) ‘ 𝑘 ) ) ↔ ∀ 𝑛 ∈ 𝑍 ( ( 𝑛 ∈ 𝑍 ↦ ( ℜ ‘ 𝐵 ) ) ‘ 𝑛 ) = ( ℜ ‘ ( ( 𝑛 ∈ 𝑍 ↦ 𝐵 ) ‘ 𝑛 ) ) )
36 25 35 sylibr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ∀ 𝑘 ∈ 𝑍 ( ( 𝑛 ∈ 𝑍 ↦ ( ℜ ‘ 𝐵 ) ) ‘ 𝑘 ) = ( ℜ ‘ ( ( 𝑛 ∈ 𝑍 ↦ 𝐵 ) ‘ 𝑘 ) ) )
37 36 r19.21bi ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑘 ∈ 𝑍 ) → ( ( 𝑛 ∈ 𝑍 ↦ ( ℜ ‘ 𝐵 ) ) ‘ 𝑘 ) = ( ℜ ‘ ( ( 𝑛 ∈ 𝑍 ↦ 𝐵 ) ‘ 𝑘 ) ) )
38 1 3 8 9 14 37 climre ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝑛 ∈ 𝑍 ↦ ( ℜ ‘ 𝐵 ) ) ⇝ ( ℜ ‘ 𝐶 ) )
39 11 ismbfcn2 ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ MblFn ↔ ( ( 𝑥 ∈ 𝐴 ↦ ( ℜ ‘ 𝐵 ) ) ∈ MblFn ∧ ( 𝑥 ∈ 𝐴 ↦ ( ℑ ‘ 𝐵 ) ) ∈ MblFn ) ) )
40 4 39 mpbid ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → ( ( 𝑥 ∈ 𝐴 ↦ ( ℜ ‘ 𝐵 ) ) ∈ MblFn ∧ ( 𝑥 ∈ 𝐴 ↦ ( ℑ ‘ 𝐵 ) ) ∈ MblFn ) )
41 40 simpld ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → ( 𝑥 ∈ 𝐴 ↦ ( ℜ ‘ 𝐵 ) ) ∈ MblFn )
42 11 anasss ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ 𝐴 ) ) → 𝐵 ∈ ℂ )
43 42 recld ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ 𝐴 ) ) → ( ℜ ‘ 𝐵 ) ∈ ℝ )
44 1 2 38 41 43 mbflimlem ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ ( ℜ ‘ 𝐶 ) ) ∈ MblFn )
45 6 mptex ⊢ ( 𝑛 ∈ 𝑍 ↦ ( ℑ ‘ 𝐵 ) ) ∈ V
46 45 a1i ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝑛 ∈ 𝑍 ↦ ( ℑ ‘ 𝐵 ) ) ∈ V )
47 12 imcld ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑛 ∈ 𝑍 ) → ( ℑ ‘ 𝐵 ) ∈ ℝ )
48 eqid ⊢ ( 𝑛 ∈ 𝑍 ↦ ( ℑ ‘ 𝐵 ) ) = ( 𝑛 ∈ 𝑍 ↦ ( ℑ ‘ 𝐵 ) )
49 48 fvmpt2 ⊢ ( ( 𝑛 ∈ 𝑍 ∧ ( ℑ ‘ 𝐵 ) ∈ ℝ ) → ( ( 𝑛 ∈ 𝑍 ↦ ( ℑ ‘ 𝐵 ) ) ‘ 𝑛 ) = ( ℑ ‘ 𝐵 ) )
50 15 47 49 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑛 ∈ 𝑍 ) → ( ( 𝑛 ∈ 𝑍 ↦ ( ℑ ‘ 𝐵 ) ) ‘ 𝑛 ) = ( ℑ ‘ 𝐵 ) )
51 22 fveq2d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑛 ∈ 𝑍 ) → ( ℑ ‘ ( ( 𝑛 ∈ 𝑍 ↦ 𝐵 ) ‘ 𝑛 ) ) = ( ℑ ‘ 𝐵 ) )
52 50 51 eqtr4d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑛 ∈ 𝑍 ) → ( ( 𝑛 ∈ 𝑍 ↦ ( ℑ ‘ 𝐵 ) ) ‘ 𝑛 ) = ( ℑ ‘ ( ( 𝑛 ∈ 𝑍 ↦ 𝐵 ) ‘ 𝑛 ) ) )
53 52 ralrimiva ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ∀ 𝑛 ∈ 𝑍 ( ( 𝑛 ∈ 𝑍 ↦ ( ℑ ‘ 𝐵 ) ) ‘ 𝑛 ) = ( ℑ ‘ ( ( 𝑛 ∈ 𝑍 ↦ 𝐵 ) ‘ 𝑛 ) ) )
54 nffvmpt1 ⊢ Ⅎ 𝑛 ( ( 𝑛 ∈ 𝑍 ↦ ( ℑ ‘ 𝐵 ) ) ‘ 𝑘 )
55 nfcv ⊢ Ⅎ 𝑛 ℑ
56 55 28 nffv ⊢ Ⅎ 𝑛 ( ℑ ‘ ( ( 𝑛 ∈ 𝑍 ↦ 𝐵 ) ‘ 𝑘 ) )
57 54 56 nfeq ⊢ Ⅎ 𝑛 ( ( 𝑛 ∈ 𝑍 ↦ ( ℑ ‘ 𝐵 ) ) ‘ 𝑘 ) = ( ℑ ‘ ( ( 𝑛 ∈ 𝑍 ↦ 𝐵 ) ‘ 𝑘 ) )
58 nfv ⊢ Ⅎ 𝑘 ( ( 𝑛 ∈ 𝑍 ↦ ( ℑ ‘ 𝐵 ) ) ‘ 𝑛 ) = ( ℑ ‘ ( ( 𝑛 ∈ 𝑍 ↦ 𝐵 ) ‘ 𝑛 ) )
59 fveq2 ⊢ ( 𝑘 = 𝑛 → ( ( 𝑛 ∈ 𝑍 ↦ ( ℑ ‘ 𝐵 ) ) ‘ 𝑘 ) = ( ( 𝑛 ∈ 𝑍 ↦ ( ℑ ‘ 𝐵 ) ) ‘ 𝑛 ) )
60 2fveq3 ⊢ ( 𝑘 = 𝑛 → ( ℑ ‘ ( ( 𝑛 ∈ 𝑍 ↦ 𝐵 ) ‘ 𝑘 ) ) = ( ℑ ‘ ( ( 𝑛 ∈ 𝑍 ↦ 𝐵 ) ‘ 𝑛 ) ) )
61 59 60 eqeq12d ⊢ ( 𝑘 = 𝑛 → ( ( ( 𝑛 ∈ 𝑍 ↦ ( ℑ ‘ 𝐵 ) ) ‘ 𝑘 ) = ( ℑ ‘ ( ( 𝑛 ∈ 𝑍 ↦ 𝐵 ) ‘ 𝑘 ) ) ↔ ( ( 𝑛 ∈ 𝑍 ↦ ( ℑ ‘ 𝐵 ) ) ‘ 𝑛 ) = ( ℑ ‘ ( ( 𝑛 ∈ 𝑍 ↦ 𝐵 ) ‘ 𝑛 ) ) ) )
62 57 58 61 cbvralw ⊢ ( ∀ 𝑘 ∈ 𝑍 ( ( 𝑛 ∈ 𝑍 ↦ ( ℑ ‘ 𝐵 ) ) ‘ 𝑘 ) = ( ℑ ‘ ( ( 𝑛 ∈ 𝑍 ↦ 𝐵 ) ‘ 𝑘 ) ) ↔ ∀ 𝑛 ∈ 𝑍 ( ( 𝑛 ∈ 𝑍 ↦ ( ℑ ‘ 𝐵 ) ) ‘ 𝑛 ) = ( ℑ ‘ ( ( 𝑛 ∈ 𝑍 ↦ 𝐵 ) ‘ 𝑛 ) ) )
63 53 62 sylibr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ∀ 𝑘 ∈ 𝑍 ( ( 𝑛 ∈ 𝑍 ↦ ( ℑ ‘ 𝐵 ) ) ‘ 𝑘 ) = ( ℑ ‘ ( ( 𝑛 ∈ 𝑍 ↦ 𝐵 ) ‘ 𝑘 ) ) )
64 63 r19.21bi ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑘 ∈ 𝑍 ) → ( ( 𝑛 ∈ 𝑍 ↦ ( ℑ ‘ 𝐵 ) ) ‘ 𝑘 ) = ( ℑ ‘ ( ( 𝑛 ∈ 𝑍 ↦ 𝐵 ) ‘ 𝑘 ) ) )
65 1 3 46 9 14 64 climim ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝑛 ∈ 𝑍 ↦ ( ℑ ‘ 𝐵 ) ) ⇝ ( ℑ ‘ 𝐶 ) )
66 40 simprd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → ( 𝑥 ∈ 𝐴 ↦ ( ℑ ‘ 𝐵 ) ) ∈ MblFn )
67 42 imcld ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ 𝐴 ) ) → ( ℑ ‘ 𝐵 ) ∈ ℝ )
68 1 2 65 66 67 mbflimlem ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ ( ℑ ‘ 𝐶 ) ) ∈ MblFn )
69 climcl ⊢ ( ( 𝑛 ∈ 𝑍 ↦ 𝐵 ) ⇝ 𝐶 → 𝐶 ∈ ℂ )
70 3 69 syl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐶 ∈ ℂ )
71 70 ismbfcn2 ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ∈ MblFn ↔ ( ( 𝑥 ∈ 𝐴 ↦ ( ℜ ‘ 𝐶 ) ) ∈ MblFn ∧ ( 𝑥 ∈ 𝐴 ↦ ( ℑ ‘ 𝐶 ) ) ∈ MblFn ) ) )
72 44 68 71 mpbir2and ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ∈ MblFn )