Metamath Proof Explorer

Theorem uffclsflim

Description: The cluster points of an ultrafilter are its limit points. (Contributed by Jeff Hankins, 11-Dec-2009) (Revised by Mario Carneiro, 26-Aug-2015)

Ref Expression
Assertion uffclsflim 
|- ( F e. ( UFil ` X ) -> ( J fClus F ) = ( J fLim F ) )

Proof

Step Hyp Ref Expression
1 ufilfil 
 |-  ( F e. ( UFil ` X ) -> F e. ( Fil ` X ) )
2 fclsfnflim 
 |-  ( F e. ( Fil ` X ) -> ( x e. ( J fClus F ) <-> E. f e. ( Fil ` X ) ( F C_ f /\ x e. ( J fLim f ) ) ) )
3 1 2 syl 
 |-  ( F e. ( UFil ` X ) -> ( x e. ( J fClus F ) <-> E. f e. ( Fil ` X ) ( F C_ f /\ x e. ( J fLim f ) ) ) )
4 3 biimpa 
 |-  ( ( F e. ( UFil ` X ) /\ x e. ( J fClus F ) ) -> E. f e. ( Fil ` X ) ( F C_ f /\ x e. ( J fLim f ) ) )
5 simprrr 
 |-  ( ( ( F e. ( UFil ` X ) /\ x e. ( J fClus F ) ) /\ ( f e. ( Fil ` X ) /\ ( F C_ f /\ x e. ( J fLim f ) ) ) ) -> x e. ( J fLim f ) )
6 simpll 
 |-  ( ( ( F e. ( UFil ` X ) /\ x e. ( J fClus F ) ) /\ ( f e. ( Fil ` X ) /\ ( F C_ f /\ x e. ( J fLim f ) ) ) ) -> F e. ( UFil ` X ) )
7 simprl 
 |-  ( ( ( F e. ( UFil ` X ) /\ x e. ( J fClus F ) ) /\ ( f e. ( Fil ` X ) /\ ( F C_ f /\ x e. ( J fLim f ) ) ) ) -> f e. ( Fil ` X ) )
8 simprrl 
 |-  ( ( ( F e. ( UFil ` X ) /\ x e. ( J fClus F ) ) /\ ( f e. ( Fil ` X ) /\ ( F C_ f /\ x e. ( J fLim f ) ) ) ) -> F C_ f )
9 ufilmax 
 |-  ( ( F e. ( UFil ` X ) /\ f e. ( Fil ` X ) /\ F C_ f ) -> F = f )
10 6 7 8 9 syl3anc 
 |-  ( ( ( F e. ( UFil ` X ) /\ x e. ( J fClus F ) ) /\ ( f e. ( Fil ` X ) /\ ( F C_ f /\ x e. ( J fLim f ) ) ) ) -> F = f )
11 10 oveq2d 
 |-  ( ( ( F e. ( UFil ` X ) /\ x e. ( J fClus F ) ) /\ ( f e. ( Fil ` X ) /\ ( F C_ f /\ x e. ( J fLim f ) ) ) ) -> ( J fLim F ) = ( J fLim f ) )
12 5 11 eleqtrrd 
 |-  ( ( ( F e. ( UFil ` X ) /\ x e. ( J fClus F ) ) /\ ( f e. ( Fil ` X ) /\ ( F C_ f /\ x e. ( J fLim f ) ) ) ) -> x e. ( J fLim F ) )
13 4 12 rexlimddv 
 |-  ( ( F e. ( UFil ` X ) /\ x e. ( J fClus F ) ) -> x e. ( J fLim F ) )
14 13 ex 
 |-  ( F e. ( UFil ` X ) -> ( x e. ( J fClus F ) -> x e. ( J fLim F ) ) )
15 14 ssrdv 
 |-  ( F e. ( UFil ` X ) -> ( J fClus F ) C_ ( J fLim F ) )
16 flimfcls 
 |-  ( J fLim F ) C_ ( J fClus F )
17 16 a1i 
 |-  ( F e. ( UFil ` X ) -> ( J fLim F ) C_ ( J fClus F ) )
18 15 17 eqssd 
 |-  ( F e. ( UFil ` X ) -> ( J fClus F ) = ( J fLim F ) )