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 | |- ( ph -> F ~~>* A ) |
|
| xlimuni.2 | |- ( ph -> F ~~>* B ) |
||
| Assertion | xlimuni | |- ( ph -> A = B ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | xlimuni.1 | |- ( ph -> F ~~>* A ) |
|
| 2 | xlimuni.2 | |- ( ph -> F ~~>* B ) |
|
| 3 | xrhaus | |- ( ordTop ` <_ ) e. Haus |
|
| 4 | 3 | a1i | |- ( ph -> ( ordTop ` <_ ) e. Haus ) |
| 5 | df-xlim | |- ~~>* = ( ~~>t ` ( ordTop ` <_ ) ) |
|
| 6 | 5 | breqi | |- ( F ~~>* A <-> F ( ~~>t ` ( ordTop ` <_ ) ) A ) |
| 7 | 1 6 | sylib | |- ( ph -> F ( ~~>t ` ( ordTop ` <_ ) ) A ) |
| 8 | 5 | breqi | |- ( F ~~>* B <-> F ( ~~>t ` ( ordTop ` <_ ) ) B ) |
| 9 | 2 8 | sylib | |- ( ph -> F ( ~~>t ` ( ordTop ` <_ ) ) B ) |
| 10 | 4 7 9 | lmmo | |- ( ph -> A = B ) |