Theorem xlimcl

Description: The limit of a sequence of extended real numbers is an extended real number. (Contributed by Glauco Siliprandi, 5-Feb-2022)

	Ref	Expression
Assertion	xlimcl	$$⊢F\underset{*}{⇝}A\to A\in {ℝ}^{*}$$

Proof

Step	Hyp	Ref	Expression
1		letopon	$$⊢\mathrm{ordTop}\left(\le \right)\in \mathrm{TopOn}\left({ℝ}^{*}\right)$$
2		df-xlim	$$⊢\underset{*}{⇝}=\underset{t}{⇝}\left(\mathrm{ordTop}\left(\le \right)\right)$$
3	2	breqi	$$⊢F\underset{*}{⇝}A\leftrightarrow F\underset{t}{⇝}\left(\mathrm{ordTop}\left(\le \right)\right)A$$
4	3	biimpi	$$⊢F\underset{*}{⇝}A\to F\underset{t}{⇝}\left(\mathrm{ordTop}\left(\le \right)\right)A$$
5		lmcl	$$⊢\left(\mathrm{ordTop}\left(\le \right)\in \mathrm{TopOn}\left({ℝ}^{*}\right)\wedge F\underset{t}{⇝}\left(\mathrm{ordTop}\left(\le \right)\right)A\right)\to A\in {ℝ}^{*}$$
6	1 4 5	sylancr	$$⊢F\underset{*}{⇝}A\to A\in {ℝ}^{*}$$