# Metamath Proof Explorer

## Theorem fclim

Description: The limit relation is function-like, and with range 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}\phantom{\rule{.4em}{0ex}}\left(\left({x}⇝{y}\wedge {x}⇝{z}\right)\to {y}={z}\right)$
4 3 ax-gen ${⊢}\forall {y}\phantom{\rule{.4em}{0ex}}\forall {z}\phantom{\rule{.4em}{0ex}}\left(\left({x}⇝{y}\wedge {x}⇝{z}\right)\to {y}={z}\right)$
5 4 ax-gen ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\forall {z}\phantom{\rule{.4em}{0ex}}\left(\left({x}⇝{y}\wedge {x}⇝{z}\right)\to {y}={z}\right)$
6 dffun2 ${⊢}\mathrm{Fun}⇝↔\left(\mathrm{Rel}⇝\wedge \forall {x}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\forall {z}\phantom{\rule{.4em}{0ex}}\left(\left({x}⇝{y}\wedge {x}⇝{z}\right)\to {y}={z}\right)\right)$
7 1 5 6 mpbir2an ${⊢}\mathrm{Fun}⇝$
8 funfn ${⊢}\mathrm{Fun}⇝↔⇝Fn\mathrm{dom}⇝$
9 7 8 mpbi ${⊢}⇝Fn\mathrm{dom}⇝$
10 vex ${⊢}{y}\in \mathrm{V}$
11 10 elrn ${⊢}{y}\in \mathrm{ran}⇝↔\exists {x}\phantom{\rule{.4em}{0ex}}{x}⇝{y}$
12 climcl ${⊢}{x}⇝{y}\to {y}\in ℂ$
13 12 exlimiv ${⊢}\exists {x}\phantom{\rule{.4em}{0ex}}{x}⇝{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}⇝⟶ℂ↔\left(⇝Fn\mathrm{dom}⇝\wedge \mathrm{ran}⇝\subseteq ℂ\right)$
17 9 15 16 mpbir2an ${⊢}⇝:\mathrm{dom}⇝⟶ℂ$