Theorem climmo

Description: An infinite sequence of complex numbers converges to at most one limit. (Contributed by Mario Carneiro, 13-Jul-2013)

	Ref	Expression
Assertion	climmo	⊢ ∃* 𝑥 𝐹 ⇝ 𝑥

Proof

Step	Hyp	Ref	Expression
1		breq2	⊢ ( 𝑥 = 𝑦 → ( 𝐹 ⇝ 𝑥 ↔ 𝐹 ⇝ 𝑦 ) )
2	1	cbvexvw	⊢ ( ∃ 𝑥 𝐹 ⇝ 𝑥 ↔ ∃ 𝑦 𝐹 ⇝ 𝑦 )
3		climeu	⊢ ( 𝐹 ⇝ 𝑦 → ∃! 𝑥 𝐹 ⇝ 𝑥 )
4	3	exlimiv	⊢ ( ∃ 𝑦 𝐹 ⇝ 𝑦 → ∃! 𝑥 𝐹 ⇝ 𝑥 )
5	2 4	sylbi	⊢ ( ∃ 𝑥 𝐹 ⇝ 𝑥 → ∃! 𝑥 𝐹 ⇝ 𝑥 )
6		moeu	⊢ ( ∃* 𝑥 𝐹 ⇝ 𝑥 ↔ ( ∃ 𝑥 𝐹 ⇝ 𝑥 → ∃! 𝑥 𝐹 ⇝ 𝑥 ) )
7	5 6	mpbir	⊢ ∃* 𝑥 𝐹 ⇝ 𝑥