Theorem fnlimfvre2

Description: The limit function of real functions, applied to elements in its domain, evaluates to Real values. (Contributed by Glauco Siliprandi, 26-Jun-2021)

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

Proof

Step	Hyp	Ref	Expression
1		fnlimfvre2.p	⊢ Ⅎ 𝑚 𝜑
2		fnlimfvre2.m	⊢ Ⅎ 𝑚 𝐹
3		fnlimfvre2.n	⊢ Ⅎ 𝑥 𝐹
4		fnlimfvre2.z	⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
5		fnlimfvre2.f	⊢ ( ( 𝜑 ∧ 𝑚 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑚 ) : dom ( 𝐹 ‘ 𝑚 ) ⟶ ℝ )
6		fnlimfvre2.d	⊢ 𝐷 = { 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ∣ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ∈ dom ⇝ }
7		fnlimfvre2.g	⊢ 𝐺 = ( 𝑥 ∈ 𝐷 ↦ ( ⇝ ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ) )
8		fnlimfvre2.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐷 )
9		nfrab1	⊢ Ⅎ 𝑥 { 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ ( ℤ≥ ‘ 𝑛 ) dom ( 𝐹 ‘ 𝑚 ) ∣ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ∈ dom ⇝ }
10	6 9	nfcxfr	⊢ Ⅎ 𝑥 𝐷
11		nfcv	⊢ Ⅎ 𝑧 𝐷
12		nfcv	⊢ Ⅎ 𝑧 ( ⇝ ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) )
13		nfcv	⊢ Ⅎ 𝑥 ⇝
14		nfcv	⊢ Ⅎ 𝑥 𝑍
15		nfcv	⊢ Ⅎ 𝑥 𝑚
16	3 15	nffv	⊢ Ⅎ 𝑥 ( 𝐹 ‘ 𝑚 )
17		nfcv	⊢ Ⅎ 𝑥 𝑧
18	16 17	nffv	⊢ Ⅎ 𝑥 ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑧 )
19	14 18	nfmpt	⊢ Ⅎ 𝑥 ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑧 ) )
20	13 19	nffv	⊢ Ⅎ 𝑥 ( ⇝ ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑧 ) ) )
21		fveq2	⊢ ( 𝑥 = 𝑧 → ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) = ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑧 ) )
22	21	mpteq2dv	⊢ ( 𝑥 = 𝑧 → ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) = ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑧 ) ) )
23	22	fveq2d	⊢ ( 𝑥 = 𝑧 → ( ⇝ ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ) = ( ⇝ ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑧 ) ) ) )
24	10 11 12 20 23	cbvmptf	⊢ ( 𝑥 ∈ 𝐷 ↦ ( ⇝ ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑥 ) ) ) ) = ( 𝑧 ∈ 𝐷 ↦ ( ⇝ ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑧 ) ) ) )
25	7 24	eqtri	⊢ 𝐺 = ( 𝑧 ∈ 𝐷 ↦ ( ⇝ ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑧 ) ) ) )
26		fveq2	⊢ ( 𝑋 = 𝑧 → ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑋 ) = ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑧 ) )
27	26	mpteq2dv	⊢ ( 𝑋 = 𝑧 → ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑋 ) ) = ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑧 ) ) )
28		eqcom	⊢ ( 𝑋 = 𝑧 ↔ 𝑧 = 𝑋 )
29	28	imbi1i	⊢ ( ( 𝑋 = 𝑧 → ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑋 ) ) = ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑧 ) ) ) ↔ ( 𝑧 = 𝑋 → ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑋 ) ) = ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑧 ) ) ) )
30		eqcom	⊢ ( ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑋 ) ) = ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑧 ) ) ↔ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑧 ) ) = ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑋 ) ) )
31	30	imbi2i	⊢ ( ( 𝑧 = 𝑋 → ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑋 ) ) = ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑧 ) ) ) ↔ ( 𝑧 = 𝑋 → ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑧 ) ) = ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑋 ) ) ) )
32	29 31	bitri	⊢ ( ( 𝑋 = 𝑧 → ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑋 ) ) = ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑧 ) ) ) ↔ ( 𝑧 = 𝑋 → ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑧 ) ) = ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑋 ) ) ) )
33	27 32	mpbi	⊢ ( 𝑧 = 𝑋 → ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑧 ) ) = ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑋 ) ) )
34	33	fveq2d	⊢ ( 𝑧 = 𝑋 → ( ⇝ ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑧 ) ) ) = ( ⇝ ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑋 ) ) ) )
35		fvexd	⊢ ( 𝜑 → ( ⇝ ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑋 ) ) ) ∈ V )
36	25 34 8 35	fvmptd3	⊢ ( 𝜑 → ( 𝐺 ‘ 𝑋 ) = ( ⇝ ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑋 ) ) ) )
37	1 2 3 4 5 6 8	fnlimfvre	⊢ ( 𝜑 → ( ⇝ ‘ ( 𝑚 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑚 ) ‘ 𝑋 ) ) ) ∈ ℝ )
38	36 37	eqeltrd	⊢ ( 𝜑 → ( 𝐺 ‘ 𝑋 ) ∈ ℝ )