Theorem lptioo1cn

Description: The lower bound of an open interval is a limit point of the interval, wirth respect to the standard topology on complex numbers. (Contributed by Glauco Siliprandi, 11-Dec-2019)

	Ref	Expression
Hypotheses	lptioo1cn.1	$$⊢J=\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)$$
	lptioo1cn.2	$$⊢\phi \to B\in {ℝ}^{*}$$
	lptioo1cn.3	$$⊢\phi \to A\in ℝ$$
	lptioo1cn.4	$$⊢\phi \to A<B$$
Assertion	lptioo1cn	$$⊢\phi \to A\in \mathrm{limPt}\left(J\right)\left(\left(A,B\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		lptioo1cn.1	$$⊢J=\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)$$
2		lptioo1cn.2	$$⊢\phi \to B\in {ℝ}^{*}$$
3		lptioo1cn.3	$$⊢\phi \to A\in ℝ$$
4		lptioo1cn.4	$$⊢\phi \to A<B$$
5		eqid	$$⊢\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)=\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)$$
6	5 3 2 4	lptioo1	$$⊢\phi \to A\in \mathrm{limPt}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\left(\left(A,B\right)\right)$$
7		eqid	$$⊢\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)=\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)$$
8	7	cnfldtop	$$⊢\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\in \mathrm{Top}$$
9	8	a1i	$$⊢\phi \to \mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\in \mathrm{Top}$$
10		ax-resscn	$$⊢ℝ\subseteq ℂ$$
11		unicntop	$$⊢ℂ=\bigcup \mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)$$
12	10 11	sseqtri	$$⊢ℝ\subseteq \bigcup \mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)$$
13	12	a1i	$$⊢\phi \to ℝ\subseteq \bigcup \mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)$$
14		ioossre	$$⊢\left(A,B\right)\subseteq ℝ$$
15	14	a1i	$$⊢\phi \to \left(A,B\right)\subseteq ℝ$$
16		eqid	$$⊢\bigcup \mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)=\bigcup \mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)$$
17	7	tgioo2	$$⊢\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)=\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){\upharpoonright }_{𝑡}ℝ$$
18	16 17	restlp	$$⊢\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\in \mathrm{Top}\wedge ℝ\subseteq \bigcup \mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\wedge \left(A,B\right)\subseteq ℝ\right)\to \mathrm{limPt}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\left(\left(A,B\right)\right)=\mathrm{limPt}\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\right)\left(\left(A,B\right)\right)\cap ℝ$$
19	9 13 15 18	syl3anc	$$⊢\phi \to \mathrm{limPt}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\left(\left(A,B\right)\right)=\mathrm{limPt}\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\right)\left(\left(A,B\right)\right)\cap ℝ$$
20	6 19	eleqtrd	$$⊢\phi \to A\in \left(\mathrm{limPt}\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\right)\left(\left(A,B\right)\right)\cap ℝ\right)$$
21		elin	$$⊢A\in \left(\mathrm{limPt}\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\right)\left(\left(A,B\right)\right)\cap ℝ\right)\leftrightarrow \left(A\in \mathrm{limPt}\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\right)\left(\left(A,B\right)\right)\wedge A\in ℝ\right)$$
22	20 21	sylib	$$⊢\phi \to \left(A\in \mathrm{limPt}\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\right)\left(\left(A,B\right)\right)\wedge A\in ℝ\right)$$
23	22	simpld	$$⊢\phi \to A\in \mathrm{limPt}\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\right)\left(\left(A,B\right)\right)$$
24	1	eqcomi	$$⊢\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)=J$$
25	24	fveq2i	$$⊢\mathrm{limPt}\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\right)=\mathrm{limPt}\left(J\right)$$
26	25	fveq1i	$$⊢\mathrm{limPt}\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\right)\left(\left(A,B\right)\right)=\mathrm{limPt}\left(J\right)\left(\left(A,B\right)\right)$$
27	23 26	eleqtrdi	$$⊢\phi \to A\in \mathrm{limPt}\left(J\right)\left(\left(A,B\right)\right)$$