Metamath Proof Explorer

Theorem rlimdmafv

Description: Two ways to express that a function has a limit, analogous to rlimdm . (Contributed by Alexander van der Vekens, 27-Nov-2017)

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

Proof

Step Hyp Ref Expression
1 rlimdmafv.1 
 |-  ( ph -> F : A --> CC )
2 rlimdmafv.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 rlimrel 
 |-  Rel ~~>r
7 6 brrelex1i 
 |-  ( F ~~>r x -> F e. _V )
8 7 adantl 
 |-  ( ( ph /\ F ~~>r x ) -> F e. _V )
9 vex 
 |-  x e. _V
10 9 a1i 
 |-  ( ( ph /\ F ~~>r x ) -> x e. _V )
11 breldmg 
 |-  ( ( F e. _V /\ x e. _V /\ F ~~>r x ) -> F e. dom ~~>r )
12 8 10 5 11 syl3anc 
 |-  ( ( ph /\ F ~~>r x ) -> F e. dom ~~>r )
13 breq2 
 |-  ( y = x -> ( F ~~>r y <-> F ~~>r x ) )
14 13 biimprd 
 |-  ( y = x -> ( F ~~>r x -> F ~~>r y ) )
15 14 spimevw 
 |-  ( F ~~>r x -> E. y F ~~>r y )
16 15 adantl 
 |-  ( ( ph /\ F ~~>r x ) -> E. y F ~~>r y )
17 1 adantr 
 |-  ( ( ph /\ F ~~>r x ) -> F : A --> CC )
18 17 adantr 
 |-  ( ( ( ph /\ F ~~>r x ) /\ ( F ~~>r y /\ F ~~>r z ) ) -> F : A --> CC )
19 2 adantr 
 |-  ( ( ph /\ F ~~>r x ) -> sup ( A , RR* , < ) = +oo )
20 19 adantr 
 |-  ( ( ( ph /\ F ~~>r x ) /\ ( F ~~>r y /\ F ~~>r z ) ) -> sup ( A , RR* , < ) = +oo )
21 simprl 
 |-  ( ( ( ph /\ F ~~>r x ) /\ ( F ~~>r y /\ F ~~>r z ) ) -> F ~~>r y )
22 simprr 
 |-  ( ( ( ph /\ F ~~>r x ) /\ ( F ~~>r y /\ F ~~>r z ) ) -> F ~~>r z )
23 18 20 21 22 rlimuni 
 |-  ( ( ( ph /\ F ~~>r x ) /\ ( F ~~>r y /\ F ~~>r z ) ) -> y = z )
24 23 ex 
 |-  ( ( ph /\ F ~~>r x ) -> ( ( F ~~>r y /\ F ~~>r z ) -> y = z ) )
25 24 alrimivv 
 |-  ( ( ph /\ F ~~>r x ) -> A. y A. z ( ( F ~~>r y /\ F ~~>r z ) -> y = z ) )
26 breq2 
 |-  ( y = z -> ( F ~~>r y <-> F ~~>r z ) )
27 26 eu4 
 |-  ( E! y F ~~>r y <-> ( E. y F ~~>r y /\ A. y A. z ( ( F ~~>r y /\ F ~~>r z ) -> y = z ) ) )
28 16 25 27 sylanbrc 
 |-  ( ( ph /\ F ~~>r x ) -> E! y F ~~>r y )
29 dfdfat2 
 |-  ( ~~>r defAt F <-> ( F e. dom ~~>r /\ E! y F ~~>r y ) )
30 12 28 29 sylanbrc 
 |-  ( ( ph /\ F ~~>r x ) -> ~~>r defAt F )
31 afvfundmfveq 
 |-  ( ~~>r defAt F -> ( ~~>r ''' F ) = ( ~~>r ` F ) )
32 30 31 syl 
 |-  ( ( ph /\ F ~~>r x ) -> ( ~~>r ''' F ) = ( ~~>r ` F ) )
33 df-fv 
 |-  ( ~~>r ` F ) = ( iota w F ~~>r w )
34 1 adantr 
 |-  ( ( ph /\ ( F ~~>r x /\ F ~~>r w ) ) -> F : A --> CC )
35 2 adantr 
 |-  ( ( ph /\ ( F ~~>r x /\ F ~~>r w ) ) -> sup ( A , RR* , < ) = +oo )
36 simprr 
 |-  ( ( ph /\ ( F ~~>r x /\ F ~~>r w ) ) -> F ~~>r w )
37 simprl 
 |-  ( ( ph /\ ( F ~~>r x /\ F ~~>r w ) ) -> F ~~>r x )
38 34 35 36 37 rlimuni 
 |-  ( ( ph /\ ( F ~~>r x /\ F ~~>r w ) ) -> w = x )
39 38 expr 
 |-  ( ( ph /\ F ~~>r x ) -> ( F ~~>r w -> w = x ) )
40 breq2 
 |-  ( w = x -> ( F ~~>r w <-> F ~~>r x ) )
41 5 40 syl5ibrcom 
 |-  ( ( ph /\ F ~~>r x ) -> ( w = x -> F ~~>r w ) )
42 39 41 impbid 
 |-  ( ( ph /\ F ~~>r x ) -> ( F ~~>r w <-> w = x ) )
43 42 adantr 
 |-  ( ( ( ph /\ F ~~>r x ) /\ x e. _V ) -> ( F ~~>r w <-> w = x ) )
44 43 iota5 
 |-  ( ( ( ph /\ F ~~>r x ) /\ x e. _V ) -> ( iota w F ~~>r w ) = x )
45 44 elvd 
 |-  ( ( ph /\ F ~~>r x ) -> ( iota w F ~~>r w ) = x )
46 33 45 syl5eq 
 |-  ( ( ph /\ F ~~>r x ) -> ( ~~>r ` F ) = x )
47 32 46 eqtrd 
 |-  ( ( ph /\ F ~~>r x ) -> ( ~~>r ''' F ) = x )
48 5 47 breqtrrd 
 |-  ( ( ph /\ F ~~>r x ) -> F ~~>r ( ~~>r ''' F ) )
49 48 ex 
 |-  ( ph -> ( F ~~>r x -> F ~~>r ( ~~>r ''' F ) ) )
50 49 exlimdv 
 |-  ( ph -> ( E. x F ~~>r x -> F ~~>r ( ~~>r ''' F ) ) )
51 4 50 syl5 
 |-  ( ph -> ( F e. dom ~~>r -> F ~~>r ( ~~>r ''' F ) ) )
52 6 releldmi 
 |-  ( F ~~>r ( ~~>r ''' F ) -> F e. dom ~~>r )
53 51 52 impbid1 
 |-  ( ph -> ( F e. dom ~~>r <-> F ~~>r ( ~~>r ''' F ) ) )