Theorem xlimuni

Description: An infinite sequence converges to at most one limit (w.r.t. to the standard topology on the extended reals). (Contributed by Glauco Siliprandi, 23-Apr-2023)

	Ref	Expression
Hypotheses	xlimuni.1	$$⊢\phi \to F\underset{*}{⇝}A$$
	xlimuni.2	$$⊢\phi \to F\underset{*}{⇝}B$$
Assertion	xlimuni	$$⊢\phi \to A=B$$

Proof

Step	Hyp	Ref	Expression
1		xlimuni.1	$$⊢\phi \to F\underset{*}{⇝}A$$
2		xlimuni.2	$$⊢\phi \to F\underset{*}{⇝}B$$
3		xrhaus	$$⊢\mathrm{ordTop}\left(\le \right)\in \mathrm{Haus}$$
4	3	a1i	$$⊢\phi \to \mathrm{ordTop}\left(\le \right)\in \mathrm{Haus}$$
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	1 6	sylib	$$⊢\phi \to F\underset{t}{⇝}\left(\mathrm{ordTop}\left(\le \right)\right)A$$
8	5	breqi	$$⊢F\underset{*}{⇝}B\leftrightarrow F\underset{t}{⇝}\left(\mathrm{ordTop}\left(\le \right)\right)B$$
9	2 8	sylib	$$⊢\phi \to F\underset{t}{⇝}\left(\mathrm{ordTop}\left(\le \right)\right)B$$
10	4 7 9	lmmo	$$⊢\phi \to A=B$$