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	$$⊢F⇝A\to \exists !xF⇝x$$

Proof

Step	Hyp	Ref	Expression
1		climcl	$$⊢F⇝A\to A\in ℂ$$
2		breq2	$$⊢y=A\to \left(F⇝y\leftrightarrow F⇝A\right)$$
3	2	spcegv	$$⊢A\in ℂ\to \left(F⇝A\to \exists yF⇝y\right)$$
4	1 3	mpcom	$$⊢F⇝A\to \exists yF⇝y$$
5		climuni	$$⊢\left(F⇝y\wedge F⇝x\right)\to y=x$$
6	5	gen2	$$⊢\forall y\forall x\left(\left(F⇝y\wedge F⇝x\right)\to y=x\right)$$
7		nfv	$$⊢ℲyF⇝x$$
8		nfv	$$⊢ℲxF⇝y$$
9		breq2	$$⊢x=y\to \left(F⇝x\leftrightarrow F⇝y\right)$$
10	7 8 9	cbveuw	$$⊢\exists !xF⇝x\leftrightarrow \exists !yF⇝y$$
11		breq2	$$⊢y=x\to \left(F⇝y\leftrightarrow F⇝x\right)$$
12	11	eu4	$$⊢\exists !yF⇝y\leftrightarrow \left(\exists yF⇝y\wedge \forall y\forall x\left(\left(F⇝y\wedge F⇝x\right)\to y=x\right)\right)$$
13	10 12	bitri	$$⊢\exists !xF⇝x\leftrightarrow \left(\exists yF⇝y\wedge \forall y\forall x\left(\left(F⇝y\wedge F⇝x\right)\to y=x\right)\right)$$
14	4 6 13	sylanblrc	$$⊢F⇝A\to \exists !xF⇝x$$