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