Metamath Proof Explorer

Theorem relcmpcmet

Description: If D is a metric space such that all the balls of some fixed size are relatively compact, then D is complete. (Contributed by Mario Carneiro, 15-Oct-2015)

Ref Expression
Hypotheses relcmpcmet.1 
|- J = ( MetOpen ` D )
relcmpcmet.2 
|- ( ph -> D e. ( Met ` X ) )
relcmpcmet.3 
|- ( ph -> R e. RR+ )
relcmpcmet.4 
|- ( ( ph /\ x e. X ) -> ( J |`t ( ( cls ` J ) ` ( x ( ball ` D ) R ) ) ) e. Comp )
Assertion relcmpcmet 
|- ( ph -> D e. ( CMet ` X ) )

Proof

Step Hyp Ref Expression
1 relcmpcmet.1 
 |-  J = ( MetOpen ` D )
2 relcmpcmet.2 
 |-  ( ph -> D e. ( Met ` X ) )
3 relcmpcmet.3 
 |-  ( ph -> R e. RR+ )
4 relcmpcmet.4 
 |-  ( ( ph /\ x e. X ) -> ( J |`t ( ( cls ` J ) ` ( x ( ball ` D ) R ) ) ) e. Comp )
5 metxmet 
 |-  ( D e. ( Met ` X ) -> D e. ( *Met ` X ) )
6 2 5 syl 
 |-  ( ph -> D e. ( *Met ` X ) )
7 6 adantr 
 |-  ( ( ph /\ f e. ( CauFil ` D ) ) -> D e. ( *Met ` X ) )
8 simpr 
 |-  ( ( ph /\ f e. ( CauFil ` D ) ) -> f e. ( CauFil ` D ) )
9 3 adantr 
 |-  ( ( ph /\ f e. ( CauFil ` D ) ) -> R e. RR+ )
10 cfil3i 
 |-  ( ( D e. ( *Met ` X ) /\ f e. ( CauFil ` D ) /\ R e. RR+ ) -> E. x e. X ( x ( ball ` D ) R ) e. f )
11 7 8 9 10 syl3anc 
 |-  ( ( ph /\ f e. ( CauFil ` D ) ) -> E. x e. X ( x ( ball ` D ) R ) e. f )
12 6 ad2antrr 
 |-  ( ( ( ph /\ f e. ( CauFil ` D ) ) /\ ( x e. X /\ ( x ( ball ` D ) R ) e. f ) ) -> D e. ( *Met ` X ) )
13 1 mopntopon 
 |-  ( D e. ( *Met ` X ) -> J e. ( TopOn ` X ) )
14 12 13 syl 
 |-  ( ( ( ph /\ f e. ( CauFil ` D ) ) /\ ( x e. X /\ ( x ( ball ` D ) R ) e. f ) ) -> J e. ( TopOn ` X ) )
15 cfilfil 
 |-  ( ( D e. ( *Met ` X ) /\ f e. ( CauFil ` D ) ) -> f e. ( Fil ` X ) )
16 6 15 sylan 
 |-  ( ( ph /\ f e. ( CauFil ` D ) ) -> f e. ( Fil ` X ) )
17 16 adantr 
 |-  ( ( ( ph /\ f e. ( CauFil ` D ) ) /\ ( x e. X /\ ( x ( ball ` D ) R ) e. f ) ) -> f e. ( Fil ` X ) )
18 simprr 
 |-  ( ( ( ph /\ f e. ( CauFil ` D ) ) /\ ( x e. X /\ ( x ( ball ` D ) R ) e. f ) ) -> ( x ( ball ` D ) R ) e. f )
19 topontop 
 |-  ( J e. ( TopOn ` X ) -> J e. Top )
20 14 19 syl 
 |-  ( ( ( ph /\ f e. ( CauFil ` D ) ) /\ ( x e. X /\ ( x ( ball ` D ) R ) e. f ) ) -> J e. Top )
21 simprl 
 |-  ( ( ( ph /\ f e. ( CauFil ` D ) ) /\ ( x e. X /\ ( x ( ball ` D ) R ) e. f ) ) -> x e. X )
22 3 rpxrd 
 |-  ( ph -> R e. RR* )
23 22 ad2antrr 
 |-  ( ( ( ph /\ f e. ( CauFil ` D ) ) /\ ( x e. X /\ ( x ( ball ` D ) R ) e. f ) ) -> R e. RR* )
24 blssm 
 |-  ( ( D e. ( *Met ` X ) /\ x e. X /\ R e. RR* ) -> ( x ( ball ` D ) R ) C_ X )
25 12 21 23 24 syl3anc 
 |-  ( ( ( ph /\ f e. ( CauFil ` D ) ) /\ ( x e. X /\ ( x ( ball ` D ) R ) e. f ) ) -> ( x ( ball ` D ) R ) C_ X )
26 toponuni 
 |-  ( J e. ( TopOn ` X ) -> X = U. J )
27 14 26 syl 
 |-  ( ( ( ph /\ f e. ( CauFil ` D ) ) /\ ( x e. X /\ ( x ( ball ` D ) R ) e. f ) ) -> X = U. J )
28 25 27 sseqtrd 
 |-  ( ( ( ph /\ f e. ( CauFil ` D ) ) /\ ( x e. X /\ ( x ( ball ` D ) R ) e. f ) ) -> ( x ( ball ` D ) R ) C_ U. J )
29 eqid 
 |-  U. J = U. J
30 29 clsss3 
 |-  ( ( J e. Top /\ ( x ( ball ` D ) R ) C_ U. J ) -> ( ( cls ` J ) ` ( x ( ball ` D ) R ) ) C_ U. J )
31 20 28 30 syl2anc 
 |-  ( ( ( ph /\ f e. ( CauFil ` D ) ) /\ ( x e. X /\ ( x ( ball ` D ) R ) e. f ) ) -> ( ( cls ` J ) ` ( x ( ball ` D ) R ) ) C_ U. J )
32 31 27 sseqtrrd 
 |-  ( ( ( ph /\ f e. ( CauFil ` D ) ) /\ ( x e. X /\ ( x ( ball ` D ) R ) e. f ) ) -> ( ( cls ` J ) ` ( x ( ball ` D ) R ) ) C_ X )
33 29 sscls 
 |-  ( ( J e. Top /\ ( x ( ball ` D ) R ) C_ U. J ) -> ( x ( ball ` D ) R ) C_ ( ( cls ` J ) ` ( x ( ball ` D ) R ) ) )
34 20 28 33 syl2anc 
 |-  ( ( ( ph /\ f e. ( CauFil ` D ) ) /\ ( x e. X /\ ( x ( ball ` D ) R ) e. f ) ) -> ( x ( ball ` D ) R ) C_ ( ( cls ` J ) ` ( x ( ball ` D ) R ) ) )
35 filss 
 |-  ( ( f e. ( Fil ` X ) /\ ( ( x ( ball ` D ) R ) e. f /\ ( ( cls ` J ) ` ( x ( ball ` D ) R ) ) C_ X /\ ( x ( ball ` D ) R ) C_ ( ( cls ` J ) ` ( x ( ball ` D ) R ) ) ) ) -> ( ( cls ` J ) ` ( x ( ball ` D ) R ) ) e. f )
36 17 18 32 34 35 syl13anc 
 |-  ( ( ( ph /\ f e. ( CauFil ` D ) ) /\ ( x e. X /\ ( x ( ball ` D ) R ) e. f ) ) -> ( ( cls ` J ) ` ( x ( ball ` D ) R ) ) e. f )
37 fclsrest 
 |-  ( ( J e. ( TopOn ` X ) /\ f e. ( Fil ` X ) /\ ( ( cls ` J ) ` ( x ( ball ` D ) R ) ) e. f ) -> ( ( J |`t ( ( cls ` J ) ` ( x ( ball ` D ) R ) ) ) fClus ( f |`t ( ( cls ` J ) ` ( x ( ball ` D ) R ) ) ) ) = ( ( J fClus f ) i^i ( ( cls ` J ) ` ( x ( ball ` D ) R ) ) ) )
38 14 17 36 37 syl3anc 
 |-  ( ( ( ph /\ f e. ( CauFil ` D ) ) /\ ( x e. X /\ ( x ( ball ` D ) R ) e. f ) ) -> ( ( J |`t ( ( cls ` J ) ` ( x ( ball ` D ) R ) ) ) fClus ( f |`t ( ( cls ` J ) ` ( x ( ball ` D ) R ) ) ) ) = ( ( J fClus f ) i^i ( ( cls ` J ) ` ( x ( ball ` D ) R ) ) ) )
39 inss1 
 |-  ( ( J fClus f ) i^i ( ( cls ` J ) ` ( x ( ball ` D ) R ) ) ) C_ ( J fClus f )
40 eqid 
 |-  dom dom D = dom dom D
41 1 40 cfilfcls 
 |-  ( f e. ( CauFil ` D ) -> ( J fClus f ) = ( J fLim f ) )
42 41 ad2antlr 
 |-  ( ( ( ph /\ f e. ( CauFil ` D ) ) /\ ( x e. X /\ ( x ( ball ` D ) R ) e. f ) ) -> ( J fClus f ) = ( J fLim f ) )
43 39 42 sseqtrid 
 |-  ( ( ( ph /\ f e. ( CauFil ` D ) ) /\ ( x e. X /\ ( x ( ball ` D ) R ) e. f ) ) -> ( ( J fClus f ) i^i ( ( cls ` J ) ` ( x ( ball ` D ) R ) ) ) C_ ( J fLim f ) )
44 38 43 eqsstrd 
 |-  ( ( ( ph /\ f e. ( CauFil ` D ) ) /\ ( x e. X /\ ( x ( ball ` D ) R ) e. f ) ) -> ( ( J |`t ( ( cls ` J ) ` ( x ( ball ` D ) R ) ) ) fClus ( f |`t ( ( cls ` J ) ` ( x ( ball ` D ) R ) ) ) ) C_ ( J fLim f ) )
45 4 ad2ant2r 
 |-  ( ( ( ph /\ f e. ( CauFil ` D ) ) /\ ( x e. X /\ ( x ( ball ` D ) R ) e. f ) ) -> ( J |`t ( ( cls ` J ) ` ( x ( ball ` D ) R ) ) ) e. Comp )
46 filfbas 
 |-  ( f e. ( Fil ` X ) -> f e. ( fBas ` X ) )
47 17 46 syl 
 |-  ( ( ( ph /\ f e. ( CauFil ` D ) ) /\ ( x e. X /\ ( x ( ball ` D ) R ) e. f ) ) -> f e. ( fBas ` X ) )
48 fbncp 
 |-  ( ( f e. ( fBas ` X ) /\ ( ( cls ` J ) ` ( x ( ball ` D ) R ) ) e. f ) -> -. ( X \ ( ( cls ` J ) ` ( x ( ball ` D ) R ) ) ) e. f )
49 47 36 48 syl2anc 
 |-  ( ( ( ph /\ f e. ( CauFil ` D ) ) /\ ( x e. X /\ ( x ( ball ` D ) R ) e. f ) ) -> -. ( X \ ( ( cls ` J ) ` ( x ( ball ` D ) R ) ) ) e. f )
50 trfil3 
 |-  ( ( f e. ( Fil ` X ) /\ ( ( cls ` J ) ` ( x ( ball ` D ) R ) ) C_ X ) -> ( ( f |`t ( ( cls ` J ) ` ( x ( ball ` D ) R ) ) ) e. ( Fil ` ( ( cls ` J ) ` ( x ( ball ` D ) R ) ) ) <-> -. ( X \ ( ( cls ` J ) ` ( x ( ball ` D ) R ) ) ) e. f ) )
51 17 32 50 syl2anc 
 |-  ( ( ( ph /\ f e. ( CauFil ` D ) ) /\ ( x e. X /\ ( x ( ball ` D ) R ) e. f ) ) -> ( ( f |`t ( ( cls ` J ) ` ( x ( ball ` D ) R ) ) ) e. ( Fil ` ( ( cls ` J ) ` ( x ( ball ` D ) R ) ) ) <-> -. ( X \ ( ( cls ` J ) ` ( x ( ball ` D ) R ) ) ) e. f ) )
52 49 51 mpbird 
 |-  ( ( ( ph /\ f e. ( CauFil ` D ) ) /\ ( x e. X /\ ( x ( ball ` D ) R ) e. f ) ) -> ( f |`t ( ( cls ` J ) ` ( x ( ball ` D ) R ) ) ) e. ( Fil ` ( ( cls ` J ) ` ( x ( ball ` D ) R ) ) ) )
53 resttopon 
 |-  ( ( J e. ( TopOn ` X ) /\ ( ( cls ` J ) ` ( x ( ball ` D ) R ) ) C_ X ) -> ( J |`t ( ( cls ` J ) ` ( x ( ball ` D ) R ) ) ) e. ( TopOn ` ( ( cls ` J ) ` ( x ( ball ` D ) R ) ) ) )
54 14 32 53 syl2anc 
 |-  ( ( ( ph /\ f e. ( CauFil ` D ) ) /\ ( x e. X /\ ( x ( ball ` D ) R ) e. f ) ) -> ( J |`t ( ( cls ` J ) ` ( x ( ball ` D ) R ) ) ) e. ( TopOn ` ( ( cls ` J ) ` ( x ( ball ` D ) R ) ) ) )
55 toponuni 
 |-  ( ( J |`t ( ( cls ` J ) ` ( x ( ball ` D ) R ) ) ) e. ( TopOn ` ( ( cls ` J ) ` ( x ( ball ` D ) R ) ) ) -> ( ( cls ` J ) ` ( x ( ball ` D ) R ) ) = U. ( J |`t ( ( cls ` J ) ` ( x ( ball ` D ) R ) ) ) )
56 54 55 syl 
 |-  ( ( ( ph /\ f e. ( CauFil ` D ) ) /\ ( x e. X /\ ( x ( ball ` D ) R ) e. f ) ) -> ( ( cls ` J ) ` ( x ( ball ` D ) R ) ) = U. ( J |`t ( ( cls ` J ) ` ( x ( ball ` D ) R ) ) ) )
57 56 fveq2d 
 |-  ( ( ( ph /\ f e. ( CauFil ` D ) ) /\ ( x e. X /\ ( x ( ball ` D ) R ) e. f ) ) -> ( Fil ` ( ( cls ` J ) ` ( x ( ball ` D ) R ) ) ) = ( Fil ` U. ( J |`t ( ( cls ` J ) ` ( x ( ball ` D ) R ) ) ) ) )
58 52 57 eleqtrd 
 |-  ( ( ( ph /\ f e. ( CauFil ` D ) ) /\ ( x e. X /\ ( x ( ball ` D ) R ) e. f ) ) -> ( f |`t ( ( cls ` J ) ` ( x ( ball ` D ) R ) ) ) e. ( Fil ` U. ( J |`t ( ( cls ` J ) ` ( x ( ball ` D ) R ) ) ) ) )
59 eqid 
 |-  U. ( J |`t ( ( cls ` J ) ` ( x ( ball ` D ) R ) ) ) = U. ( J |`t ( ( cls ` J ) ` ( x ( ball ` D ) R ) ) )
60 59 fclscmpi 
 |-  ( ( ( J |`t ( ( cls ` J ) ` ( x ( ball ` D ) R ) ) ) e. Comp /\ ( f |`t ( ( cls ` J ) ` ( x ( ball ` D ) R ) ) ) e. ( Fil ` U. ( J |`t ( ( cls ` J ) ` ( x ( ball ` D ) R ) ) ) ) ) -> ( ( J |`t ( ( cls ` J ) ` ( x ( ball ` D ) R ) ) ) fClus ( f |`t ( ( cls ` J ) ` ( x ( ball ` D ) R ) ) ) ) =/= (/) )
61 45 58 60 syl2anc 
 |-  ( ( ( ph /\ f e. ( CauFil ` D ) ) /\ ( x e. X /\ ( x ( ball ` D ) R ) e. f ) ) -> ( ( J |`t ( ( cls ` J ) ` ( x ( ball ` D ) R ) ) ) fClus ( f |`t ( ( cls ` J ) ` ( x ( ball ` D ) R ) ) ) ) =/= (/) )
62 ssn0 
 |-  ( ( ( ( J |`t ( ( cls ` J ) ` ( x ( ball ` D ) R ) ) ) fClus ( f |`t ( ( cls ` J ) ` ( x ( ball ` D ) R ) ) ) ) C_ ( J fLim f ) /\ ( ( J |`t ( ( cls ` J ) ` ( x ( ball ` D ) R ) ) ) fClus ( f |`t ( ( cls ` J ) ` ( x ( ball ` D ) R ) ) ) ) =/= (/) ) -> ( J fLim f ) =/= (/) )
63 44 61 62 syl2anc 
 |-  ( ( ( ph /\ f e. ( CauFil ` D ) ) /\ ( x e. X /\ ( x ( ball ` D ) R ) e. f ) ) -> ( J fLim f ) =/= (/) )
64 11 63 rexlimddv 
 |-  ( ( ph /\ f e. ( CauFil ` D ) ) -> ( J fLim f ) =/= (/) )
65 64 ralrimiva 
 |-  ( ph -> A. f e. ( CauFil ` D ) ( J fLim f ) =/= (/) )
66 1 iscmet 
 |-  ( D e. ( CMet ` X ) <-> ( D e. ( Met ` X ) /\ A. f e. ( CauFil ` D ) ( J fLim f ) =/= (/) ) )
67 2 65 66 sylanbrc 
 |-  ( ph -> D e. ( CMet ` X ) )