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

Proof

Step	Hyp	Ref	Expression
1		fnlimfvre2.p	$⊢ Ⅎ m φ$
2		fnlimfvre2.m	$⊢ \underline{Ⅎ} m F$
3		fnlimfvre2.n	$⊢ \underline{Ⅎ} x F$
4		fnlimfvre2.z	$⊢ Z = ℤ_{\geq M}$
5		fnlimfvre2.f	$⊢ (φ \land m \in Z) \to F (m) : dom F (m) ⟶ ℝ$
6		fnlimfvre2.d	$⊢ D = \{x \in ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} dom F (m) \| (m \in Z ⟼ F (m) (x)) \in dom ⇝\}$
7		fnlimfvre2.g	$⊢ G = (x \in D ⟼ ⇝ ((m \in Z ⟼ F (m) (x))))$
8		fnlimfvre2.x	$⊢ φ \to X \in D$
9		nfrab1	$⊢ \underline{Ⅎ} x \{x \in ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} dom F (m) \| (m \in Z ⟼ F (m) (x)) \in dom ⇝\}$
10	6 9	nfcxfr	$⊢ \underline{Ⅎ} x D$
11		nfcv	$⊢ \underline{Ⅎ} z D$
12		nfcv	$⊢ \underline{Ⅎ} z ⇝ ((m \in Z ⟼ F (m) (x)))$
13		nfcv	$⊢ \underline{Ⅎ} x ⇝$
14		nfcv	$⊢ \underline{Ⅎ} x Z$
15		nfcv	$⊢ \underline{Ⅎ} x m$
16	3 15	nffv	$⊢ \underline{Ⅎ} x F (m)$
17		nfcv	$⊢ \underline{Ⅎ} x z$
18	16 17	nffv	$⊢ \underline{Ⅎ} x F (m) (z)$
19	14 18	nfmpt	$⊢ \underline{Ⅎ} x (m \in Z ⟼ F (m) (z))$
20	13 19	nffv	$⊢ \underline{Ⅎ} x ⇝ ((m \in Z ⟼ F (m) (z)))$
21		fveq2	$⊢ x = z \to F (m) (x) = F (m) (z)$
22	21	mpteq2dv	$⊢ x = z \to (m \in Z ⟼ F (m) (x)) = (m \in Z ⟼ F (m) (z))$
23	22	fveq2d	$⊢ x = z \to ⇝ ((m \in Z ⟼ F (m) (x))) = ⇝ ((m \in Z ⟼ F (m) (z)))$
24	10 11 12 20 23	cbvmptf	$⊢ (x \in D ⟼ ⇝ ((m \in Z ⟼ F (m) (x)))) = (z \in D ⟼ ⇝ ((m \in Z ⟼ F (m) (z))))$
25	7 24	eqtri	$⊢ G = (z \in D ⟼ ⇝ ((m \in Z ⟼ F (m) (z))))$
26		fveq2	$⊢ X = z \to F (m) (X) = F (m) (z)$
27	26	mpteq2dv	$⊢ X = z \to (m \in Z ⟼ F (m) (X)) = (m \in Z ⟼ F (m) (z))$
28		eqcom	$⊢ X = z \leftrightarrow z = X$
29	28	imbi1i	$⊢ (X = z \to (m \in Z ⟼ F (m) (X)) = (m \in Z ⟼ F (m) (z))) \leftrightarrow (z = X \to (m \in Z ⟼ F (m) (X)) = (m \in Z ⟼ F (m) (z)))$
30		eqcom	$⊢ (m \in Z ⟼ F (m) (X)) = (m \in Z ⟼ F (m) (z)) \leftrightarrow (m \in Z ⟼ F (m) (z)) = (m \in Z ⟼ F (m) (X))$
31	30	imbi2i	$⊢ (z = X \to (m \in Z ⟼ F (m) (X)) = (m \in Z ⟼ F (m) (z))) \leftrightarrow (z = X \to (m \in Z ⟼ F (m) (z)) = (m \in Z ⟼ F (m) (X)))$
32	29 31	bitri	$⊢ (X = z \to (m \in Z ⟼ F (m) (X)) = (m \in Z ⟼ F (m) (z))) \leftrightarrow (z = X \to (m \in Z ⟼ F (m) (z)) = (m \in Z ⟼ F (m) (X)))$
33	27 32	mpbi	$⊢ z = X \to (m \in Z ⟼ F (m) (z)) = (m \in Z ⟼ F (m) (X))$
34	33	fveq2d	$⊢ z = X \to ⇝ ((m \in Z ⟼ F (m) (z))) = ⇝ ((m \in Z ⟼ F (m) (X)))$
35		fvexd	$⊢ φ \to ⇝ ((m \in Z ⟼ F (m) (X))) \in V$
36	25 34 8 35	fvmptd3	$⊢ φ \to G (X) = ⇝ ((m \in Z ⟼ F (m) (X)))$
37	1 2 3 4 5 6 8	fnlimfvre	$⊢ φ \to ⇝ ((m \in Z ⟼ F (m) (X))) \in ℝ$
38	36 37	eqeltrd	$⊢ φ \to G (X) \in ℝ$

Metamath Proof Explorer

Theorem fnlimfvre2

Proof