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

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 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 ) )