Metamath Proof Explorer

Theorem rlimdmafv2

Description: Two ways to express that a function has a limit, analogous to rlimdm . (Contributed by AV, 5-Sep-2022)

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

Proof

Step Hyp Ref Expression
1 rlimdmafv2.1 
 |-  ( ph -> F : A --> CC )
2 rlimdmafv2.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 dfatafv2iota 
 |-  ( ~~>r defAt F -> ( ~~>r '''' F ) = ( iota w F ~~>r w ) )
32 30 31 syl 
 |-  ( ( ph /\ F ~~>r x ) -> ( ~~>r '''' F ) = ( iota w F ~~>r w ) )
33 1 adantr 
 |-  ( ( ph /\ ( F ~~>r x /\ F ~~>r w ) ) -> F : A --> CC )
34 2 adantr 
 |-  ( ( ph /\ ( F ~~>r x /\ F ~~>r w ) ) -> sup ( A , RR* , < ) = +oo )
35 simprr 
 |-  ( ( ph /\ ( F ~~>r x /\ F ~~>r w ) ) -> F ~~>r w )
36 simprl 
 |-  ( ( ph /\ ( F ~~>r x /\ F ~~>r w ) ) -> F ~~>r x )
37 33 34 35 36 rlimuni 
 |-  ( ( ph /\ ( F ~~>r x /\ F ~~>r w ) ) -> w = x )
38 37 expr 
 |-  ( ( ph /\ F ~~>r x ) -> ( F ~~>r w -> w = x ) )
39 breq2 
 |-  ( w = x -> ( F ~~>r w <-> F ~~>r x ) )
40 5 39 syl5ibrcom 
 |-  ( ( ph /\ F ~~>r x ) -> ( w = x -> F ~~>r w ) )
41 38 40 impbid 
 |-  ( ( ph /\ F ~~>r x ) -> ( F ~~>r w <-> w = x ) )
42 41 adantr 
 |-  ( ( ( ph /\ F ~~>r x ) /\ x e. _V ) -> ( F ~~>r w <-> w = x ) )
43 42 iota5 
 |-  ( ( ( ph /\ F ~~>r x ) /\ x e. _V ) -> ( iota w F ~~>r w ) = x )
44 43 elvd 
 |-  ( ( ph /\ F ~~>r x ) -> ( iota w F ~~>r w ) = x )
45 32 44 eqtrd 
 |-  ( ( ph /\ F ~~>r x ) -> ( ~~>r '''' F ) = x )
46 5 45 breqtrrd 
 |-  ( ( ph /\ F ~~>r x ) -> F ~~>r ( ~~>r '''' F ) )
47 46 ex 
 |-  ( ph -> ( F ~~>r x -> F ~~>r ( ~~>r '''' F ) ) )
48 47 exlimdv 
 |-  ( ph -> ( E. x F ~~>r x -> F ~~>r ( ~~>r '''' F ) ) )
49 4 48 syl5 
 |-  ( ph -> ( F e. dom ~~>r -> F ~~>r ( ~~>r '''' F ) ) )
50 6 releldmi 
 |-  ( F ~~>r ( ~~>r '''' F ) -> F e. dom ~~>r )
51 49 50 impbid1 
 |-  ( ph -> ( F e. dom ~~>r <-> F ~~>r ( ~~>r '''' F ) ) )