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

Metamath Proof Explorer

Theorem limcmo

Description: If B is a limit point of the domain of the function F , then there is at most one limit value of F at B . (Contributed by Mario Carneiro, 25-Dec-2016)

Ref Expression
Hypotheses limcflf.f 
|- ( ph -> F : A --> CC )
limcflf.a 
|- ( ph -> A C_ CC )
limcflf.b 
|- ( ph -> B e. ( ( limPt ` K ) ` A ) )
limcflf.k 
|- K = ( TopOpen ` CCfld )
Assertion limcmo 
|- ( ph -> E* x x e. ( F limCC B ) )

Proof

Step Hyp Ref Expression
1 limcflf.f 
 |-  ( ph -> F : A --> CC )
2 limcflf.a 
 |-  ( ph -> A C_ CC )
3 limcflf.b 
 |-  ( ph -> B e. ( ( limPt ` K ) ` A ) )
4 limcflf.k 
 |-  K = ( TopOpen ` CCfld )
5 4 cnfldhaus 
 |-  K e. Haus
6 eqid 
 |-  ( A \ { B } ) = ( A \ { B } )
7 eqid 
 |-  ( ( ( nei ` K ) ` { B } ) |`t ( A \ { B } ) ) = ( ( ( nei ` K ) ` { B } ) |`t ( A \ { B } ) )
8 1 2 3 4 6 7 limcflflem 
 |-  ( ph -> ( ( ( nei ` K ) ` { B } ) |`t ( A \ { B } ) ) e. ( Fil ` ( A \ { B } ) ) )
9 difss 
 |-  ( A \ { B } ) C_ A
10 fssres 
 |-  ( ( F : A --> CC /\ ( A \ { B } ) C_ A ) -> ( F |` ( A \ { B } ) ) : ( A \ { B } ) --> CC )
11 1 9 10 sylancl 
 |-  ( ph -> ( F |` ( A \ { B } ) ) : ( A \ { B } ) --> CC )
12 4 cnfldtopon 
 |-  K e. ( TopOn ` CC )
13 12 toponunii 
 |-  CC = U. K
14 13 hausflf 
 |-  ( ( K e. Haus /\ ( ( ( nei ` K ) ` { B } ) |`t ( A \ { B } ) ) e. ( Fil ` ( A \ { B } ) ) /\ ( F |` ( A \ { B } ) ) : ( A \ { B } ) --> CC ) -> E* x x e. ( ( K fLimf ( ( ( nei ` K ) ` { B } ) |`t ( A \ { B } ) ) ) ` ( F |` ( A \ { B } ) ) ) )
15 5 8 11 14 mp3an2i 
 |-  ( ph -> E* x x e. ( ( K fLimf ( ( ( nei ` K ) ` { B } ) |`t ( A \ { B } ) ) ) ` ( F |` ( A \ { B } ) ) ) )
16 1 2 3 4 6 7 limcflf 
 |-  ( ph -> ( F limCC B ) = ( ( K fLimf ( ( ( nei ` K ) ` { B } ) |`t ( A \ { B } ) ) ) ` ( F |` ( A \ { B } ) ) ) )
17 16 eleq2d 
 |-  ( ph -> ( x e. ( F limCC B ) <-> x e. ( ( K fLimf ( ( ( nei ` K ) ` { B } ) |`t ( A \ { B } ) ) ) ` ( F |` ( A \ { B } ) ) ) ) )
18 17 mobidv 
 |-  ( ph -> ( E* x x e. ( F limCC B ) <-> E* x x e. ( ( K fLimf ( ( ( nei ` K ) ` { B } ) |`t ( A \ { B } ) ) ) ` ( F |` ( A \ { B } ) ) ) ) )
19 15 18 mpbird 
 |-  ( ph -> E* x x e. ( F limCC B ) )