Theorem xlimclim

Description: Given a sequence of reals, it converges to a real number A w.r.t. the standard topology on the reals, if and only if it converges to A w.r.t. to the standard topology on the extended reals (see climreeq ). (Contributed by Glauco Siliprandi, 5-Feb-2022)

	Ref	Expression
Hypotheses	xlimclim.m	$$⊢\phi \to M\in \mathbb{Z}$$
	xlimclim.z	$$⊢Z={\mathbb{Z}}_{\ge M}$$
	xlimclim.f	$$⊢\phi \to F:Z⟶ℝ$$
	xlimclim.a	$$⊢\phi \to A\in ℝ$$
Assertion	xlimclim	$$⊢\phi \to \left(F\underset{*}{⇝}A\leftrightarrow F⇝A\right)$$

Proof

Step	Hyp	Ref	Expression
1		xlimclim.m	$$⊢\phi \to M\in \mathbb{Z}$$
2		xlimclim.z	$$⊢Z={\mathbb{Z}}_{\ge M}$$
3		xlimclim.f	$$⊢\phi \to F:Z⟶ℝ$$
4		xlimclim.a	$$⊢\phi \to A\in ℝ$$
5		df-xlim	$$⊢\underset{*}{⇝}=\underset{t}{⇝}\left(\mathrm{ordTop}\left(\le \right)\right)$$
6	5	breqi	$$⊢F\underset{*}{⇝}A\leftrightarrow F\underset{t}{⇝}\left(\mathrm{ordTop}\left(\le \right)\right)A$$
7	6	a1i	$$⊢\phi \to \left(F\underset{*}{⇝}A\leftrightarrow F\underset{t}{⇝}\left(\mathrm{ordTop}\left(\le \right)\right)A\right)$$
8		xrtgioo2	$$⊢\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)=\mathrm{ordTop}\left(\le \right){\upharpoonright }_{𝑡}ℝ$$
9		reex	$$⊢ℝ\in \mathrm{V}$$
10	9	a1i	$$⊢\phi \to ℝ\in \mathrm{V}$$
11		letop	$$⊢\mathrm{ordTop}\left(\le \right)\in \mathrm{Top}$$
12	11	a1i	$$⊢\phi \to \mathrm{ordTop}\left(\le \right)\in \mathrm{Top}$$
13	8 2 10 12 4 1 3	lmss	$$⊢\phi \to \left(F\underset{t}{⇝}\left(\mathrm{ordTop}\left(\le \right)\right)A\leftrightarrow F\underset{t}{⇝}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)A\right)$$
14		eqid	$$⊢\underset{t}{⇝}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)=\underset{t}{⇝}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)$$
15	14 2 1 3	climreeq	$$⊢\phi \to \left(F\underset{t}{⇝}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)A\leftrightarrow F⇝A\right)$$
16	7 13 15	3bitrd	$$⊢\phi \to \left(F\underset{*}{⇝}A\leftrightarrow F⇝A\right)$$