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