Theorem lmlim

Description: Relate a limit in a given topology to a complex number limit, provided that topology agrees with the common topology on CC on the required subset. (Contributed by Thierry Arnoux, 11-Jul-2017)

	Ref	Expression
Hypotheses	lmlim.j	$$⊢J\in \mathrm{TopOn}\left(Y\right)$$
	lmlim.f	$$⊢\phi \to F:\mathbb{N}⟶X$$
	lmlim.p	$$⊢\phi \to P\in X$$
	lmlim.t	$$⊢J{\upharpoonright }_{𝑡}X=\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){\upharpoonright }_{𝑡}X$$
	lmlim.x	$$⊢X\subseteq ℂ$$
Assertion	lmlim	$$⊢\phi \to \left(F\underset{t}{⇝}\left(J\right)P\leftrightarrow F⇝P\right)$$

Proof

Step	Hyp	Ref	Expression
1		lmlim.j	$$⊢J\in \mathrm{TopOn}\left(Y\right)$$
2		lmlim.f	$$⊢\phi \to F:\mathbb{N}⟶X$$
3		lmlim.p	$$⊢\phi \to P\in X$$
4		lmlim.t	$$⊢J{\upharpoonright }_{𝑡}X=\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){\upharpoonright }_{𝑡}X$$
5		lmlim.x	$$⊢X\subseteq ℂ$$
6		eqid	$$⊢J{\upharpoonright }_{𝑡}X=J{\upharpoonright }_{𝑡}X$$
7		nnuz	$$⊢\mathbb{N}={\mathbb{Z}}_{\ge 1}$$
8		cnex	$$⊢ℂ\in \mathrm{V}$$
9	8	a1i	$$⊢\phi \to ℂ\in \mathrm{V}$$
10	5	a1i	$$⊢\phi \to X\subseteq ℂ$$
11	9 10	ssexd	$$⊢\phi \to X\in \mathrm{V}$$
12	1	topontopi	$$⊢J\in \mathrm{Top}$$
13	12	a1i	$$⊢\phi \to J\in \mathrm{Top}$$
14		1z	$$⊢1\in \mathbb{Z}$$
15	14	a1i	$$⊢\phi \to 1\in \mathbb{Z}$$
16	6 7 11 13 3 15 2	lmss	$$⊢\phi \to \left(F\underset{t}{⇝}\left(J\right)P\leftrightarrow F\underset{t}{⇝}\left(J{\upharpoonright }_{𝑡}X\right)P\right)$$
17	4	fveq2i	$$⊢\underset{t}{⇝}\left(J{\upharpoonright }_{𝑡}X\right)=\underset{t}{⇝}\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){\upharpoonright }_{𝑡}X\right)$$
18	17	breqi	$$⊢F\underset{t}{⇝}\left(J{\upharpoonright }_{𝑡}X\right)P\leftrightarrow F\underset{t}{⇝}\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){\upharpoonright }_{𝑡}X\right)P$$
19	18	a1i	$$⊢\phi \to \left(F\underset{t}{⇝}\left(J{\upharpoonright }_{𝑡}X\right)P\leftrightarrow F\underset{t}{⇝}\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){\upharpoonright }_{𝑡}X\right)P\right)$$
20		eqid	$$⊢\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){\upharpoonright }_{𝑡}X=\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){\upharpoonright }_{𝑡}X$$
21		eqid	$$⊢\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)=\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)$$
22	21	cnfldtop	$$⊢\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\in \mathrm{Top}$$
23	22	a1i	$$⊢\phi \to \mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\in \mathrm{Top}$$
24	20 7 11 23 3 15 2	lmss	$$⊢\phi \to \left(F\underset{t}{⇝}\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\right)P\leftrightarrow F\underset{t}{⇝}\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){\upharpoonright }_{𝑡}X\right)P\right)$$
25		fss	$$⊢\left(F:\mathbb{N}⟶X\wedge X\subseteq ℂ\right)\to F:\mathbb{N}⟶ℂ$$
26	2 5 25	sylancl	$$⊢\phi \to F:\mathbb{N}⟶ℂ$$
27	21 7	lmclimf	$$⊢\left(1\in \mathbb{Z}\wedge F:\mathbb{N}⟶ℂ\right)\to \left(F\underset{t}{⇝}\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\right)P\leftrightarrow F⇝P\right)$$
28	14 26 27	sylancr	$$⊢\phi \to \left(F\underset{t}{⇝}\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\right)P\leftrightarrow F⇝P\right)$$
29	24 28	bitr3d	$$⊢\phi \to \left(F\underset{t}{⇝}\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){\upharpoonright }_{𝑡}X\right)P\leftrightarrow F⇝P\right)$$
30	16 19 29	3bitrd	$$⊢\phi \to \left(F\underset{t}{⇝}\left(J\right)P\leftrightarrow F⇝P\right)$$