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 ⊢ ( ( 𝑥 ⇝ 𝑦 ∧ 𝑥 ⇝ 𝑧 ) → 𝑦 = 𝑧 )
3 2 ax-gen ⊢ ∀ 𝑧 ( ( 𝑥 ⇝ 𝑦 ∧ 𝑥 ⇝ 𝑧 ) → 𝑦 = 𝑧 )
4 3 ax-gen ⊢ ∀ 𝑦 ∀ 𝑧 ( ( 𝑥 ⇝ 𝑦 ∧ 𝑥 ⇝ 𝑧 ) → 𝑦 = 𝑧 )
5 4 ax-gen ⊢ ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( ( 𝑥 ⇝ 𝑦 ∧ 𝑥 ⇝ 𝑧 ) → 𝑦 = 𝑧 )
6 dffun2 ⊢ ( Fun ⇝ ↔ ( Rel ⇝ ∧ ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( ( 𝑥 ⇝ 𝑦 ∧ 𝑥 ⇝ 𝑧 ) → 𝑦 = 𝑧 ) ) )
7 1 5 6 mpbir2an ⊢ Fun ⇝
8 funfn ⊢ ( Fun ⇝ ↔ ⇝ Fn dom ⇝ )
9 7 8 mpbi ⊢ ⇝ Fn dom ⇝
10 vex ⊢ 𝑦 ∈ V
11 10 elrn ⊢ ( 𝑦 ∈ ran ⇝ ↔ ∃ 𝑥 𝑥 ⇝ 𝑦 )
12 climcl ⊢ ( 𝑥 ⇝ 𝑦 → 𝑦 ∈ ℂ )
13 12 exlimiv ⊢ ( ∃ 𝑥 𝑥 ⇝ 𝑦 → 𝑦 ∈ ℂ )
14 11 13 sylbi ⊢ ( 𝑦 ∈ ran ⇝ → 𝑦 ∈ ℂ )
15 14 ssriv ⊢ ran ⇝ ⊆ ℂ
16 df-f ⊢ ( ⇝ : dom ⇝ ⟶ ℂ ↔ ( ⇝ Fn dom ⇝ ∧ ran ⇝ ⊆ ℂ ) )
17 9 15 16 mpbir2an ⊢ ⇝ : dom ⇝ ⟶ ℂ