idlimc

Description: Limit of the identity function. (Contributed by Glauco Siliprandi, 11-Dec-2019)

	Ref	Expression
Hypotheses	idlimc.a	$⊢ φ \to A \subseteq ℂ$
	idlimc.f	$⊢ F = (x \in A ⟼ x)$
	idlimc.x	$⊢ φ \to X \in ℂ$
Assertion	idlimc	$⊢ φ \to X \in (F {lim}_{ℂ} X)$

Proof

Step	Hyp	Ref	Expression
1		idlimc.a	$⊢ φ \to A \subseteq ℂ$
2		idlimc.f	$⊢ F = (x \in A ⟼ x)$
3		idlimc.x	$⊢ φ \to X \in ℂ$
4		simpr	$⊢ (φ \land w \in ℝ^{+}) \to w \in ℝ^{+}$
5		simpr	$⊢ (φ \land x \in A) \to x \in A$
6	2	fvmpt2	$⊢ (x \in A \land x \in A) \to F (x) = x$
7	5 5 6	syl2anc	$⊢ (φ \land x \in A) \to F (x) = x$
8	7	fvoveq1d	$⊢ (φ \land x \in A) \to \|F (x) - X\| = \|x - X\|$
9	8	adantr	$⊢ ((φ \land x \in A) \land \|x - X\| < w) \to \|F (x) - X\| = \|x - X\|$
10		simpr	$⊢ ((φ \land x \in A) \land \|x - X\| < w) \to \|x - X\| < w$
11	9 10	eqbrtrd	$⊢ ((φ \land x \in A) \land \|x - X\| < w) \to \|F (x) - X\| < w$
12	11	adantrl	$⊢ ((φ \land x \in A) \land (x \neq X \land \|x - X\| < w)) \to \|F (x) - X\| < w$
13	12	ex	$⊢ (φ \land x \in A) \to ((x \neq X \land \|x - X\| < w) \to \|F (x) - X\| < w)$
14	13	adantlr	$⊢ ((φ \land w \in ℝ^{+}) \land x \in A) \to ((x \neq X \land \|x - X\| < w) \to \|F (x) - X\| < w)$
15	14	ralrimiva	$⊢ (φ \land w \in ℝ^{+}) \to \forall x \in A ((x \neq X \land \|x - X\| < w) \to \|F (x) - X\| < w)$
16		nfcv	$⊢ \underline{Ⅎ} z x$
17		nfcv	$⊢ \underline{Ⅎ} z X$
18	16 17	nfne	$⊢ Ⅎ z x \neq X$
19		nfv	$⊢ Ⅎ z \|x - X\| < w$
20	18 19	nfan	$⊢ Ⅎ z (x \neq X \land \|x - X\| < w)$
21		nfv	$⊢ Ⅎ z \|F (x) - X\| < w$
22	20 21	nfim	$⊢ Ⅎ z ((x \neq X \land \|x - X\| < w) \to \|F (x) - X\| < w)$
23		nfv	$⊢ Ⅎ x (z \neq X \land \|z - X\| < w)$
24		nfcv	$⊢ \underline{Ⅎ} x abs$
25		nfmpt1	$⊢ \underline{Ⅎ} x (x \in A ⟼ x)$
26	2 25	nfcxfr	$⊢ \underline{Ⅎ} x F$
27		nfcv	$⊢ \underline{Ⅎ} x z$
28	26 27	nffv	$⊢ \underline{Ⅎ} x F (z)$
29		nfcv	$⊢ \underline{Ⅎ} x -$
30		nfcv	$⊢ \underline{Ⅎ} x X$
31	28 29 30	nfov	$⊢ \underline{Ⅎ} x (F (z) - X)$
32	24 31	nffv	$⊢ \underline{Ⅎ} x \|F (z) - X\|$
33		nfcv	$⊢ \underline{Ⅎ} x <$
34		nfcv	$⊢ \underline{Ⅎ} x w$
35	32 33 34	nfbr	$⊢ Ⅎ x \|F (z) - X\| < w$
36	23 35	nfim	$⊢ Ⅎ x ((z \neq X \land \|z - X\| < w) \to \|F (z) - X\| < w)$
37		neeq1	$⊢ x = z \to (x \neq X \leftrightarrow z \neq X)$
38		fvoveq1	$⊢ x = z \to \|x - X\| = \|z - X\|$
39	38	breq1d	$⊢ x = z \to (\|x - X\| < w \leftrightarrow \|z - X\| < w)$
40	37 39	anbi12d	$⊢ x = z \to ((x \neq X \land \|x - X\| < w) \leftrightarrow (z \neq X \land \|z - X\| < w))$
41	40	imbrov2fvoveq	$⊢ x = z \to (((x \neq X \land \|x - X\| < w) \to \|F (x) - X\| < w) \leftrightarrow ((z \neq X \land \|z - X\| < w) \to \|F (z) - X\| < w))$
42	22 36 41	cbvralw	$⊢ \forall x \in A ((x \neq X \land \|x - X\| < w) \to \|F (x) - X\| < w) \leftrightarrow \forall z \in A ((z \neq X \land \|z - X\| < w) \to \|F (z) - X\| < w)$
43	15 42	sylib	$⊢ (φ \land w \in ℝ^{+}) \to \forall z \in A ((z \neq X \land \|z - X\| < w) \to \|F (z) - X\| < w)$
44		brimralrspcev	$⊢ (w \in ℝ^{+} \land \forall z \in A ((z \neq X \land \|z - X\| < w) \to \|F (z) - X\| < w)) \to \exists y \in ℝ^{+} \forall z \in A ((z \neq X \land \|z - X\| < y) \to \|F (z) - X\| < w)$
45	4 43 44	syl2anc	$⊢ (φ \land w \in ℝ^{+}) \to \exists y \in ℝ^{+} \forall z \in A ((z \neq X \land \|z - X\| < y) \to \|F (z) - X\| < w)$
46	45	ralrimiva	$⊢ φ \to \forall w \in ℝ^{+} \exists y \in ℝ^{+} \forall z \in A ((z \neq X \land \|z - X\| < y) \to \|F (z) - X\| < w)$
47	1	sselda	$⊢ (φ \land x \in A) \to x \in ℂ$
48	47 2	fmptd	$⊢ φ \to F : A ⟶ ℂ$
49	48 1 3	ellimc3	$⊢ φ \to (X \in (F {lim}_{ℂ} X) \leftrightarrow (X \in ℂ \land \forall w \in ℝ^{+} \exists y \in ℝ^{+} \forall z \in A ((z \neq X \land \|z - X\| < y) \to \|F (z) - X\| < w)))$
50	3 46 49	mpbir2and	$⊢ φ \to X \in (F {lim}_{ℂ} X)$

Metamath Proof Explorer

Theorem idlimc

Proof