fnlimfvre

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	fnlimfvre.p	$⊢ Ⅎ m φ$
	fnlimfvre.m	$⊢ \underline{Ⅎ} m F$
	fnlimfvre.n	$⊢ \underline{Ⅎ} x F$
	fnlimfvre.z	$⊢ Z = ℤ_{\geq M}$
	fnlimfvre.f	$⊢ (φ \land m \in Z) \to F (m) : dom F (m) ⟶ ℝ$
	fnlimfvre.d	$⊢ D = \{x \in ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} dom F (m) \| (m \in Z ⟼ F (m) (x)) \in dom ⇝\}$
	fnlimfvre.x	$⊢ φ \to X \in D$
Assertion	fnlimfvre	$⊢ φ \to ⇝ ((m \in Z ⟼ F (m) (X))) \in ℝ$

Proof

Step	Hyp	Ref	Expression
1		fnlimfvre.p	$⊢ Ⅎ m φ$
2		fnlimfvre.m	$⊢ \underline{Ⅎ} m F$
3		fnlimfvre.n	$⊢ \underline{Ⅎ} x F$
4		fnlimfvre.z	$⊢ Z = ℤ_{\geq M}$
5		fnlimfvre.f	$⊢ (φ \land m \in Z) \to F (m) : dom F (m) ⟶ ℝ$
6		fnlimfvre.d	$⊢ D = \{x \in ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} dom F (m) \| (m \in Z ⟼ F (m) (x)) \in dom ⇝\}$
7		fnlimfvre.x	$⊢ φ \to X \in D$
8		nfcv	$⊢ \underline{Ⅎ} x Z$
9		nfcv	$⊢ \underline{Ⅎ} x ℤ_{\geq n}$
10		nfcv	$⊢ \underline{Ⅎ} x m$
11	3 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	14	ssrab2f	$⊢ \{x \in ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} dom F (m) \| (m \in Z ⟼ F (m) (x)) \in dom ⇝\} \subseteq ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} dom F (m)$
16	6 15	eqsstri	$⊢ D \subseteq ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} dom F (m)$
17	16	sseli	$⊢ X \in D \to X \in ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} dom F (m)$
18		eliun	$⊢ X \in ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} dom F (m) \leftrightarrow \exists n \in Z X \in ⋂_{m \in ℤ_{\geq n}} dom F (m)$
19	17 18	sylib	$⊢ X \in D \to \exists n \in Z X \in ⋂_{m \in ℤ_{\geq n}} dom F (m)$
20	7 19	syl	$⊢ φ \to \exists n \in Z X \in ⋂_{m \in ℤ_{\geq n}} dom F (m)$
21		nfv	$⊢ Ⅎ n φ$
22		nfv	$⊢ Ⅎ n ⇝ ((m \in Z ⟼ F (m) (X))) \in ℝ$
23		nfv	$⊢ Ⅎ m n \in Z$
24		nfcv	$⊢ \underline{Ⅎ} m X$
25		nfii1	$⊢ \underline{Ⅎ} m ⋂_{m \in ℤ_{\geq n}} dom F (m)$
26	24 25	nfel	$⊢ Ⅎ m X \in ⋂_{m \in ℤ_{\geq n}} dom F (m)$
27	1 23 26	nf3an	$⊢ Ⅎ m (φ \land n \in Z \land X \in ⋂_{m \in ℤ_{\geq n}} dom F (m))$
28		uzssz	$⊢ ℤ_{\geq M} \subseteq ℤ$
29	4	eleq2i	$⊢ n \in Z \leftrightarrow n \in ℤ_{\geq M}$
30	29	biimpi	$⊢ n \in Z \to n \in ℤ_{\geq M}$
31	28 30	sseldi	$⊢ n \in Z \to n \in ℤ$
32	31	3ad2ant2	$⊢ (φ \land n \in Z \land X \in ⋂_{m \in ℤ_{\geq n}} dom F (m)) \to n \in ℤ$
33		eqid	$⊢ ℤ_{\geq n} = ℤ_{\geq n}$
34	4	fvexi	$⊢ Z \in V$
35	34	a1i	$⊢ (φ \land n \in Z \land X \in ⋂_{m \in ℤ_{\geq n}} dom F (m)) \to Z \in V$
36	4	uztrn2	$⊢ (n \in Z \land j \in ℤ_{\geq n}) \to j \in Z$
37	36	ssd	$⊢ n \in Z \to ℤ_{\geq n} \subseteq Z$
38	37	3ad2ant2	$⊢ (φ \land n \in Z \land X \in ⋂_{m \in ℤ_{\geq n}} dom F (m)) \to ℤ_{\geq n} \subseteq Z$
39		fvexd	$⊢ ((φ \land n \in Z \land X \in ⋂_{m \in ℤ_{\geq n}} dom F (m)) \land m \in Z) \to F (m) (X) \in V$
40		fvexd	$⊢ (φ \land n \in Z \land X \in ⋂_{m \in ℤ_{\geq n}} dom F (m)) \to ℤ_{\geq n} \in V$
41		ssidd	$⊢ (φ \land n \in Z \land X \in ⋂_{m \in ℤ_{\geq n}} dom F (m)) \to ℤ_{\geq n} \subseteq ℤ_{\geq n}$
42		fvexd	$⊢ ((φ \land n \in Z \land X \in ⋂_{m \in ℤ_{\geq n}} dom F (m)) \land m \in ℤ_{\geq n}) \to F (m) (X) \in V$
43		eqidd	$⊢ ((φ \land n \in Z \land X \in ⋂_{m \in ℤ_{\geq n}} dom F (m)) \land m \in ℤ_{\geq n}) \to F (m) (X) = F (m) (X)$
44	27 32 33 35 38 39 40 41 42 43	climfveqmpt	$⊢ (φ \land n \in Z \land X \in ⋂_{m \in ℤ_{\geq n}} dom F (m)) \to ⇝ ((m \in Z ⟼ F (m) (X))) = ⇝ ((m \in ℤ_{\geq n} ⟼ F (m) (X)))$
45	6	eleq2i	$⊢ X \in D \leftrightarrow X \in \{x \in ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} dom F (m) \| (m \in Z ⟼ F (m) (x)) \in dom ⇝\}$
46	45	biimpi	$⊢ X \in D \to X \in \{x \in ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} dom F (m) \| (m \in Z ⟼ F (m) (x)) \in dom ⇝\}$
47		nfcv	$⊢ \underline{Ⅎ} x X$
48	11 47	nffv	$⊢ \underline{Ⅎ} x F (m) (X)$
49	8 48	nfmpt	$⊢ \underline{Ⅎ} x (m \in Z ⟼ F (m) (X))$
50		nfcv	$⊢ \underline{Ⅎ} x dom ⇝$
51	49 50	nfel	$⊢ Ⅎ x (m \in Z ⟼ F (m) (X)) \in dom ⇝$
52		fveq2	$⊢ x = X \to F (m) (x) = F (m) (X)$
53	52	mpteq2dv	$⊢ x = X \to (m \in Z ⟼ F (m) (x)) = (m \in Z ⟼ F (m) (X))$
54	53	eleq1d	$⊢ x = X \to ((m \in Z ⟼ F (m) (x)) \in dom ⇝ \leftrightarrow (m \in Z ⟼ F (m) (X)) \in dom ⇝)$
55	47 14 51 54	elrabf	$⊢ X \in \{x \in ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} dom F (m) \| (m \in Z ⟼ F (m) (x)) \in dom ⇝\} \leftrightarrow (X \in ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} dom F (m) \land (m \in Z ⟼ F (m) (X)) \in dom ⇝)$
56	55	biimpi	$⊢ X \in \{x \in ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} dom F (m) \| (m \in Z ⟼ F (m) (x)) \in dom ⇝\} \to (X \in ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} dom F (m) \land (m \in Z ⟼ F (m) (X)) \in dom ⇝)$
57	56	simprd	$⊢ X \in \{x \in ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} dom F (m) \| (m \in Z ⟼ F (m) (x)) \in dom ⇝\} \to (m \in Z ⟼ F (m) (X)) \in dom ⇝$
58	46 57	syl	$⊢ X \in D \to (m \in Z ⟼ F (m) (X)) \in dom ⇝$
59	58	adantr	$⊢ (X \in D \land n \in Z) \to (m \in Z ⟼ F (m) (X)) \in dom ⇝$
60		nfmpt1	$⊢ \underline{Ⅎ} m (m \in Z ⟼ F (m) (x))$
61		nfcv	$⊢ \underline{Ⅎ} m dom ⇝$
62	60 61	nfel	$⊢ Ⅎ m (m \in Z ⟼ F (m) (x)) \in dom ⇝$
63		nfv	$⊢ Ⅎ m j \in Z$
64	63	nfci	$⊢ \underline{Ⅎ} m Z$
65	64 25	nfiun	$⊢ \underline{Ⅎ} m ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} dom F (m)$
66	62 65	nfrabw	$⊢ \underline{Ⅎ} m \{x \in ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} dom F (m) \| (m \in Z ⟼ F (m) (x)) \in dom ⇝\}$
67	6 66	nfcxfr	$⊢ \underline{Ⅎ} m D$
68	24 67	nfel	$⊢ Ⅎ m X \in D$
69	68 23	nfan	$⊢ Ⅎ m (X \in D \land n \in Z)$
70	31	adantl	$⊢ (X \in D \land n \in Z) \to n \in ℤ$
71	34	a1i	$⊢ (X \in D \land n \in Z) \to Z \in V$
72	37	adantl	$⊢ (X \in D \land n \in Z) \to ℤ_{\geq n} \subseteq Z$
73		fvexd	$⊢ ((X \in D \land n \in Z) \land m \in Z) \to F (m) (X) \in V$
74		fvexd	$⊢ (X \in D \land n \in Z) \to ℤ_{\geq n} \in V$
75		ssidd	$⊢ (X \in D \land n \in Z) \to ℤ_{\geq n} \subseteq ℤ_{\geq n}$
76		fvexd	$⊢ ((X \in D \land n \in Z) \land m \in ℤ_{\geq n}) \to F (m) (X) \in V$
77		eqidd	$⊢ ((X \in D \land n \in Z) \land m \in ℤ_{\geq n}) \to F (m) (X) = F (m) (X)$
78	69 70 33 71 72 73 74 75 76 77	climeldmeqmpt	$⊢ (X \in D \land n \in Z) \to ((m \in Z ⟼ F (m) (X)) \in dom ⇝ \leftrightarrow (m \in ℤ_{\geq n} ⟼ F (m) (X)) \in dom ⇝)$
79	59 78	mpbid	$⊢ (X \in D \land n \in Z) \to (m \in ℤ_{\geq n} ⟼ F (m) (X)) \in dom ⇝$
80		climdm	$⊢ (m \in ℤ_{\geq n} ⟼ F (m) (X)) \in dom ⇝ \leftrightarrow (m \in ℤ_{\geq n} ⟼ F (m) (X)) ⇝ ⇝ ((m \in ℤ_{\geq n} ⟼ F (m) (X)))$
81	79 80	sylib	$⊢ (X \in D \land n \in Z) \to (m \in ℤ_{\geq n} ⟼ F (m) (X)) ⇝ ⇝ ((m \in ℤ_{\geq n} ⟼ F (m) (X)))$
82	7 81	sylan	$⊢ (φ \land n \in Z) \to (m \in ℤ_{\geq n} ⟼ F (m) (X)) ⇝ ⇝ ((m \in ℤ_{\geq n} ⟼ F (m) (X)))$
83	82	3adant3	$⊢ (φ \land n \in Z \land X \in ⋂_{m \in ℤ_{\geq n}} dom F (m)) \to (m \in ℤ_{\geq n} ⟼ F (m) (X)) ⇝ ⇝ ((m \in ℤ_{\geq n} ⟼ F (m) (X)))$
84		simpl1	$⊢ ((φ \land n \in Z \land X \in ⋂_{m \in ℤ_{\geq n}} dom F (m)) \land j \in ℤ_{\geq n}) \to φ$
85		simpl2	$⊢ ((φ \land n \in Z \land X \in ⋂_{m \in ℤ_{\geq n}} dom F (m)) \land j \in ℤ_{\geq n}) \to n \in Z$
86		nfcv	$⊢ \underline{Ⅎ} j dom F (m)$
87		nfcv	$⊢ \underline{Ⅎ} m j$
88	2 87	nffv	$⊢ \underline{Ⅎ} m F (j)$
89	88	nfdm	$⊢ \underline{Ⅎ} m dom F (j)$
90		fveq2	$⊢ m = j \to F (m) = F (j)$
91	90	dmeqd	$⊢ m = j \to dom F (m) = dom F (j)$
92	86 89 91	cbviin	$⊢ ⋂_{m \in ℤ_{\geq n}} dom F (m) = ⋂_{j \in ℤ_{\geq n}} dom F (j)$
93	92	eleq2i	$⊢ X \in ⋂_{m \in ℤ_{\geq n}} dom F (m) \leftrightarrow X \in ⋂_{j \in ℤ_{\geq n}} dom F (j)$
94	93	biimpi	$⊢ X \in ⋂_{m \in ℤ_{\geq n}} dom F (m) \to X \in ⋂_{j \in ℤ_{\geq n}} dom F (j)$
95	94	adantr	$⊢ (X \in ⋂_{m \in ℤ_{\geq n}} dom F (m) \land j \in ℤ_{\geq n}) \to X \in ⋂_{j \in ℤ_{\geq n}} dom F (j)$
96		simpr	$⊢ (X \in ⋂_{m \in ℤ_{\geq n}} dom F (m) \land j \in ℤ_{\geq n}) \to j \in ℤ_{\geq n}$
97		eliinid	$⊢ (X \in ⋂_{j \in ℤ_{\geq n}} dom F (j) \land j \in ℤ_{\geq n}) \to X \in dom F (j)$
98	95 96 97	syl2anc	$⊢ (X \in ⋂_{m \in ℤ_{\geq n}} dom F (m) \land j \in ℤ_{\geq n}) \to X \in dom F (j)$
99	98	3ad2antl3	$⊢ ((φ \land n \in Z \land X \in ⋂_{m \in ℤ_{\geq n}} dom F (m)) \land j \in ℤ_{\geq n}) \to X \in dom F (j)$
100		simpr	$⊢ ((φ \land n \in Z \land X \in ⋂_{m \in ℤ_{\geq n}} dom F (m)) \land j \in ℤ_{\geq n}) \to j \in ℤ_{\geq n}$
101		id	$⊢ j \in ℤ_{\geq n} \to j \in ℤ_{\geq n}$
102		fvexd	$⊢ j \in ℤ_{\geq n} \to F (j) (X) \in V$
103	88 24	nffv	$⊢ \underline{Ⅎ} m F (j) (X)$
104	90	fveq1d	$⊢ m = j \to F (m) (X) = F (j) (X)$
105		eqid	$⊢ (m \in ℤ_{\geq n} ⟼ F (m) (X)) = (m \in ℤ_{\geq n} ⟼ F (m) (X))$
106	87 103 104 105	fvmptf	$⊢ (j \in ℤ_{\geq n} \land F (j) (X) \in V) \to (m \in ℤ_{\geq n} ⟼ F (m) (X)) (j) = F (j) (X)$
107	101 102 106	syl2anc	$⊢ j \in ℤ_{\geq n} \to (m \in ℤ_{\geq n} ⟼ F (m) (X)) (j) = F (j) (X)$
108	107	adantl	$⊢ ((φ \land n \in Z \land X \in dom F (j)) \land j \in ℤ_{\geq n}) \to (m \in ℤ_{\geq n} ⟼ F (m) (X)) (j) = F (j) (X)$
109		simpll	$⊢ ((φ \land n \in Z) \land j \in ℤ_{\geq n}) \to φ$
110	36	adantll	$⊢ ((φ \land n \in Z) \land j \in ℤ_{\geq n}) \to j \in Z$
111	1 63	nfan	$⊢ Ⅎ m (φ \land j \in Z)$
112		nfcv	$⊢ \underline{Ⅎ} m ℝ$
113	88 89 112	nff	$⊢ Ⅎ m F (j) : dom F (j) ⟶ ℝ$
114	111 113	nfim	$⊢ Ⅎ m ((φ \land j \in Z) \to F (j) : dom F (j) ⟶ ℝ)$
115		eleq1w	$⊢ m = j \to (m \in Z \leftrightarrow j \in Z)$
116	115	anbi2d	$⊢ m = j \to ((φ \land m \in Z) \leftrightarrow (φ \land j \in Z))$
117	90 91	feq12d	$⊢ m = j \to (F (m) : dom F (m) ⟶ ℝ \leftrightarrow F (j) : dom F (j) ⟶ ℝ)$
118	116 117	imbi12d	$⊢ m = j \to (((φ \land m \in Z) \to F (m) : dom F (m) ⟶ ℝ) \leftrightarrow ((φ \land j \in Z) \to F (j) : dom F (j) ⟶ ℝ))$
119	114 118 5	chvarfv	$⊢ (φ \land j \in Z) \to F (j) : dom F (j) ⟶ ℝ$
120	109 110 119	syl2anc	$⊢ ((φ \land n \in Z) \land j \in ℤ_{\geq n}) \to F (j) : dom F (j) ⟶ ℝ$
121	120	3adantl3	$⊢ ((φ \land n \in Z \land X \in dom F (j)) \land j \in ℤ_{\geq n}) \to F (j) : dom F (j) ⟶ ℝ$
122		simpl3	$⊢ ((φ \land n \in Z \land X \in dom F (j)) \land j \in ℤ_{\geq n}) \to X \in dom F (j)$
123	121 122	ffvelrnd	$⊢ ((φ \land n \in Z \land X \in dom F (j)) \land j \in ℤ_{\geq n}) \to F (j) (X) \in ℝ$
124	108 123	eqeltrd	$⊢ ((φ \land n \in Z \land X \in dom F (j)) \land j \in ℤ_{\geq n}) \to (m \in ℤ_{\geq n} ⟼ F (m) (X)) (j) \in ℝ$
125	84 85 99 100 124	syl31anc	$⊢ ((φ \land n \in Z \land X \in ⋂_{m \in ℤ_{\geq n}} dom F (m)) \land j \in ℤ_{\geq n}) \to (m \in ℤ_{\geq n} ⟼ F (m) (X)) (j) \in ℝ$
126	33 32 83 125	climrecl	$⊢ (φ \land n \in Z \land X \in ⋂_{m \in ℤ_{\geq n}} dom F (m)) \to ⇝ ((m \in ℤ_{\geq n} ⟼ F (m) (X))) \in ℝ$
127	44 126	eqeltrd	$⊢ (φ \land n \in Z \land X \in ⋂_{m \in ℤ_{\geq n}} dom F (m)) \to ⇝ ((m \in Z ⟼ F (m) (X))) \in ℝ$
128	127	3exp	$⊢ φ \to (n \in Z \to (X \in ⋂_{m \in ℤ_{\geq n}} dom F (m) \to ⇝ ((m \in Z ⟼ F (m) (X))) \in ℝ))$
129	21 22 128	rexlimd	$⊢ φ \to (\exists n \in Z X \in ⋂_{m \in ℤ_{\geq n}} dom F (m) \to ⇝ ((m \in Z ⟼ F (m) (X))) \in ℝ)$
130	20 129	mpd	$⊢ φ \to ⇝ ((m \in Z ⟼ F (m) (X))) \in ℝ$

Metamath Proof Explorer

Theorem fnlimfvre

Proof