Metamath Proof Explorer

Theorem ulmdm

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

		Ref	Expression
	Assertion	ulmdm	$⊢ F \in dom \underset{u}{⇝} (S) \leftrightarrow F \underset{u}{⇝} (S) \underset{u}{⇝} (S) (F)$

Proof

Step	Hyp	Ref	Expression
1		ulmrel	$⊢ Rel \underset{u}{⇝} (S)$
2		ulmuni	$⊢ (x \underset{u}{⇝} (S) y \land x \underset{u}{⇝} (S) z) \to y = z$
3	2	ax-gen	$⊢ \forall z ((x \underset{u}{⇝} (S) y \land x \underset{u}{⇝} (S) z) \to y = z)$
4	3	gen2	$⊢ \forall x \forall y \forall z ((x \underset{u}{⇝} (S) y \land x \underset{u}{⇝} (S) z) \to y = z)$
5		dffun2	$⊢ Fun \underset{u}{⇝} (S) \leftrightarrow (Rel \underset{u}{⇝} (S) \land \forall x \forall y \forall z ((x \underset{u}{⇝} (S) y \land x \underset{u}{⇝} (S) z) \to y = z))$
6	1 4 5	mpbir2an	$⊢ Fun \underset{u}{⇝} (S)$
7		funfvbrb	$⊢ Fun \underset{u}{⇝} (S) \to (F \in dom \underset{u}{⇝} (S) \leftrightarrow F \underset{u}{⇝} (S) \underset{u}{⇝} (S) (F))$
8	6 7	ax-mp	$⊢ F \in dom \underset{u}{⇝} (S) \leftrightarrow F \underset{u}{⇝} (S) \underset{u}{⇝} (S) (F)$