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 ⇝ ⟶ ℂ