Theorem xlimconst

Description: A constant sequence converges to its value, w.r.t. the standard topology on the extended reals. (Contributed by Glauco Siliprandi, 5-Feb-2022)

	Ref	Expression
Hypotheses	xlimconst.p	$$⊢Ⅎk\phi$$
	xlimconst.k	$$⊢\underset{\_}{Ⅎ}kF$$
	xlimconst.m	$$⊢\phi \to M\in \mathbb{Z}$$
	xlimconst.z	$$⊢Z={\mathbb{Z}}_{\ge M}$$
	xlimconst.f	$$⊢\phi \to FFnZ$$
	xlimconst.a	$$⊢\phi \to A\in {ℝ}^{*}$$
	xlimconst.e	$$⊢\left(\phi \wedge k\in Z\right)\to F\left(k\right)=A$$
Assertion	xlimconst	$$⊢\phi \to F\underset{*}{⇝}A$$

Proof

Step	Hyp	Ref	Expression
1		xlimconst.p	$$⊢Ⅎk\phi$$
2		xlimconst.k	$$⊢\underset{\_}{Ⅎ}kF$$
3		xlimconst.m	$$⊢\phi \to M\in \mathbb{Z}$$
4		xlimconst.z	$$⊢Z={\mathbb{Z}}_{\ge M}$$
5		xlimconst.f	$$⊢\phi \to FFnZ$$
6		xlimconst.a	$$⊢\phi \to A\in {ℝ}^{*}$$
7		xlimconst.e	$$⊢\left(\phi \wedge k\in Z\right)\to F\left(k\right)=A$$
8	1 2 5 6 7	fconst7	$$⊢\phi \to F=Z\times \left\{A\right\}$$
9		letopon	$$⊢\mathrm{ordTop}\left(\le \right)\in \mathrm{TopOn}\left({ℝ}^{*}\right)$$
10	4	lmconst	$$⊢\left(\mathrm{ordTop}\left(\le \right)\in \mathrm{TopOn}\left({ℝ}^{*}\right)\wedge A\in {ℝ}^{*}\wedge M\in \mathbb{Z}\right)\to \left(Z\times \left\{A\right\}\right)\underset{t}{⇝}\left(\mathrm{ordTop}\left(\le \right)\right)A$$
11	9 6 3 10	mp3an2i	$$⊢\phi \to \left(Z\times \left\{A\right\}\right)\underset{t}{⇝}\left(\mathrm{ordTop}\left(\le \right)\right)A$$
12	8 11	eqbrtrd	$$⊢\phi \to F\underset{t}{⇝}\left(\mathrm{ordTop}\left(\le \right)\right)A$$
13		df-xlim	$$⊢\underset{*}{⇝}=\underset{t}{⇝}\left(\mathrm{ordTop}\left(\le \right)\right)$$
14	13	breqi	$$⊢F\underset{*}{⇝}A\leftrightarrow F\underset{t}{⇝}\left(\mathrm{ordTop}\left(\le \right)\right)A$$
15	12 14	sylibr	$$⊢\phi \to F\underset{*}{⇝}A$$