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

Metamath Proof Explorer

Theorem fnlimf

Description: The limit function of real functions, is a real-valued function. (Contributed by Glauco Siliprandi, 26-Jun-2021)

Ref Expression
Hypotheses fnlimf.p ⊢ Ⅎ 𝑚 𝜑
fnlimf.m ⊢ Ⅎ 𝑚 𝐹
fnlimf.n ⊢ Ⅎ 𝑥 𝐹
fnlimf.z ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
fnlimf.f ⊢ ( ( 𝜑 ∧ 𝑚 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑚 ) : dom ( 𝐹 ‘ 𝑚 ) ⟶ ℝ )
fnlimf.d ⊢ 𝐷 = { 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ∣ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ∈ dom ⇝ }
fnlimf.g ⊢ 𝐺 = ( 𝑥 ∈ 𝐷 ↦ ( ⇝ ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ) )
Assertion fnlimf ( 𝜑 → 𝐺 : 𝐷 ⟶ ℝ )

Proof

Step Hyp Ref Expression
1 fnlimf.p ⊢ Ⅎ 𝑚 𝜑
2 fnlimf.m ⊢ Ⅎ 𝑚 𝐹
3 fnlimf.n ⊢ Ⅎ 𝑥 𝐹
4 fnlimf.z ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
5 fnlimf.f ⊢ ( ( 𝜑 ∧ 𝑚 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑚 ) : dom ( 𝐹 ‘ 𝑚 ) ⟶ ℝ )
6 fnlimf.d ⊢ 𝐷 = { 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ∣ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ∈ dom ⇝ }
7 fnlimf.g ⊢ 𝐺 = ( 𝑥 ∈ 𝐷 ↦ ( ⇝ ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ) )
8 nfv ⊢ Ⅎ 𝑚 𝑧 ∈ 𝐷
9 1 8 nfan ⊢ Ⅎ 𝑚 ( 𝜑 ∧ 𝑧 ∈ 𝐷 )
10 5 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐷 ) ∧ 𝑚 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑚 ) : dom ( 𝐹 ‘ 𝑚 ) ⟶ ℝ )
11 simpr ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐷 ) → 𝑧 ∈ 𝐷 )
12 9 2 3 4 10 6 11 fnlimfvre ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐷 ) → ( ⇝ ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑧 ) ) ) ∈ ℝ )
13 nfrab1 ⊢ Ⅎ 𝑥 { 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ∣ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ∈ dom ⇝ }
14 6 13 nfcxfr ⊢ Ⅎ 𝑥 𝐷
15 nfcv ⊢ Ⅎ 𝑧 𝐷
16 nfcv ⊢ Ⅎ 𝑧 ( ⇝ ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) )
17 nfcv ⊢ Ⅎ 𝑥 ⇝
18 nfcv ⊢ Ⅎ 𝑥 𝑍
19 nfcv ⊢ Ⅎ 𝑥 𝑚
20 3 19 nffv ⊢ Ⅎ 𝑥 ( 𝐹 ‘ 𝑚 )
21 nfcv ⊢ Ⅎ 𝑥 𝑧
22 20 21 nffv ⊢ Ⅎ 𝑥 ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑧 )
23 18 22 nfmpt ⊢ Ⅎ 𝑥 ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑧 ) )
24 17 23 nffv ⊢ Ⅎ 𝑥 ( ⇝ ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑧 ) ) )
25 fveq2 ⊢ ( 𝑥 = 𝑧 → ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) = ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑧 ) )
26 25 mpteq2dv ⊢ ( 𝑥 = 𝑧 → ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) = ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑧 ) ) )
27 26 fveq2d ⊢ ( 𝑥 = 𝑧 → ( ⇝ ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ) = ( ⇝ ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑧 ) ) ) )
28 14 15 16 24 27 cbvmptf ⊢ ( 𝑥 ∈ 𝐷 ↦ ( ⇝ ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ) ) = ( 𝑧 ∈ 𝐷 ↦ ( ⇝ ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑧 ) ) ) )
29 7 28 eqtri ⊢ 𝐺 = ( 𝑧 ∈ 𝐷 ↦ ( ⇝ ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑧 ) ) ) )
30 12 29 fmptd ⊢ ( 𝜑 → 𝐺 : 𝐷 ⟶ ℝ )