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

Metamath Proof Explorer

Theorem climdm

Description: Two ways to express that a function has a limit. (The expression ( ~>F ) is sometimes useful as a shorthand for "the unique limit of the function F "). (Contributed by Mario Carneiro, 18-Mar-2014)

		Ref	Expression
	Assertion	climdm	⊢ ( 𝐹 ∈ dom ⇝ ↔ 𝐹 ⇝ ( ⇝ ‘ 𝐹 ) )

Proof

Step	Hyp	Ref	Expression
1		fclim	⊢ ⇝ : dom ⇝ ⟶ ℂ
2		ffun	⊢ ( ⇝ : dom ⇝ ⟶ ℂ → Fun ⇝ )
3		funfvbrb	⊢ ( Fun ⇝ → ( 𝐹 ∈ dom ⇝ ↔ 𝐹 ⇝ ( ⇝ ‘ 𝐹 ) ) )
4	1 2 3	mp2b	⊢ ( 𝐹 ∈ dom ⇝ ↔ 𝐹 ⇝ ( ⇝ ‘ 𝐹 ) )