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	$⊢ \underline{Ⅎ} x F$
	fnlimcnv.2	$⊢ D = \{x \in ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} dom F (m) \| (m \in Z ⟼ F (m) (x)) \in dom ⇝\}$
	fnlimcnv.3	$⊢ G = (x \in D ⟼ ⇝ ((m \in Z ⟼ F (m) (x))))$
	fnlimcnv.4	$⊢ φ \to X \in D$
Assertion	fnlimcnv	$⊢ φ \to (m \in Z ⟼ F (m) (X)) ⇝ G (X)$

Proof

Step	Hyp	Ref	Expression
1		fnlimcnv.1	$⊢ \underline{Ⅎ} x F$
2		fnlimcnv.2	$⊢ D = \{x \in ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} dom F (m) \| (m \in Z ⟼ F (m) (x)) \in dom ⇝\}$
3		fnlimcnv.3	$⊢ G = (x \in D ⟼ ⇝ ((m \in Z ⟼ F (m) (x))))$
4		fnlimcnv.4	$⊢ φ \to X \in D$
5		fveq2	$⊢ y = X \to F (m) (y) = F (m) (X)$
6	5	mpteq2dv	$⊢ y = X \to (m \in Z ⟼ F (m) (y)) = (m \in Z ⟼ F (m) (X))$
7	6	eleq1d	$⊢ y = X \to ((m \in Z ⟼ F (m) (y)) \in dom ⇝ \leftrightarrow (m \in Z ⟼ F (m) (X)) \in dom ⇝)$
8		nfcv	$⊢ \underline{Ⅎ} x Z$
9		nfcv	$⊢ \underline{Ⅎ} x ℤ_{\geq n}$
10		nfcv	$⊢ \underline{Ⅎ} x m$
11	1 10	nffv	$⊢ \underline{Ⅎ} x F (m)$
12	11	nfdm	$⊢ \underline{Ⅎ} x dom F (m)$
13	9 12	nfiin	$⊢ \underline{Ⅎ} x ⋂_{m \in ℤ_{\geq n}} dom F (m)$
14	8 13	nfiun	$⊢ \underline{Ⅎ} x ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} dom F (m)$
15		nfcv	$⊢ \underline{Ⅎ} y ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} dom F (m)$
16		nfv	$⊢ Ⅎ y (m \in Z ⟼ F (m) (x)) \in dom ⇝$
17		nfcv	$⊢ \underline{Ⅎ} x y$
18	11 17	nffv	$⊢ \underline{Ⅎ} x F (m) (y)$
19	8 18	nfmpt	$⊢ \underline{Ⅎ} x (m \in Z ⟼ F (m) (y))$
20		nfcv	$⊢ \underline{Ⅎ} x dom ⇝$
21	19 20	nfel	$⊢ Ⅎ x (m \in Z ⟼ F (m) (y)) \in dom ⇝$
22		fveq2	$⊢ x = y \to F (m) (x) = F (m) (y)$
23	22	mpteq2dv	$⊢ x = y \to (m \in Z ⟼ F (m) (x)) = (m \in Z ⟼ F (m) (y))$
24	23	eleq1d	$⊢ x = y \to ((m \in Z ⟼ F (m) (x)) \in dom ⇝ \leftrightarrow (m \in Z ⟼ F (m) (y)) \in dom ⇝)$
25	14 15 16 21 24	cbvrabw	$⊢ \{x \in ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} dom F (m) \| (m \in Z ⟼ F (m) (x)) \in dom ⇝\} = \{y \in ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} dom F (m) \| (m \in Z ⟼ F (m) (y)) \in dom ⇝\}$
26	2 25	eqtri	$⊢ D = \{y \in ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} dom F (m) \| (m \in Z ⟼ F (m) (y)) \in dom ⇝\}$
27	7 26	elrab2	$⊢ X \in D \leftrightarrow (X \in ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} dom F (m) \land (m \in Z ⟼ F (m) (X)) \in dom ⇝)$
28	4 27	sylib	$⊢ φ \to (X \in ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} dom F (m) \land (m \in Z ⟼ F (m) (X)) \in dom ⇝)$
29	28	simprd	$⊢ φ \to (m \in Z ⟼ F (m) (X)) \in dom ⇝$
30		climdm	$⊢ (m \in Z ⟼ F (m) (X)) \in dom ⇝ \leftrightarrow (m \in Z ⟼ F (m) (X)) ⇝ ⇝ ((m \in Z ⟼ F (m) (X)))$
31	29 30	sylib	$⊢ φ \to (m \in Z ⟼ F (m) (X)) ⇝ ⇝ ((m \in Z ⟼ F (m) (X)))$
32		nfrab1	$⊢ \underline{Ⅎ} x \{x \in ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} dom F (m) \| (m \in Z ⟼ F (m) (x)) \in dom ⇝\}$
33	2 32	nfcxfr	$⊢ \underline{Ⅎ} x D$
34	33 1 3 4	fnlimfv	$⊢ φ \to G (X) = ⇝ ((m \in Z ⟼ F (m) (X)))$
35	34	eqcomd	$⊢ φ \to ⇝ ((m \in Z ⟼ F (m) (X))) = G (X)$
36	31 35	breqtrd	$⊢ φ \to (m \in Z ⟼ F (m) (X)) ⇝ G (X)$

Metamath Proof Explorer

Theorem fnlimcnv

Proof