This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⊢ ⇝ : dom ⁡ ⇝ ⟶ ℂ

Proof

Step Hyp Ref Expression
1 climrel ⊢ Rel ⁡ ⇝
2 climuni ⊢ x ⇝ y ∧ x ⇝ z → y = z
3 2 ax-gen ⊢ ∀ z x ⇝ y ∧ x ⇝ z → y = z
4 3 ax-gen ⊢ ∀ y ∀ z x ⇝ y ∧ x ⇝ z → y = z
5 4 ax-gen ⊢ ∀ x ∀ y ∀ z x ⇝ y ∧ x ⇝ z → y = z
6 dffun2 ⊢ Fun ⁡ ⇝ ↔ Rel ⁡ ⇝ ∧ ∀ x ∀ y ∀ z x ⇝ y ∧ x ⇝ z → y = z
7 1 5 6 mpbir2an ⊢ Fun ⁡ ⇝
8 funfn ⊢ Fun ⁡ ⇝ ↔ ⇝ Fn dom ⁡ ⇝
9 7 8 mpbi ⊢ ⇝ Fn dom ⁡ ⇝
10 vex ⊢ y ∈ V
11 10 elrn ⊢ y ∈ ran ⁡ ⇝ ↔ ∃ x x ⇝ y
12 climcl ⊢ x ⇝ y → y ∈ ℂ
13 12 exlimiv ⊢ ∃ x x ⇝ y → y ∈ ℂ
14 11 13 sylbi ⊢ y ∈ ran ⁡ ⇝ → y ∈ ℂ
15 14 ssriv ⊢ ran ⁡ ⇝ ⊆ ℂ
16 df-f ⊢ ⇝ : dom ⁡ ⇝ ⟶ ℂ ↔ ⇝ Fn dom ⁡ ⇝ ∧ ran ⁡ ⇝ ⊆ ℂ
17 9 15 16 mpbir2an ⊢ ⇝ : dom ⁡ ⇝ ⟶ ℂ