Theorem climeu

Description: An infinite sequence of complex numbers converges to at most one limit. (Contributed by NM, 25-Dec-2005)

	Ref	Expression
Assertion	climeu	⊢ ( 𝐹 ⇝ 𝐴 → ∃! 𝑥 𝐹 ⇝ 𝑥 )

Proof

Step	Hyp	Ref	Expression
1		climcl	⊢ ( 𝐹 ⇝ 𝐴 → 𝐴 ∈ ℂ )
2		breq2	⊢ ( 𝑦 = 𝐴 → ( 𝐹 ⇝ 𝑦 ↔ 𝐹 ⇝ 𝐴 ) )
3	2	spcegv	⊢ ( 𝐴 ∈ ℂ → ( 𝐹 ⇝ 𝐴 → ∃ 𝑦 𝐹 ⇝ 𝑦 ) )
4	1 3	mpcom	⊢ ( 𝐹 ⇝ 𝐴 → ∃ 𝑦 𝐹 ⇝ 𝑦 )
5		climuni	⊢ ( ( 𝐹 ⇝ 𝑦 ∧ 𝐹 ⇝ 𝑥 ) → 𝑦 = 𝑥 )
6	5	gen2	⊢ ∀ 𝑦 ∀ 𝑥 ( ( 𝐹 ⇝ 𝑦 ∧ 𝐹 ⇝ 𝑥 ) → 𝑦 = 𝑥 )
7		nfv	⊢ Ⅎ 𝑦 𝐹 ⇝ 𝑥
8		nfv	⊢ Ⅎ 𝑥 𝐹 ⇝ 𝑦
9		breq2	⊢ ( 𝑥 = 𝑦 → ( 𝐹 ⇝ 𝑥 ↔ 𝐹 ⇝ 𝑦 ) )
10	7 8 9	cbveuw	⊢ ( ∃! 𝑥 𝐹 ⇝ 𝑥 ↔ ∃! 𝑦 𝐹 ⇝ 𝑦 )
11		breq2	⊢ ( 𝑦 = 𝑥 → ( 𝐹 ⇝ 𝑦 ↔ 𝐹 ⇝ 𝑥 ) )
12	11	eu4	⊢ ( ∃! 𝑦 𝐹 ⇝ 𝑦 ↔ ( ∃ 𝑦 𝐹 ⇝ 𝑦 ∧ ∀ 𝑦 ∀ 𝑥 ( ( 𝐹 ⇝ 𝑦 ∧ 𝐹 ⇝ 𝑥 ) → 𝑦 = 𝑥 ) ) )
13	10 12	bitri	⊢ ( ∃! 𝑥 𝐹 ⇝ 𝑥 ↔ ( ∃ 𝑦 𝐹 ⇝ 𝑦 ∧ ∀ 𝑦 ∀ 𝑥 ( ( 𝐹 ⇝ 𝑦 ∧ 𝐹 ⇝ 𝑥 ) → 𝑦 = 𝑥 ) ) )
14	4 6 13	sylanblrc	⊢ ( 𝐹 ⇝ 𝐴 → ∃! 𝑥 𝐹 ⇝ 𝑥 )