Theorem fnlimcnv

Description: The sequence of function values converges to the value of the limit function G at any point of its domain D . (Contributed by Glauco Siliprandi, 26-Jun-2021)

	Ref	Expression
Hypotheses	fnlimcnv.1	⊢ Ⅎ 𝑥 𝐹
	fnlimcnv.2	⊢ 𝐷 = { 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ∣ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ∈ dom ⇝ }
	fnlimcnv.3	⊢ 𝐺 = ( 𝑥 ∈ 𝐷 ↦ ( ⇝ ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ) )
	fnlimcnv.4	⊢ ( 𝜑 → 𝑋 ∈ 𝐷 )
Assertion	fnlimcnv	⊢ ( 𝜑 → ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑋 ) ) ⇝ ( 𝐺 ‘ 𝑋 ) )

Proof

Step	Hyp	Ref	Expression
1		fnlimcnv.1	⊢ Ⅎ 𝑥 𝐹
2		fnlimcnv.2	⊢ 𝐷 = { 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ∣ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ∈ dom ⇝ }
3		fnlimcnv.3	⊢ 𝐺 = ( 𝑥 ∈ 𝐷 ↦ ( ⇝ ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ) )
4		fnlimcnv.4	⊢ ( 𝜑 → 𝑋 ∈ 𝐷 )
5		fveq2	⊢ ( 𝑦 = 𝑋 → ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑦 ) = ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑋 ) )
6	5	mpteq2dv	⊢ ( 𝑦 = 𝑋 → ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑦 ) ) = ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑋 ) ) )
7	6	eleq1d	⊢ ( 𝑦 = 𝑋 → ( ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑦 ) ) ∈ dom ⇝ ↔ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑋 ) ) ∈ dom ⇝ ) )
8		nfcv	⊢ Ⅎ 𝑥 𝑍
9		nfcv	⊢ Ⅎ 𝑥 ( ℤ≥ ‘ 𝑛 )
10		nfcv	⊢ Ⅎ 𝑥 𝑚
11	1 10	nffv	⊢ Ⅎ 𝑥 ( 𝐹 ‘ 𝑚 )
12	11	nfdm	⊢ Ⅎ 𝑥 dom ( 𝐹 ‘ 𝑚 )
13	9 12	nfiin	⊢ Ⅎ 𝑥 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 )
14	8 13	nfiun	⊢ Ⅎ 𝑥 ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 )
15		nfcv	⊢ Ⅎ 𝑦 ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 )
16		nfv	⊢ Ⅎ 𝑦 ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ∈ dom ⇝
17		nfcv	⊢ Ⅎ 𝑥 𝑦
18	11 17	nffv	⊢ Ⅎ 𝑥 ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑦 )
19	8 18	nfmpt	⊢ Ⅎ 𝑥 ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑦 ) )
20		nfcv	⊢ Ⅎ 𝑥 dom ⇝
21	19 20	nfel	⊢ Ⅎ 𝑥 ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑦 ) ) ∈ dom ⇝
22		fveq2	⊢ ( 𝑥 = 𝑦 → ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) = ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑦 ) )
23	22	mpteq2dv	⊢ ( 𝑥 = 𝑦 → ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) = ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑦 ) ) )
24	23	eleq1d	⊢ ( 𝑥 = 𝑦 → ( ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ∈ dom ⇝ ↔ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑦 ) ) ∈ dom ⇝ ) )
25	14 15 16 21 24	cbvrabw	⊢ { 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ∣ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ∈ dom ⇝ } = { 𝑦 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ∣ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑦 ) ) ∈ dom ⇝ }
26	2 25	eqtri	⊢ 𝐷 = { 𝑦 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ∣ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑦 ) ) ∈ dom ⇝ }
27	7 26	elrab2	⊢ ( 𝑋 ∈ 𝐷 ↔ ( 𝑋 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ∧ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑋 ) ) ∈ dom ⇝ ) )
28	4 27	sylib	⊢ ( 𝜑 → ( 𝑋 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ∧ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑋 ) ) ∈ dom ⇝ ) )
29	28	simprd	⊢ ( 𝜑 → ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑋 ) ) ∈ dom ⇝ )
30		climdm	⊢ ( ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑋 ) ) ∈ dom ⇝ ↔ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑋 ) ) ⇝ ( ⇝ ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑋 ) ) ) )
31	29 30	sylib	⊢ ( 𝜑 → ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑋 ) ) ⇝ ( ⇝ ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑋 ) ) ) )
32		nfrab1	⊢ Ⅎ 𝑥 { 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ∣ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ∈ dom ⇝ }
33	2 32	nfcxfr	⊢ Ⅎ 𝑥 𝐷
34	33 1 3 4	fnlimfv	⊢ ( 𝜑 → ( 𝐺 ‘ 𝑋 ) = ( ⇝ ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑋 ) ) ) )
35	34	eqcomd	⊢ ( 𝜑 → ( ⇝ ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑋 ) ) ) = ( 𝐺 ‘ 𝑋 ) )
36	31 35	breqtrd	⊢ ( 𝜑 → ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑋 ) ) ⇝ ( 𝐺 ‘ 𝑋 ) )