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 )