Metamath Proof Explorer

Theorem cfilfcls

Description: Similar to ultrafilters ( uffclsflim ), the cluster points and limit points of a Cauchy filter coincide. (Contributed by Mario Carneiro, 15-Oct-2015)

Ref Expression
Hypotheses cfilfcls.1 
|- J = ( MetOpen ` D )
cfilfcls.2 
|- X = dom dom D
Assertion cfilfcls 
|- ( F e. ( CauFil ` D ) -> ( J fClus F ) = ( J fLim F ) )

Proof

Step Hyp Ref Expression
1 cfilfcls.1 
 |-  J = ( MetOpen ` D )
2 cfilfcls.2 
 |-  X = dom dom D
3 eqid 
 |-  U. J = U. J
4 3 fclselbas 
 |-  ( x e. ( J fClus F ) -> x e. U. J )
5 4 adantl 
 |-  ( ( F e. ( CauFil ` D ) /\ x e. ( J fClus F ) ) -> x e. U. J )
6 df-cfil 
 |-  CauFil = ( d e. U. ran *Met |-> { f e. ( Fil ` dom dom d ) | A. x e. RR+ E. y e. f ( d " ( y X. y ) ) C_ ( 0 [,) x ) } )
7 6 mptrcl 
 |-  ( F e. ( CauFil ` D ) -> D e. U. ran *Met )
8 xmetunirn 
 |-  ( D e. U. ran *Met <-> D e. ( *Met ` dom dom D ) )
9 7 8 sylib 
 |-  ( F e. ( CauFil ` D ) -> D e. ( *Met ` dom dom D ) )
10 2 fveq2i 
 |-  ( *Met ` X ) = ( *Met ` dom dom D )
11 9 10 eleqtrrdi 
 |-  ( F e. ( CauFil ` D ) -> D e. ( *Met ` X ) )
12 11 adantr 
 |-  ( ( F e. ( CauFil ` D ) /\ x e. ( J fClus F ) ) -> D e. ( *Met ` X ) )
13 1 mopntopon 
 |-  ( D e. ( *Met ` X ) -> J e. ( TopOn ` X ) )
14 12 13 syl 
 |-  ( ( F e. ( CauFil ` D ) /\ x e. ( J fClus F ) ) -> J e. ( TopOn ` X ) )
15 toponuni 
 |-  ( J e. ( TopOn ` X ) -> X = U. J )
16 14 15 syl 
 |-  ( ( F e. ( CauFil ` D ) /\ x e. ( J fClus F ) ) -> X = U. J )
17 5 16 eleqtrrd 
 |-  ( ( F e. ( CauFil ` D ) /\ x e. ( J fClus F ) ) -> x e. X )
18 1 mopni2 
 |-  ( ( D e. ( *Met ` X ) /\ y e. J /\ x e. y ) -> E. r e. RR+ ( x ( ball ` D ) r ) C_ y )
19 18 3expb 
 |-  ( ( D e. ( *Met ` X ) /\ ( y e. J /\ x e. y ) ) -> E. r e. RR+ ( x ( ball ` D ) r ) C_ y )
20 12 19 sylan 
 |-  ( ( ( F e. ( CauFil ` D ) /\ x e. ( J fClus F ) ) /\ ( y e. J /\ x e. y ) ) -> E. r e. RR+ ( x ( ball ` D ) r ) C_ y )
21 cfilfil 
 |-  ( ( D e. ( *Met ` X ) /\ F e. ( CauFil ` D ) ) -> F e. ( Fil ` X ) )
22 11 21 mpancom 
 |-  ( F e. ( CauFil ` D ) -> F e. ( Fil ` X ) )
23 22 adantr 
 |-  ( ( F e. ( CauFil ` D ) /\ x e. ( J fClus F ) ) -> F e. ( Fil ` X ) )
24 23 ad2antrr 
 |-  ( ( ( ( F e. ( CauFil ` D ) /\ x e. ( J fClus F ) ) /\ ( y e. J /\ x e. y ) ) /\ ( r e. RR+ /\ ( x ( ball ` D ) r ) C_ y ) ) -> F e. ( Fil ` X ) )
25 12 adantr 
 |-  ( ( ( F e. ( CauFil ` D ) /\ x e. ( J fClus F ) ) /\ r e. RR+ ) -> D e. ( *Met ` X ) )
26 simpll 
 |-  ( ( ( F e. ( CauFil ` D ) /\ x e. ( J fClus F ) ) /\ r e. RR+ ) -> F e. ( CauFil ` D ) )
27 rphalfcl 
 |-  ( r e. RR+ -> ( r / 2 ) e. RR+ )
28 27 adantl 
 |-  ( ( ( F e. ( CauFil ` D ) /\ x e. ( J fClus F ) ) /\ r e. RR+ ) -> ( r / 2 ) e. RR+ )
29 rphalfcl 
 |-  ( ( r / 2 ) e. RR+ -> ( ( r / 2 ) / 2 ) e. RR+ )
30 28 29 syl 
 |-  ( ( ( F e. ( CauFil ` D ) /\ x e. ( J fClus F ) ) /\ r e. RR+ ) -> ( ( r / 2 ) / 2 ) e. RR+ )
31 cfil3i 
 |-  ( ( D e. ( *Met ` X ) /\ F e. ( CauFil ` D ) /\ ( ( r / 2 ) / 2 ) e. RR+ ) -> E. y e. X ( y ( ball ` D ) ( ( r / 2 ) / 2 ) ) e. F )
32 25 26 30 31 syl3anc 
 |-  ( ( ( F e. ( CauFil ` D ) /\ x e. ( J fClus F ) ) /\ r e. RR+ ) -> E. y e. X ( y ( ball ` D ) ( ( r / 2 ) / 2 ) ) e. F )
33 23 ad2antrr 
 |-  ( ( ( ( F e. ( CauFil ` D ) /\ x e. ( J fClus F ) ) /\ r e. RR+ ) /\ ( y e. X /\ ( y ( ball ` D ) ( ( r / 2 ) / 2 ) ) e. F ) ) -> F e. ( Fil ` X ) )
34 simprr 
 |-  ( ( ( ( F e. ( CauFil ` D ) /\ x e. ( J fClus F ) ) /\ r e. RR+ ) /\ ( y e. X /\ ( y ( ball ` D ) ( ( r / 2 ) / 2 ) ) e. F ) ) -> ( y ( ball ` D ) ( ( r / 2 ) / 2 ) ) e. F )
35 25 adantr 
 |-  ( ( ( ( F e. ( CauFil ` D ) /\ x e. ( J fClus F ) ) /\ r e. RR+ ) /\ ( y e. X /\ ( y ( ball ` D ) ( ( r / 2 ) / 2 ) ) e. F ) ) -> D e. ( *Met ` X ) )
36 17 ad2antrr 
 |-  ( ( ( ( F e. ( CauFil ` D ) /\ x e. ( J fClus F ) ) /\ r e. RR+ ) /\ ( y e. X /\ ( y ( ball ` D ) ( ( r / 2 ) / 2 ) ) e. F ) ) -> x e. X )
37 rpxr 
 |-  ( r e. RR+ -> r e. RR* )
38 37 ad2antlr 
 |-  ( ( ( ( F e. ( CauFil ` D ) /\ x e. ( J fClus F ) ) /\ r e. RR+ ) /\ ( y e. X /\ ( y ( ball ` D ) ( ( r / 2 ) / 2 ) ) e. F ) ) -> r e. RR* )
39 blssm 
 |-  ( ( D e. ( *Met ` X ) /\ x e. X /\ r e. RR* ) -> ( x ( ball ` D ) r ) C_ X )
40 35 36 38 39 syl3anc 
 |-  ( ( ( ( F e. ( CauFil ` D ) /\ x e. ( J fClus F ) ) /\ r e. RR+ ) /\ ( y e. X /\ ( y ( ball ` D ) ( ( r / 2 ) / 2 ) ) e. F ) ) -> ( x ( ball ` D ) r ) C_ X )
41 simpllr 
 |-  ( ( ( ( F e. ( CauFil ` D ) /\ x e. ( J fClus F ) ) /\ r e. RR+ ) /\ ( y e. X /\ ( y ( ball ` D ) ( ( r / 2 ) / 2 ) ) e. F ) ) -> x e. ( J fClus F ) )
42 28 adantr 
 |-  ( ( ( ( F e. ( CauFil ` D ) /\ x e. ( J fClus F ) ) /\ r e. RR+ ) /\ ( y e. X /\ ( y ( ball ` D ) ( ( r / 2 ) / 2 ) ) e. F ) ) -> ( r / 2 ) e. RR+ )
43 42 rpxrd 
 |-  ( ( ( ( F e. ( CauFil ` D ) /\ x e. ( J fClus F ) ) /\ r e. RR+ ) /\ ( y e. X /\ ( y ( ball ` D ) ( ( r / 2 ) / 2 ) ) e. F ) ) -> ( r / 2 ) e. RR* )
44 1 blopn 
 |-  ( ( D e. ( *Met ` X ) /\ x e. X /\ ( r / 2 ) e. RR* ) -> ( x ( ball ` D ) ( r / 2 ) ) e. J )
45 35 36 43 44 syl3anc 
 |-  ( ( ( ( F e. ( CauFil ` D ) /\ x e. ( J fClus F ) ) /\ r e. RR+ ) /\ ( y e. X /\ ( y ( ball ` D ) ( ( r / 2 ) / 2 ) ) e. F ) ) -> ( x ( ball ` D ) ( r / 2 ) ) e. J )
46 blcntr 
 |-  ( ( D e. ( *Met ` X ) /\ x e. X /\ ( r / 2 ) e. RR+ ) -> x e. ( x ( ball ` D ) ( r / 2 ) ) )
47 35 36 42 46 syl3anc 
 |-  ( ( ( ( F e. ( CauFil ` D ) /\ x e. ( J fClus F ) ) /\ r e. RR+ ) /\ ( y e. X /\ ( y ( ball ` D ) ( ( r / 2 ) / 2 ) ) e. F ) ) -> x e. ( x ( ball ` D ) ( r / 2 ) ) )
48 fclsopni 
 |-  ( ( x e. ( J fClus F ) /\ ( ( x ( ball ` D ) ( r / 2 ) ) e. J /\ x e. ( x ( ball ` D ) ( r / 2 ) ) /\ ( y ( ball ` D ) ( ( r / 2 ) / 2 ) ) e. F ) ) -> ( ( x ( ball ` D ) ( r / 2 ) ) i^i ( y ( ball ` D ) ( ( r / 2 ) / 2 ) ) ) =/= (/) )
49 41 45 47 34 48 syl13anc 
 |-  ( ( ( ( F e. ( CauFil ` D ) /\ x e. ( J fClus F ) ) /\ r e. RR+ ) /\ ( y e. X /\ ( y ( ball ` D ) ( ( r / 2 ) / 2 ) ) e. F ) ) -> ( ( x ( ball ` D ) ( r / 2 ) ) i^i ( y ( ball ` D ) ( ( r / 2 ) / 2 ) ) ) =/= (/) )
50 n0 
 |-  ( ( ( x ( ball ` D ) ( r / 2 ) ) i^i ( y ( ball ` D ) ( ( r / 2 ) / 2 ) ) ) =/= (/) <-> E. z z e. ( ( x ( ball ` D ) ( r / 2 ) ) i^i ( y ( ball ` D ) ( ( r / 2 ) / 2 ) ) ) )
51 49 50 sylib 
 |-  ( ( ( ( F e. ( CauFil ` D ) /\ x e. ( J fClus F ) ) /\ r e. RR+ ) /\ ( y e. X /\ ( y ( ball ` D ) ( ( r / 2 ) / 2 ) ) e. F ) ) -> E. z z e. ( ( x ( ball ` D ) ( r / 2 ) ) i^i ( y ( ball ` D ) ( ( r / 2 ) / 2 ) ) ) )
52 elin 
 |-  ( z e. ( ( x ( ball ` D ) ( r / 2 ) ) i^i ( y ( ball ` D ) ( ( r / 2 ) / 2 ) ) ) <-> ( z e. ( x ( ball ` D ) ( r / 2 ) ) /\ z e. ( y ( ball ` D ) ( ( r / 2 ) / 2 ) ) ) )
53 35 adantr 
 |-  ( ( ( ( ( F e. ( CauFil ` D ) /\ x e. ( J fClus F ) ) /\ r e. RR+ ) /\ ( y e. X /\ ( y ( ball ` D ) ( ( r / 2 ) / 2 ) ) e. F ) ) /\ ( z e. ( x ( ball ` D ) ( r / 2 ) ) /\ z e. ( y ( ball ` D ) ( ( r / 2 ) / 2 ) ) ) ) -> D e. ( *Met ` X ) )
54 simplrl 
 |-  ( ( ( ( ( F e. ( CauFil ` D ) /\ x e. ( J fClus F ) ) /\ r e. RR+ ) /\ ( y e. X /\ ( y ( ball ` D ) ( ( r / 2 ) / 2 ) ) e. F ) ) /\ ( z e. ( x ( ball ` D ) ( r / 2 ) ) /\ z e. ( y ( ball ` D ) ( ( r / 2 ) / 2 ) ) ) ) -> y e. X )
55 42 adantr 
 |-  ( ( ( ( ( F e. ( CauFil ` D ) /\ x e. ( J fClus F ) ) /\ r e. RR+ ) /\ ( y e. X /\ ( y ( ball ` D ) ( ( r / 2 ) / 2 ) ) e. F ) ) /\ ( z e. ( x ( ball ` D ) ( r / 2 ) ) /\ z e. ( y ( ball ` D ) ( ( r / 2 ) / 2 ) ) ) ) -> ( r / 2 ) e. RR+ )
56 55 rpred 
 |-  ( ( ( ( ( F e. ( CauFil ` D ) /\ x e. ( J fClus F ) ) /\ r e. RR+ ) /\ ( y e. X /\ ( y ( ball ` D ) ( ( r / 2 ) / 2 ) ) e. F ) ) /\ ( z e. ( x ( ball ` D ) ( r / 2 ) ) /\ z e. ( y ( ball ` D ) ( ( r / 2 ) / 2 ) ) ) ) -> ( r / 2 ) e. RR )
57 simprr 
 |-  ( ( ( ( ( F e. ( CauFil ` D ) /\ x e. ( J fClus F ) ) /\ r e. RR+ ) /\ ( y e. X /\ ( y ( ball ` D ) ( ( r / 2 ) / 2 ) ) e. F ) ) /\ ( z e. ( x ( ball ` D ) ( r / 2 ) ) /\ z e. ( y ( ball ` D ) ( ( r / 2 ) / 2 ) ) ) ) -> z e. ( y ( ball ` D ) ( ( r / 2 ) / 2 ) ) )
58 blhalf 
 |-  ( ( ( D e. ( *Met ` X ) /\ y e. X ) /\ ( ( r / 2 ) e. RR /\ z e. ( y ( ball ` D ) ( ( r / 2 ) / 2 ) ) ) ) -> ( y ( ball ` D ) ( ( r / 2 ) / 2 ) ) C_ ( z ( ball ` D ) ( r / 2 ) ) )
59 53 54 56 57 58 syl22anc 
 |-  ( ( ( ( ( F e. ( CauFil ` D ) /\ x e. ( J fClus F ) ) /\ r e. RR+ ) /\ ( y e. X /\ ( y ( ball ` D ) ( ( r / 2 ) / 2 ) ) e. F ) ) /\ ( z e. ( x ( ball ` D ) ( r / 2 ) ) /\ z e. ( y ( ball ` D ) ( ( r / 2 ) / 2 ) ) ) ) -> ( y ( ball ` D ) ( ( r / 2 ) / 2 ) ) C_ ( z ( ball ` D ) ( r / 2 ) ) )
60 blssm 
 |-  ( ( D e. ( *Met ` X ) /\ x e. X /\ ( r / 2 ) e. RR* ) -> ( x ( ball ` D ) ( r / 2 ) ) C_ X )
61 35 36 43 60 syl3anc 
 |-  ( ( ( ( F e. ( CauFil ` D ) /\ x e. ( J fClus F ) ) /\ r e. RR+ ) /\ ( y e. X /\ ( y ( ball ` D ) ( ( r / 2 ) / 2 ) ) e. F ) ) -> ( x ( ball ` D ) ( r / 2 ) ) C_ X )
62 61 sselda 
 |-  ( ( ( ( ( F e. ( CauFil ` D ) /\ x e. ( J fClus F ) ) /\ r e. RR+ ) /\ ( y e. X /\ ( y ( ball ` D ) ( ( r / 2 ) / 2 ) ) e. F ) ) /\ z e. ( x ( ball ` D ) ( r / 2 ) ) ) -> z e. X )
63 62 adantrr 
 |-  ( ( ( ( ( F e. ( CauFil ` D ) /\ x e. ( J fClus F ) ) /\ r e. RR+ ) /\ ( y e. X /\ ( y ( ball ` D ) ( ( r / 2 ) / 2 ) ) e. F ) ) /\ ( z e. ( x ( ball ` D ) ( r / 2 ) ) /\ z e. ( y ( ball ` D ) ( ( r / 2 ) / 2 ) ) ) ) -> z e. X )
64 simpllr 
 |-  ( ( ( ( ( F e. ( CauFil ` D ) /\ x e. ( J fClus F ) ) /\ r e. RR+ ) /\ ( y e. X /\ ( y ( ball ` D ) ( ( r / 2 ) / 2 ) ) e. F ) ) /\ ( z e. ( x ( ball ` D ) ( r / 2 ) ) /\ z e. ( y ( ball ` D ) ( ( r / 2 ) / 2 ) ) ) ) -> r e. RR+ )
65 64 rpred 
 |-  ( ( ( ( ( F e. ( CauFil ` D ) /\ x e. ( J fClus F ) ) /\ r e. RR+ ) /\ ( y e. X /\ ( y ( ball ` D ) ( ( r / 2 ) / 2 ) ) e. F ) ) /\ ( z e. ( x ( ball ` D ) ( r / 2 ) ) /\ z e. ( y ( ball ` D ) ( ( r / 2 ) / 2 ) ) ) ) -> r e. RR )
66 simprl 
 |-  ( ( ( ( ( F e. ( CauFil ` D ) /\ x e. ( J fClus F ) ) /\ r e. RR+ ) /\ ( y e. X /\ ( y ( ball ` D ) ( ( r / 2 ) / 2 ) ) e. F ) ) /\ ( z e. ( x ( ball ` D ) ( r / 2 ) ) /\ z e. ( y ( ball ` D ) ( ( r / 2 ) / 2 ) ) ) ) -> z e. ( x ( ball ` D ) ( r / 2 ) ) )
67 55 rpxrd 
 |-  ( ( ( ( ( F e. ( CauFil ` D ) /\ x e. ( J fClus F ) ) /\ r e. RR+ ) /\ ( y e. X /\ ( y ( ball ` D ) ( ( r / 2 ) / 2 ) ) e. F ) ) /\ ( z e. ( x ( ball ` D ) ( r / 2 ) ) /\ z e. ( y ( ball ` D ) ( ( r / 2 ) / 2 ) ) ) ) -> ( r / 2 ) e. RR* )
68 36 adantr 
 |-  ( ( ( ( ( F e. ( CauFil ` D ) /\ x e. ( J fClus F ) ) /\ r e. RR+ ) /\ ( y e. X /\ ( y ( ball ` D ) ( ( r / 2 ) / 2 ) ) e. F ) ) /\ ( z e. ( x ( ball ` D ) ( r / 2 ) ) /\ z e. ( y ( ball ` D ) ( ( r / 2 ) / 2 ) ) ) ) -> x e. X )
69 blcom 
 |-  ( ( ( D e. ( *Met ` X ) /\ ( r / 2 ) e. RR* ) /\ ( x e. X /\ z e. X ) ) -> ( z e. ( x ( ball ` D ) ( r / 2 ) ) <-> x e. ( z ( ball ` D ) ( r / 2 ) ) ) )
70 53 67 68 63 69 syl22anc 
 |-  ( ( ( ( ( F e. ( CauFil ` D ) /\ x e. ( J fClus F ) ) /\ r e. RR+ ) /\ ( y e. X /\ ( y ( ball ` D ) ( ( r / 2 ) / 2 ) ) e. F ) ) /\ ( z e. ( x ( ball ` D ) ( r / 2 ) ) /\ z e. ( y ( ball ` D ) ( ( r / 2 ) / 2 ) ) ) ) -> ( z e. ( x ( ball ` D ) ( r / 2 ) ) <-> x e. ( z ( ball ` D ) ( r / 2 ) ) ) )
71 66 70 mpbid 
 |-  ( ( ( ( ( F e. ( CauFil ` D ) /\ x e. ( J fClus F ) ) /\ r e. RR+ ) /\ ( y e. X /\ ( y ( ball ` D ) ( ( r / 2 ) / 2 ) ) e. F ) ) /\ ( z e. ( x ( ball ` D ) ( r / 2 ) ) /\ z e. ( y ( ball ` D ) ( ( r / 2 ) / 2 ) ) ) ) -> x e. ( z ( ball ` D ) ( r / 2 ) ) )
72 blhalf 
 |-  ( ( ( D e. ( *Met ` X ) /\ z e. X ) /\ ( r e. RR /\ x e. ( z ( ball ` D ) ( r / 2 ) ) ) ) -> ( z ( ball ` D ) ( r / 2 ) ) C_ ( x ( ball ` D ) r ) )
73 53 63 65 71 72 syl22anc 
 |-  ( ( ( ( ( F e. ( CauFil ` D ) /\ x e. ( J fClus F ) ) /\ r e. RR+ ) /\ ( y e. X /\ ( y ( ball ` D ) ( ( r / 2 ) / 2 ) ) e. F ) ) /\ ( z e. ( x ( ball ` D ) ( r / 2 ) ) /\ z e. ( y ( ball ` D ) ( ( r / 2 ) / 2 ) ) ) ) -> ( z ( ball ` D ) ( r / 2 ) ) C_ ( x ( ball ` D ) r ) )
74 59 73 sstrd 
 |-  ( ( ( ( ( F e. ( CauFil ` D ) /\ x e. ( J fClus F ) ) /\ r e. RR+ ) /\ ( y e. X /\ ( y ( ball ` D ) ( ( r / 2 ) / 2 ) ) e. F ) ) /\ ( z e. ( x ( ball ` D ) ( r / 2 ) ) /\ z e. ( y ( ball ` D ) ( ( r / 2 ) / 2 ) ) ) ) -> ( y ( ball ` D ) ( ( r / 2 ) / 2 ) ) C_ ( x ( ball ` D ) r ) )
75 74 ex 
 |-  ( ( ( ( F e. ( CauFil ` D ) /\ x e. ( J fClus F ) ) /\ r e. RR+ ) /\ ( y e. X /\ ( y ( ball ` D ) ( ( r / 2 ) / 2 ) ) e. F ) ) -> ( ( z e. ( x ( ball ` D ) ( r / 2 ) ) /\ z e. ( y ( ball ` D ) ( ( r / 2 ) / 2 ) ) ) -> ( y ( ball ` D ) ( ( r / 2 ) / 2 ) ) C_ ( x ( ball ` D ) r ) ) )
76 52 75 biimtrid 
 |-  ( ( ( ( F e. ( CauFil ` D ) /\ x e. ( J fClus F ) ) /\ r e. RR+ ) /\ ( y e. X /\ ( y ( ball ` D ) ( ( r / 2 ) / 2 ) ) e. F ) ) -> ( z e. ( ( x ( ball ` D ) ( r / 2 ) ) i^i ( y ( ball ` D ) ( ( r / 2 ) / 2 ) ) ) -> ( y ( ball ` D ) ( ( r / 2 ) / 2 ) ) C_ ( x ( ball ` D ) r ) ) )
77 76 exlimdv 
 |-  ( ( ( ( F e. ( CauFil ` D ) /\ x e. ( J fClus F ) ) /\ r e. RR+ ) /\ ( y e. X /\ ( y ( ball ` D ) ( ( r / 2 ) / 2 ) ) e. F ) ) -> ( E. z z e. ( ( x ( ball ` D ) ( r / 2 ) ) i^i ( y ( ball ` D ) ( ( r / 2 ) / 2 ) ) ) -> ( y ( ball ` D ) ( ( r / 2 ) / 2 ) ) C_ ( x ( ball ` D ) r ) ) )
78 51 77 mpd 
 |-  ( ( ( ( F e. ( CauFil ` D ) /\ x e. ( J fClus F ) ) /\ r e. RR+ ) /\ ( y e. X /\ ( y ( ball ` D ) ( ( r / 2 ) / 2 ) ) e. F ) ) -> ( y ( ball ` D ) ( ( r / 2 ) / 2 ) ) C_ ( x ( ball ` D ) r ) )
79 filss 
 |-  ( ( F e. ( Fil ` X ) /\ ( ( y ( ball ` D ) ( ( r / 2 ) / 2 ) ) e. F /\ ( x ( ball ` D ) r ) C_ X /\ ( y ( ball ` D ) ( ( r / 2 ) / 2 ) ) C_ ( x ( ball ` D ) r ) ) ) -> ( x ( ball ` D ) r ) e. F )
80 33 34 40 78 79 syl13anc 
 |-  ( ( ( ( F e. ( CauFil ` D ) /\ x e. ( J fClus F ) ) /\ r e. RR+ ) /\ ( y e. X /\ ( y ( ball ` D ) ( ( r / 2 ) / 2 ) ) e. F ) ) -> ( x ( ball ` D ) r ) e. F )
81 32 80 rexlimddv 
 |-  ( ( ( F e. ( CauFil ` D ) /\ x e. ( J fClus F ) ) /\ r e. RR+ ) -> ( x ( ball ` D ) r ) e. F )
82 81 ad2ant2r 
 |-  ( ( ( ( F e. ( CauFil ` D ) /\ x e. ( J fClus F ) ) /\ ( y e. J /\ x e. y ) ) /\ ( r e. RR+ /\ ( x ( ball ` D ) r ) C_ y ) ) -> ( x ( ball ` D ) r ) e. F )
83 toponss 
 |-  ( ( J e. ( TopOn ` X ) /\ y e. J ) -> y C_ X )
84 83 adantrr 
 |-  ( ( J e. ( TopOn ` X ) /\ ( y e. J /\ x e. y ) ) -> y C_ X )
85 14 84 sylan 
 |-  ( ( ( F e. ( CauFil ` D ) /\ x e. ( J fClus F ) ) /\ ( y e. J /\ x e. y ) ) -> y C_ X )
86 85 adantr 
 |-  ( ( ( ( F e. ( CauFil ` D ) /\ x e. ( J fClus F ) ) /\ ( y e. J /\ x e. y ) ) /\ ( r e. RR+ /\ ( x ( ball ` D ) r ) C_ y ) ) -> y C_ X )
87 simprr 
 |-  ( ( ( ( F e. ( CauFil ` D ) /\ x e. ( J fClus F ) ) /\ ( y e. J /\ x e. y ) ) /\ ( r e. RR+ /\ ( x ( ball ` D ) r ) C_ y ) ) -> ( x ( ball ` D ) r ) C_ y )
88 filss 
 |-  ( ( F e. ( Fil ` X ) /\ ( ( x ( ball ` D ) r ) e. F /\ y C_ X /\ ( x ( ball ` D ) r ) C_ y ) ) -> y e. F )
89 24 82 86 87 88 syl13anc 
 |-  ( ( ( ( F e. ( CauFil ` D ) /\ x e. ( J fClus F ) ) /\ ( y e. J /\ x e. y ) ) /\ ( r e. RR+ /\ ( x ( ball ` D ) r ) C_ y ) ) -> y e. F )
90 20 89 rexlimddv 
 |-  ( ( ( F e. ( CauFil ` D ) /\ x e. ( J fClus F ) ) /\ ( y e. J /\ x e. y ) ) -> y e. F )
91 90 expr 
 |-  ( ( ( F e. ( CauFil ` D ) /\ x e. ( J fClus F ) ) /\ y e. J ) -> ( x e. y -> y e. F ) )
92 91 ralrimiva 
 |-  ( ( F e. ( CauFil ` D ) /\ x e. ( J fClus F ) ) -> A. y e. J ( x e. y -> y e. F ) )
93 flimopn 
 |-  ( ( J e. ( TopOn ` X ) /\ F e. ( Fil ` X ) ) -> ( x e. ( J fLim F ) <-> ( x e. X /\ A. y e. J ( x e. y -> y e. F ) ) ) )
94 14 23 93 syl2anc 
 |-  ( ( F e. ( CauFil ` D ) /\ x e. ( J fClus F ) ) -> ( x e. ( J fLim F ) <-> ( x e. X /\ A. y e. J ( x e. y -> y e. F ) ) ) )
95 17 92 94 mpbir2and 
 |-  ( ( F e. ( CauFil ` D ) /\ x e. ( J fClus F ) ) -> x e. ( J fLim F ) )
96 95 ex 
 |-  ( F e. ( CauFil ` D ) -> ( x e. ( J fClus F ) -> x e. ( J fLim F ) ) )
97 96 ssrdv 
 |-  ( F e. ( CauFil ` D ) -> ( J fClus F ) C_ ( J fLim F ) )
98 flimfcls 
 |-  ( J fLim F ) C_ ( J fClus F )
99 98 a1i 
 |-  ( F e. ( CauFil ` D ) -> ( J fLim F ) C_ ( J fClus F ) )
100 97 99 eqssd 
 |-  ( F e. ( CauFil ` D ) -> ( J fClus F ) = ( J fLim F ) )