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

Metamath Proof Explorer

Theorem rlimdm

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

Ref Expression
Hypotheses rlimuni.1 
|- ( ph -> F : A --> CC )
rlimuni.2 
|- ( ph -> sup ( A , RR* , < ) = +oo )
Assertion rlimdm 
|- ( ph -> ( F e. dom ~~>r <-> F ~~>r ( ~~>r ` F ) ) )

Proof

Step Hyp Ref Expression
1 rlimuni.1 
 |-  ( ph -> F : A --> CC )
2 rlimuni.2 
 |-  ( ph -> sup ( A , RR* , < ) = +oo )
3 eldmg 
 |-  ( F e. dom ~~>r -> ( F e. dom ~~>r <-> E. x F ~~>r x ) )
4 3 ibi 
 |-  ( F e. dom ~~>r -> E. x F ~~>r x )
5 simpr 
 |-  ( ( ph /\ F ~~>r x ) -> F ~~>r x )
6 df-fv 
 |-  ( ~~>r ` F ) = ( iota y F ~~>r y )
7 1 adantr 
 |-  ( ( ph /\ ( F ~~>r x /\ F ~~>r y ) ) -> F : A --> CC )
8 2 adantr 
 |-  ( ( ph /\ ( F ~~>r x /\ F ~~>r y ) ) -> sup ( A , RR* , < ) = +oo )
9 simprr 
 |-  ( ( ph /\ ( F ~~>r x /\ F ~~>r y ) ) -> F ~~>r y )
10 simprl 
 |-  ( ( ph /\ ( F ~~>r x /\ F ~~>r y ) ) -> F ~~>r x )
11 7 8 9 10 rlimuni 
 |-  ( ( ph /\ ( F ~~>r x /\ F ~~>r y ) ) -> y = x )
12 11 expr 
 |-  ( ( ph /\ F ~~>r x ) -> ( F ~~>r y -> y = x ) )
13 breq2 
 |-  ( y = x -> ( F ~~>r y <-> F ~~>r x ) )
14 5 13 syl5ibrcom 
 |-  ( ( ph /\ F ~~>r x ) -> ( y = x -> F ~~>r y ) )
15 12 14 impbid 
 |-  ( ( ph /\ F ~~>r x ) -> ( F ~~>r y <-> y = x ) )
16 15 adantr 
 |-  ( ( ( ph /\ F ~~>r x ) /\ x e. _V ) -> ( F ~~>r y <-> y = x ) )
17 16 iota5 
 |-  ( ( ( ph /\ F ~~>r x ) /\ x e. _V ) -> ( iota y F ~~>r y ) = x )
18 17 elvd 
 |-  ( ( ph /\ F ~~>r x ) -> ( iota y F ~~>r y ) = x )
19 6 18 eqtrid 
 |-  ( ( ph /\ F ~~>r x ) -> ( ~~>r ` F ) = x )
20 5 19 breqtrrd 
 |-  ( ( ph /\ F ~~>r x ) -> F ~~>r ( ~~>r ` F ) )
21 20 ex 
 |-  ( ph -> ( F ~~>r x -> F ~~>r ( ~~>r ` F ) ) )
22 21 exlimdv 
 |-  ( ph -> ( E. x F ~~>r x -> F ~~>r ( ~~>r ` F ) ) )
23 4 22 syl5 
 |-  ( ph -> ( F e. dom ~~>r -> F ~~>r ( ~~>r ` F ) ) )
24 rlimrel 
 |-  Rel ~~>r
25 24 releldmi 
 |-  ( F ~~>r ( ~~>r ` F ) -> F e. dom ~~>r )
26 23 25 impbid1 
 |-  ( ph -> ( F e. dom ~~>r <-> F ~~>r ( ~~>r ` F ) ) )