Metamath Proof Explorer

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 ⊢Ⅎmφ
fnlimfvre2.m ⊢Ⅎ_mF
fnlimfvre2.n ⊢Ⅎ_xF
fnlimfvre2.z ⊢Z=ℤ≥M
fnlimfvre2.f ⊢φ∧m∈Z→F⁡m:dom⁡F⁡m⟶ℝ
fnlimfvre2.d ⊢D=x∈⋃n∈Z⋂m∈ℤ≥ndom⁡F⁡m|m∈Z⟼F⁡m⁡x∈dom⁡⇝
fnlimfvre2.g ⊢G=x∈D⟼⇝⁡m∈Z⟼F⁡m⁡x
fnlimfvre2.x ⊢φ→X∈D
Assertion fnlimfvre2 ⊢φ→G⁡X∈ℝ

Proof

Step Hyp Ref Expression
1 fnlimfvre2.p ⊢Ⅎmφ
2 fnlimfvre2.m ⊢Ⅎ_mF
3 fnlimfvre2.n ⊢Ⅎ_xF
4 fnlimfvre2.z ⊢Z=ℤ≥M
5 fnlimfvre2.f ⊢φ∧m∈Z→F⁡m:dom⁡F⁡m⟶ℝ
6 fnlimfvre2.d ⊢D=x∈⋃n∈Z⋂m∈ℤ≥ndom⁡F⁡m|m∈Z⟼F⁡m⁡x∈dom⁡⇝
7 fnlimfvre2.g ⊢G=x∈D⟼⇝⁡m∈Z⟼F⁡m⁡x
8 fnlimfvre2.x ⊢φ→X∈D
9 nfrab1 ⊢Ⅎ_xx∈⋃n∈Z⋂m∈ℤ≥ndom⁡F⁡m|m∈Z⟼F⁡m⁡x∈dom⁡⇝
10 6 9 nfcxfr ⊢Ⅎ_xD
11 nfcv ⊢Ⅎ_zD
12 nfcv ⊢Ⅎ_z⇝⁡m∈Z⟼F⁡m⁡x
13 nfcv ⊢Ⅎ_x⇝
14 nfcv ⊢Ⅎ_xZ
15 nfcv ⊢Ⅎ_xm
16 3 15 nffv ⊢Ⅎ_xF⁡m
17 nfcv ⊢Ⅎ_xz
18 16 17 nffv ⊢Ⅎ_xF⁡m⁡z
19 14 18 nfmpt ⊢Ⅎ_xm∈Z⟼F⁡m⁡z
20 13 19 nffv ⊢Ⅎ_x⇝⁡m∈Z⟼F⁡m⁡z
21 fveq2 ⊢x=z→F⁡m⁡x=F⁡m⁡z
22 21 mpteq2dv ⊢x=z→m∈Z⟼F⁡m⁡x=m∈Z⟼F⁡m⁡z
23 22 fveq2d ⊢x=z→⇝⁡m∈Z⟼F⁡m⁡x=⇝⁡m∈Z⟼F⁡m⁡z
24 10 11 12 20 23 cbvmptf ⊢x∈D⟼⇝⁡m∈Z⟼F⁡m⁡x=z∈D⟼⇝⁡m∈Z⟼F⁡m⁡z
25 7 24 eqtri ⊢G=z∈D⟼⇝⁡m∈Z⟼F⁡m⁡z
26 fveq2 ⊢X=z→F⁡m⁡X=F⁡m⁡z
27 26 mpteq2dv ⊢X=z→m∈Z⟼F⁡m⁡X=m∈Z⟼F⁡m⁡z
28 eqcom ⊢X=z↔z=X
29 28 imbi1i ⊢X=z→m∈Z⟼F⁡m⁡X=m∈Z⟼F⁡m⁡z↔z=X→m∈Z⟼F⁡m⁡X=m∈Z⟼F⁡m⁡z
30 eqcom ⊢m∈Z⟼F⁡m⁡X=m∈Z⟼F⁡m⁡z↔m∈Z⟼F⁡m⁡z=m∈Z⟼F⁡m⁡X
31 30 imbi2i ⊢z=X→m∈Z⟼F⁡m⁡X=m∈Z⟼F⁡m⁡z↔z=X→m∈Z⟼F⁡m⁡z=m∈Z⟼F⁡m⁡X
32 29 31 bitri ⊢X=z→m∈Z⟼F⁡m⁡X=m∈Z⟼F⁡m⁡z↔z=X→m∈Z⟼F⁡m⁡z=m∈Z⟼F⁡m⁡X
33 27 32 mpbi ⊢z=X→m∈Z⟼F⁡m⁡z=m∈Z⟼F⁡m⁡X
34 33 fveq2d ⊢z=X→⇝⁡m∈Z⟼F⁡m⁡z=⇝⁡m∈Z⟼F⁡m⁡X
35 fvexd ⊢φ→⇝⁡m∈Z⟼F⁡m⁡X∈V
36 25 34 8 35 fvmptd3 ⊢φ→G⁡X=⇝⁡m∈Z⟼F⁡m⁡X
37 1 2 3 4 5 6 8 fnlimfvre ⊢φ→⇝⁡m∈Z⟼F⁡m⁡X∈ℝ
38 36 37 eqeltrd ⊢φ→G⁡X∈ℝ