Theorem idlimc

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

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

Proof

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