Theorem limcmo

Description: If B is a limit point of the domain of the function F , then there is at most one limit value of F at B . (Contributed by Mario Carneiro, 25-Dec-2016)

	Ref	Expression
Hypotheses	limcflf.f	$$⊢\phi \to F:A⟶ℂ$$
	limcflf.a	$$⊢\phi \to A\subseteq ℂ$$
	limcflf.b	$$⊢\phi \to B\in \mathrm{limPt}\left(K\right)\left(A\right)$$
	limcflf.k	$$⊢K=\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)$$
Assertion	limcmo	$$⊢\phi \to {\exists }^{*}xx\in \left(F{lim}_{ℂ}B\right)$$

Proof

Step	Hyp	Ref	Expression
1		limcflf.f	$$⊢\phi \to F:A⟶ℂ$$
2		limcflf.a	$$⊢\phi \to A\subseteq ℂ$$
3		limcflf.b	$$⊢\phi \to B\in \mathrm{limPt}\left(K\right)\left(A\right)$$
4		limcflf.k	$$⊢K=\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)$$
5	4	cnfldhaus	$$⊢K\in \mathrm{Haus}$$
6		eqid	$$⊢A\setminus \left\{B\right\}=A\setminus \left\{B\right\}$$
7		eqid	$$⊢\mathrm{nei}\left(K\right)\left(\left\{B\right\}\right){\upharpoonright }_{𝑡}\left(A\setminus \left\{B\right\}\right)=\mathrm{nei}\left(K\right)\left(\left\{B\right\}\right){\upharpoonright }_{𝑡}\left(A\setminus \left\{B\right\}\right)$$
8	1 2 3 4 6 7	limcflflem	$$⊢\phi \to \mathrm{nei}\left(K\right)\left(\left\{B\right\}\right){\upharpoonright }_{𝑡}\left(A\setminus \left\{B\right\}\right)\in \mathrm{Fil}\left(A\setminus \left\{B\right\}\right)$$
9		difss	$$⊢A\setminus \left\{B\right\}\subseteq A$$
10		fssres	$$⊢\left(F:A⟶ℂ\wedge A\setminus \left\{B\right\}\subseteq A\right)\to \left({F\upharpoonright }_{\left(A\setminus \left\{B\right\}\right)}\right):A\setminus \left\{B\right\}⟶ℂ$$
11	1 9 10	sylancl	$$⊢\phi \to \left({F\upharpoonright }_{\left(A\setminus \left\{B\right\}\right)}\right):A\setminus \left\{B\right\}⟶ℂ$$
12	4	cnfldtopon	$$⊢K\in \mathrm{TopOn}\left(ℂ\right)$$
13	12	toponunii	$$⊢ℂ=\bigcup K$$
14	13	hausflf	$$⊢\left(K\in \mathrm{Haus}\wedge \mathrm{nei}\left(K\right)\left(\left\{B\right\}\right){\upharpoonright }_{𝑡}\left(A\setminus \left\{B\right\}\right)\in \mathrm{Fil}\left(A\setminus \left\{B\right\}\right)\wedge \left({F\upharpoonright }_{\left(A\setminus \left\{B\right\}\right)}\right):A\setminus \left\{B\right\}⟶ℂ\right)\to {\exists }^{*}xx\in \left(K\mathrm{fLimf}\left(\mathrm{nei}\left(K\right)\left(\left\{B\right\}\right){\upharpoonright }_{𝑡}\left(A\setminus \left\{B\right\}\right)\right)\right)\left({F\upharpoonright }_{\left(A\setminus \left\{B\right\}\right)}\right)$$
15	5 8 11 14	mp3an2i	$$⊢\phi \to {\exists }^{*}xx\in \left(K\mathrm{fLimf}\left(\mathrm{nei}\left(K\right)\left(\left\{B\right\}\right){\upharpoonright }_{𝑡}\left(A\setminus \left\{B\right\}\right)\right)\right)\left({F\upharpoonright }_{\left(A\setminus \left\{B\right\}\right)}\right)$$
16	1 2 3 4 6 7	limcflf	$$⊢\phi \to F{lim}_{ℂ}B=\left(K\mathrm{fLimf}\left(\mathrm{nei}\left(K\right)\left(\left\{B\right\}\right){\upharpoonright }_{𝑡}\left(A\setminus \left\{B\right\}\right)\right)\right)\left({F\upharpoonright }_{\left(A\setminus \left\{B\right\}\right)}\right)$$
17	16	eleq2d	$$⊢\phi \to \left(x\in \left(F{lim}_{ℂ}B\right)\leftrightarrow x\in \left(K\mathrm{fLimf}\left(\mathrm{nei}\left(K\right)\left(\left\{B\right\}\right){\upharpoonright }_{𝑡}\left(A\setminus \left\{B\right\}\right)\right)\right)\left({F\upharpoonright }_{\left(A\setminus \left\{B\right\}\right)}\right)\right)$$
18	17	mobidv	$$⊢\phi \to \left({\exists }^{*}xx\in \left(F{lim}_{ℂ}B\right)\leftrightarrow {\exists }^{*}xx\in \left(K\mathrm{fLimf}\left(\mathrm{nei}\left(K\right)\left(\left\{B\right\}\right){\upharpoonright }_{𝑡}\left(A\setminus \left\{B\right\}\right)\right)\right)\left({F\upharpoonright }_{\left(A\setminus \left\{B\right\}\right)}\right)\right)$$
19	15 18	mpbird	$$⊢\phi \to {\exists }^{*}xx\in \left(F{lim}_{ℂ}B\right)$$