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 e. dom ( ~~>u ` S ) <-> F ( ~~>u ` S ) ( ( ~~>u ` S ) ` F ) )

Proof

Step	Hyp	Ref	Expression
1		ulmrel	|- Rel ( ~~>u ` S )
2		ulmuni	|- ( ( x ( ~~>u ` S ) y /\ x ( ~~>u ` S ) z ) -> y = z )
3	2	ax-gen	|- A. z ( ( x ( ~~>u ` S ) y /\ x ( ~~>u ` S ) z ) -> y = z )
4	3	gen2	|- A. x A. y A. z ( ( x ( ~~>u ` S ) y /\ x ( ~~>u ` S ) z ) -> y = z )
5		dffun2	|- ( Fun ( ~~>u ` S ) <-> ( Rel ( ~~>u ` S ) /\ A. x A. y A. z ( ( x ( ~~>u ` S ) y /\ x ( ~~>u ` S ) z ) -> y = z ) ) )
6	1 4 5	mpbir2an	|- Fun ( ~~>u ` S )
7		funfvbrb	|- ( Fun ( ~~>u ` S ) -> ( F e. dom ( ~~>u ` S ) <-> F ( ~~>u ` S ) ( ( ~~>u ` S ) ` F ) ) )
8	6 7	ax-mp	|- ( F e. dom ( ~~>u ` S ) <-> F ( ~~>u ` S ) ( ( ~~>u ` S ) ` F ) )