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

Proof

Step Hyp Ref Expression
1 fnlimf.p ⊢ Ⅎ m φ
2 fnlimf.m ⊢ Ⅎ _ m F
3 fnlimf.n ⊢ Ⅎ _ x F
4 fnlimf.z ⊢ Z = ℤ ≥ M
5 fnlimf.f ⊢ φ ∧ m ∈ Z → F ⁡ m : dom ⁡ F ⁡ m ⟶ ℝ
6 fnlimf.d ⊢ D = x ∈ ⋃ n ∈ Z ⋂ m ∈ ℤ ≥ n dom ⁡ F ⁡ m | m ∈ Z ⟼ F ⁡ m ⁡ x ∈ dom ⁡ ⇝
7 fnlimf.g ⊢ G = x ∈ D ⟼ ⇝ ⁡ m ∈ Z ⟼ F ⁡ m ⁡ x
8 nfv ⊢ Ⅎ m z ∈ D
9 1 8 nfan ⊢ Ⅎ m φ ∧ z ∈ D
10 5 adantlr ⊢ φ ∧ z ∈ D ∧ m ∈ Z → F ⁡ m : dom ⁡ F ⁡ m ⟶ ℝ
11 simpr ⊢ φ ∧ z ∈ D → z ∈ D
12 9 2 3 4 10 6 11 fnlimfvre ⊢ φ ∧ z ∈ D → ⇝ ⁡ m ∈ Z ⟼ F ⁡ m ⁡ z ∈ ℝ
13 nfrab1 ⊢ Ⅎ _ x x ∈ ⋃ n ∈ Z ⋂ m ∈ ℤ ≥ n dom ⁡ F ⁡ m | m ∈ Z ⟼ F ⁡ m ⁡ x ∈ dom ⁡ ⇝
14 6 13 nfcxfr ⊢ Ⅎ _ x D
15 nfcv ⊢ Ⅎ _ z D
16 nfcv ⊢ Ⅎ _ z ⇝ ⁡ m ∈ Z ⟼ F ⁡ m ⁡ x
17 nfcv ⊢ Ⅎ _ x ⇝
18 nfcv ⊢ Ⅎ _ x Z
19 nfcv ⊢ Ⅎ _ x m
20 3 19 nffv ⊢ Ⅎ _ x F ⁡ m
21 nfcv ⊢ Ⅎ _ x z
22 20 21 nffv ⊢ Ⅎ _ x F ⁡ m ⁡ z
23 18 22 nfmpt ⊢ Ⅎ _ x m ∈ Z ⟼ F ⁡ m ⁡ z
24 17 23 nffv ⊢ Ⅎ _ x ⇝ ⁡ m ∈ Z ⟼ F ⁡ m ⁡ z
25 fveq2 ⊢ x = z → F ⁡ m ⁡ x = F ⁡ m ⁡ z
26 25 mpteq2dv ⊢ x = z → m ∈ Z ⟼ F ⁡ m ⁡ x = m ∈ Z ⟼ F ⁡ m ⁡ z
27 26 fveq2d ⊢ x = z → ⇝ ⁡ m ∈ Z ⟼ F ⁡ m ⁡ x = ⇝ ⁡ m ∈ Z ⟼ F ⁡ m ⁡ z
28 14 15 16 24 27 cbvmptf ⊢ x ∈ D ⟼ ⇝ ⁡ m ∈ Z ⟼ F ⁡ m ⁡ x = z ∈ D ⟼ ⇝ ⁡ m ∈ Z ⟼ F ⁡ m ⁡ z
29 7 28 eqtri ⊢ G = z ∈ D ⟼ ⇝ ⁡ m ∈ Z ⟼ F ⁡ m ⁡ z
30 12 29 fmptd ⊢ φ → G : D ⟶ ℝ