Theorem limccl

Description: Closure of the limit operator. (Contributed by Mario Carneiro, 25-Dec-2016)

	Ref	Expression
Assertion	limccl	$$⊢F{lim}_{ℂ}B\subseteq ℂ$$

Proof

Step	Hyp	Ref	Expression
1		limcrcl	$$⊢x\in \left(F{lim}_{ℂ}B\right)\to \left(F:\mathrm{dom}F⟶ℂ\wedge \mathrm{dom}F\subseteq ℂ\wedge B\in ℂ\right)$$
2		eqid	$$⊢\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){\upharpoonright }_{𝑡}\left(\mathrm{dom}F\cup \left\{B\right\}\right)=\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){\upharpoonright }_{𝑡}\left(\mathrm{dom}F\cup \left\{B\right\}\right)$$
3		eqid	$$⊢\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)=\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)$$
4	2 3	limcfval	$$⊢\left(F:\mathrm{dom}F⟶ℂ\wedge \mathrm{dom}F\subseteq ℂ\wedge B\in ℂ\right)\to \left(F{lim}_{ℂ}B=\left\{y|\left(z\in \left(\mathrm{dom}F\cup \left\{B\right\}\right)⟼if\left(z=B,y,F\left(z\right)\right)\right)\in \left(\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){\upharpoonright }_{𝑡}\left(\mathrm{dom}F\cup \left\{B\right\}\right)\right)\mathrm{CnP}\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\right)\left(B\right)\right\}\wedge F{lim}_{ℂ}B\subseteq ℂ\right)$$
5	1 4	syl	$$⊢x\in \left(F{lim}_{ℂ}B\right)\to \left(F{lim}_{ℂ}B=\left\{y|\left(z\in \left(\mathrm{dom}F\cup \left\{B\right\}\right)⟼if\left(z=B,y,F\left(z\right)\right)\right)\in \left(\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){\upharpoonright }_{𝑡}\left(\mathrm{dom}F\cup \left\{B\right\}\right)\right)\mathrm{CnP}\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\right)\left(B\right)\right\}\wedge F{lim}_{ℂ}B\subseteq ℂ\right)$$
6	5	simprd	$$⊢x\in \left(F{lim}_{ℂ}B\right)\to F{lim}_{ℂ}B\subseteq ℂ$$
7		id	$$⊢x\in \left(F{lim}_{ℂ}B\right)\to x\in \left(F{lim}_{ℂ}B\right)$$
8	6 7	sseldd	$$⊢x\in \left(F{lim}_{ℂ}B\right)\to x\in ℂ$$
9	8	ssriv	$$⊢F{lim}_{ℂ}B\subseteq ℂ$$