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 | ⊢ ( 𝜑 → 𝐹 ~~>* 𝐴 ) | |
| xlimuni.2 | ⊢ ( 𝜑 → 𝐹 ~~>* 𝐵 ) | ||
| Assertion | xlimuni | ⊢ ( 𝜑 → 𝐴 = 𝐵 ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | xlimuni.1 | ⊢ ( 𝜑 → 𝐹 ~~>* 𝐴 ) | |
| 2 | xlimuni.2 | ⊢ ( 𝜑 → 𝐹 ~~>* 𝐵 ) | |
| 3 | xrhaus | ⊢ ( ordTop ‘ ≤ ) ∈ Haus | |
| 4 | 3 | a1i | ⊢ ( 𝜑 → ( ordTop ‘ ≤ ) ∈ Haus ) |
| 5 | df-xlim | ⊢ ~~>* = ( ⇝𝑡 ‘ ( ordTop ‘ ≤ ) ) | |
| 6 | 5 | breqi | ⊢ ( 𝐹 ~~>* 𝐴 ↔ 𝐹 ( ⇝𝑡 ‘ ( ordTop ‘ ≤ ) ) 𝐴 ) |
| 7 | 1 6 | sylib | ⊢ ( 𝜑 → 𝐹 ( ⇝𝑡 ‘ ( ordTop ‘ ≤ ) ) 𝐴 ) |
| 8 | 5 | breqi | ⊢ ( 𝐹 ~~>* 𝐵 ↔ 𝐹 ( ⇝𝑡 ‘ ( ordTop ‘ ≤ ) ) 𝐵 ) |
| 9 | 2 8 | sylib | ⊢ ( 𝜑 → 𝐹 ( ⇝𝑡 ‘ ( ordTop ‘ ≤ ) ) 𝐵 ) |
| 10 | 4 7 9 | lmmo | ⊢ ( 𝜑 → 𝐴 = 𝐵 ) |