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	⊢ ( 𝜑 → 𝐺 : 𝐷 ⟶ ℝ )