Theorem fclim

Description: The limit relation is function-like, and with codomain the complex numbers. (Contributed by Mario Carneiro, 31-Jan-2014)

	Ref	Expression
Assertion	fclim	$$⊢⇝:\mathrm{dom}⇝⟶ℂ$$

Proof

Step	Hyp	Ref	Expression
1		climrel	$$⊢\mathrm{Rel}⇝$$
2		climuni	$$⊢\left(x⇝y\wedge x⇝z\right)\to y=z$$
3	2	ax-gen	$$⊢\forall z\left(\left(x⇝y\wedge x⇝z\right)\to y=z\right)$$
4	3	ax-gen	$$⊢\forall y\forall z\left(\left(x⇝y\wedge x⇝z\right)\to y=z\right)$$
5	4	ax-gen	$$⊢\forall x\forall y\forall z\left(\left(x⇝y\wedge x⇝z\right)\to y=z\right)$$
6		dffun2	$$⊢\mathrm{Fun}⇝\leftrightarrow \left(\mathrm{Rel}⇝\wedge \forall x\forall y\forall z\left(\left(x⇝y\wedge x⇝z\right)\to y=z\right)\right)$$
7	1 5 6	mpbir2an	$$⊢\mathrm{Fun}⇝$$
8		funfn	$$⊢\mathrm{Fun}⇝\leftrightarrow ⇝Fn\mathrm{dom}⇝$$
9	7 8	mpbi	$$⊢⇝Fn\mathrm{dom}⇝$$
10		vex	$$⊢y\in \mathrm{V}$$
11	10	elrn	$$⊢y\in \mathrm{ran}⇝\leftrightarrow \exists xx⇝y$$
12		climcl	$$⊢x⇝y\to y\in ℂ$$
13	12	exlimiv	$$⊢\exists xx⇝y\to y\in ℂ$$
14	11 13	sylbi	$$⊢y\in \mathrm{ran}⇝\to y\in ℂ$$
15	14	ssriv	$$⊢\mathrm{ran}⇝\subseteq ℂ$$
16		df-f	$$⊢⇝:\mathrm{dom}⇝⟶ℂ\leftrightarrow \left(⇝Fn\mathrm{dom}⇝\wedge \mathrm{ran}⇝\subseteq ℂ\right)$$
17	9 15 16	mpbir2an	$$⊢⇝:\mathrm{dom}⇝⟶ℂ$$