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 ⊢ 𝐽 = ( MetOpen ‘ 𝐷 )
relcmpcmet.2 ⊢ ( 𝜑 → 𝐷 ∈ ( Met ‘ 𝑋 ) )
relcmpcmet.3 ⊢ ( 𝜑 → 𝑅 ∈ ℝ+ )
relcmpcmet.4 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( 𝐽 ↾t ( ( cls ‘ 𝐽 ) ‘ ( 𝑥 ( ball ‘ 𝐷 ) 𝑅 ) ) ) ∈ Comp )
Assertion relcmpcmet ( 𝜑 → 𝐷 ∈ ( CMet ‘ 𝑋 ) )

Proof

Step Hyp Ref Expression
1 relcmpcmet.1 ⊢ 𝐽 = ( MetOpen ‘ 𝐷 )
2 relcmpcmet.2 ⊢ ( 𝜑 → 𝐷 ∈ ( Met ‘ 𝑋 ) )
3 relcmpcmet.3 ⊢ ( 𝜑 → 𝑅 ∈ ℝ+ )
4 relcmpcmet.4 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( 𝐽 ↾t ( ( cls ‘ 𝐽 ) ‘ ( 𝑥 ( ball ‘ 𝐷 ) 𝑅 ) ) ) ∈ Comp )
5 metxmet ⊢ ( 𝐷 ∈ ( Met ‘ 𝑋 ) → 𝐷 ∈ ( ∞Met ‘ 𝑋 ) )
6 2 5 syl ⊢ ( 𝜑 → 𝐷 ∈ ( ∞Met ‘ 𝑋 ) )
7 6 adantr ⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( CauFil ‘ 𝐷 ) ) → 𝐷 ∈ ( ∞Met ‘ 𝑋 ) )
8 simpr ⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( CauFil ‘ 𝐷 ) ) → 𝑓 ∈ ( CauFil ‘ 𝐷 ) )
9 3 adantr ⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( CauFil ‘ 𝐷 ) ) → 𝑅 ∈ ℝ+ )
10 cfil3i ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑓 ∈ ( CauFil ‘ 𝐷 ) ∧ 𝑅 ∈ ℝ+ ) → ∃ 𝑥 ∈ 𝑋 ( 𝑥 ( ball ‘ 𝐷 ) 𝑅 ) ∈ 𝑓 )
11 7 8 9 10 syl3anc ⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( CauFil ‘ 𝐷 ) ) → ∃ 𝑥 ∈ 𝑋 ( 𝑥 ( ball ‘ 𝐷 ) 𝑅 ) ∈ 𝑓 )
12 6 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ( CauFil ‘ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝑋 ∧ ( 𝑥 ( ball ‘ 𝐷 ) 𝑅 ) ∈ 𝑓 ) ) → 𝐷 ∈ ( ∞Met ‘ 𝑋 ) )
13 1 mopntopon ⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
14 12 13 syl ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ( CauFil ‘ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝑋 ∧ ( 𝑥 ( ball ‘ 𝐷 ) 𝑅 ) ∈ 𝑓 ) ) → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
15 cfilfil ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑓 ∈ ( CauFil ‘ 𝐷 ) ) → 𝑓 ∈ ( Fil ‘ 𝑋 ) )
16 6 15 sylan ⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( CauFil ‘ 𝐷 ) ) → 𝑓 ∈ ( Fil ‘ 𝑋 ) )
17 16 adantr ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ( CauFil ‘ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝑋 ∧ ( 𝑥 ( ball ‘ 𝐷 ) 𝑅 ) ∈ 𝑓 ) ) → 𝑓 ∈ ( Fil ‘ 𝑋 ) )
18 simprr ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ( CauFil ‘ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝑋 ∧ ( 𝑥 ( ball ‘ 𝐷 ) 𝑅 ) ∈ 𝑓 ) ) → ( 𝑥 ( ball ‘ 𝐷 ) 𝑅 ) ∈ 𝑓 )
19 topontop ⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → 𝐽 ∈ Top )
20 14 19 syl ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ( CauFil ‘ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝑋 ∧ ( 𝑥 ( ball ‘ 𝐷 ) 𝑅 ) ∈ 𝑓 ) ) → 𝐽 ∈ Top )
21 simprl ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ( CauFil ‘ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝑋 ∧ ( 𝑥 ( ball ‘ 𝐷 ) 𝑅 ) ∈ 𝑓 ) ) → 𝑥 ∈ 𝑋 )
22 3 rpxrd ⊢ ( 𝜑 → 𝑅 ∈ ℝ* )
23 22 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ( CauFil ‘ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝑋 ∧ ( 𝑥 ( ball ‘ 𝐷 ) 𝑅 ) ∈ 𝑓 ) ) → 𝑅 ∈ ℝ* )
24 blssm ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑥 ∈ 𝑋 ∧ 𝑅 ∈ ℝ* ) → ( 𝑥 ( ball ‘ 𝐷 ) 𝑅 ) ⊆ 𝑋 )
25 12 21 23 24 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ( CauFil ‘ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝑋 ∧ ( 𝑥 ( ball ‘ 𝐷 ) 𝑅 ) ∈ 𝑓 ) ) → ( 𝑥 ( ball ‘ 𝐷 ) 𝑅 ) ⊆ 𝑋 )
26 toponuni ⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → 𝑋 = ∪ 𝐽 )
27 14 26 syl ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ( CauFil ‘ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝑋 ∧ ( 𝑥 ( ball ‘ 𝐷 ) 𝑅 ) ∈ 𝑓 ) ) → 𝑋 = ∪ 𝐽 )
28 25 27 sseqtrd ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ( CauFil ‘ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝑋 ∧ ( 𝑥 ( ball ‘ 𝐷 ) 𝑅 ) ∈ 𝑓 ) ) → ( 𝑥 ( ball ‘ 𝐷 ) 𝑅 ) ⊆ ∪ 𝐽 )
29 eqid ⊢ ∪ 𝐽 = ∪ 𝐽
30 29 clsss3 ⊢ ( ( 𝐽 ∈ Top ∧ ( 𝑥 ( ball ‘ 𝐷 ) 𝑅 ) ⊆ ∪ 𝐽 ) → ( ( cls ‘ 𝐽 ) ‘ ( 𝑥 ( ball ‘ 𝐷 ) 𝑅 ) ) ⊆ ∪ 𝐽 )
31 20 28 30 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ( CauFil ‘ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝑋 ∧ ( 𝑥 ( ball ‘ 𝐷 ) 𝑅 ) ∈ 𝑓 ) ) → ( ( cls ‘ 𝐽 ) ‘ ( 𝑥 ( ball ‘ 𝐷 ) 𝑅 ) ) ⊆ ∪ 𝐽 )
32 31 27 sseqtrrd ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ( CauFil ‘ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝑋 ∧ ( 𝑥 ( ball ‘ 𝐷 ) 𝑅 ) ∈ 𝑓 ) ) → ( ( cls ‘ 𝐽 ) ‘ ( 𝑥 ( ball ‘ 𝐷 ) 𝑅 ) ) ⊆ 𝑋 )
33 29 sscls ⊢ ( ( 𝐽 ∈ Top ∧ ( 𝑥 ( ball ‘ 𝐷 ) 𝑅 ) ⊆ ∪ 𝐽 ) → ( 𝑥 ( ball ‘ 𝐷 ) 𝑅 ) ⊆ ( ( cls ‘ 𝐽 ) ‘ ( 𝑥 ( ball ‘ 𝐷 ) 𝑅 ) ) )
34 20 28 33 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ( CauFil ‘ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝑋 ∧ ( 𝑥 ( ball ‘ 𝐷 ) 𝑅 ) ∈ 𝑓 ) ) → ( 𝑥 ( ball ‘ 𝐷 ) 𝑅 ) ⊆ ( ( cls ‘ 𝐽 ) ‘ ( 𝑥 ( ball ‘ 𝐷 ) 𝑅 ) ) )
35 filss ⊢ ( ( 𝑓 ∈ ( Fil ‘ 𝑋 ) ∧ ( ( 𝑥 ( ball ‘ 𝐷 ) 𝑅 ) ∈ 𝑓 ∧ ( ( cls ‘ 𝐽 ) ‘ ( 𝑥 ( ball ‘ 𝐷 ) 𝑅 ) ) ⊆ 𝑋 ∧ ( 𝑥 ( ball ‘ 𝐷 ) 𝑅 ) ⊆ ( ( cls ‘ 𝐽 ) ‘ ( 𝑥 ( ball ‘ 𝐷 ) 𝑅 ) ) ) ) → ( ( cls ‘ 𝐽 ) ‘ ( 𝑥 ( ball ‘ 𝐷 ) 𝑅 ) ) ∈ 𝑓 )
36 17 18 32 34 35 syl13anc ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ( CauFil ‘ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝑋 ∧ ( 𝑥 ( ball ‘ 𝐷 ) 𝑅 ) ∈ 𝑓 ) ) → ( ( cls ‘ 𝐽 ) ‘ ( 𝑥 ( ball ‘ 𝐷 ) 𝑅 ) ) ∈ 𝑓 )
37 fclsrest ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑓 ∈ ( Fil ‘ 𝑋 ) ∧ ( ( cls ‘ 𝐽 ) ‘ ( 𝑥 ( ball ‘ 𝐷 ) 𝑅 ) ) ∈ 𝑓 ) → ( ( 𝐽 ↾t ( ( cls ‘ 𝐽 ) ‘ ( 𝑥 ( ball ‘ 𝐷 ) 𝑅 ) ) ) fClus ( 𝑓 ↾t ( ( cls ‘ 𝐽 ) ‘ ( 𝑥 ( ball ‘ 𝐷 ) 𝑅 ) ) ) ) = ( ( 𝐽 fClus 𝑓 ) ∩ ( ( cls ‘ 𝐽 ) ‘ ( 𝑥 ( ball ‘ 𝐷 ) 𝑅 ) ) ) )
38 14 17 36 37 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ( CauFil ‘ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝑋 ∧ ( 𝑥 ( ball ‘ 𝐷 ) 𝑅 ) ∈ 𝑓 ) ) → ( ( 𝐽 ↾t ( ( cls ‘ 𝐽 ) ‘ ( 𝑥 ( ball ‘ 𝐷 ) 𝑅 ) ) ) fClus ( 𝑓 ↾t ( ( cls ‘ 𝐽 ) ‘ ( 𝑥 ( ball ‘ 𝐷 ) 𝑅 ) ) ) ) = ( ( 𝐽 fClus 𝑓 ) ∩ ( ( cls ‘ 𝐽 ) ‘ ( 𝑥 ( ball ‘ 𝐷 ) 𝑅 ) ) ) )
39 inss1 ⊢ ( ( 𝐽 fClus 𝑓 ) ∩ ( ( cls ‘ 𝐽 ) ‘ ( 𝑥 ( ball ‘ 𝐷 ) 𝑅 ) ) ) ⊆ ( 𝐽 fClus 𝑓 )
40 eqid ⊢ dom dom 𝐷 = dom dom 𝐷
41 1 40 cfilfcls ⊢ ( 𝑓 ∈ ( CauFil ‘ 𝐷 ) → ( 𝐽 fClus 𝑓 ) = ( 𝐽 fLim 𝑓 ) )
42 41 ad2antlr ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ( CauFil ‘ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝑋 ∧ ( 𝑥 ( ball ‘ 𝐷 ) 𝑅 ) ∈ 𝑓 ) ) → ( 𝐽 fClus 𝑓 ) = ( 𝐽 fLim 𝑓 ) )
43 39 42 sseqtrid ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ( CauFil ‘ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝑋 ∧ ( 𝑥 ( ball ‘ 𝐷 ) 𝑅 ) ∈ 𝑓 ) ) → ( ( 𝐽 fClus 𝑓 ) ∩ ( ( cls ‘ 𝐽 ) ‘ ( 𝑥 ( ball ‘ 𝐷 ) 𝑅 ) ) ) ⊆ ( 𝐽 fLim 𝑓 ) )
44 38 43 eqsstrd ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ( CauFil ‘ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝑋 ∧ ( 𝑥 ( ball ‘ 𝐷 ) 𝑅 ) ∈ 𝑓 ) ) → ( ( 𝐽 ↾t ( ( cls ‘ 𝐽 ) ‘ ( 𝑥 ( ball ‘ 𝐷 ) 𝑅 ) ) ) fClus ( 𝑓 ↾t ( ( cls ‘ 𝐽 ) ‘ ( 𝑥 ( ball ‘ 𝐷 ) 𝑅 ) ) ) ) ⊆ ( 𝐽 fLim 𝑓 ) )
45 4 ad2ant2r ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ( CauFil ‘ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝑋 ∧ ( 𝑥 ( ball ‘ 𝐷 ) 𝑅 ) ∈ 𝑓 ) ) → ( 𝐽 ↾t ( ( cls ‘ 𝐽 ) ‘ ( 𝑥 ( ball ‘ 𝐷 ) 𝑅 ) ) ) ∈ Comp )
46 filfbas ⊢ ( 𝑓 ∈ ( Fil ‘ 𝑋 ) → 𝑓 ∈ ( fBas ‘ 𝑋 ) )
47 17 46 syl ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ( CauFil ‘ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝑋 ∧ ( 𝑥 ( ball ‘ 𝐷 ) 𝑅 ) ∈ 𝑓 ) ) → 𝑓 ∈ ( fBas ‘ 𝑋 ) )
48 fbncp ⊢ ( ( 𝑓 ∈ ( fBas ‘ 𝑋 ) ∧ ( ( cls ‘ 𝐽 ) ‘ ( 𝑥 ( ball ‘ 𝐷 ) 𝑅 ) ) ∈ 𝑓 ) → ¬ ( 𝑋 ∖ ( ( cls ‘ 𝐽 ) ‘ ( 𝑥 ( ball ‘ 𝐷 ) 𝑅 ) ) ) ∈ 𝑓 )
49 47 36 48 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ( CauFil ‘ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝑋 ∧ ( 𝑥 ( ball ‘ 𝐷 ) 𝑅 ) ∈ 𝑓 ) ) → ¬ ( 𝑋 ∖ ( ( cls ‘ 𝐽 ) ‘ ( 𝑥 ( ball ‘ 𝐷 ) 𝑅 ) ) ) ∈ 𝑓 )
50 trfil3 ⊢ ( ( 𝑓 ∈ ( Fil ‘ 𝑋 ) ∧ ( ( cls ‘ 𝐽 ) ‘ ( 𝑥 ( ball ‘ 𝐷 ) 𝑅 ) ) ⊆ 𝑋 ) → ( ( 𝑓 ↾t ( ( cls ‘ 𝐽 ) ‘ ( 𝑥 ( ball ‘ 𝐷 ) 𝑅 ) ) ) ∈ ( Fil ‘ ( ( cls ‘ 𝐽 ) ‘ ( 𝑥 ( ball ‘ 𝐷 ) 𝑅 ) ) ) ↔ ¬ ( 𝑋 ∖ ( ( cls ‘ 𝐽 ) ‘ ( 𝑥 ( ball ‘ 𝐷 ) 𝑅 ) ) ) ∈ 𝑓 ) )
51 17 32 50 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ( CauFil ‘ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝑋 ∧ ( 𝑥 ( ball ‘ 𝐷 ) 𝑅 ) ∈ 𝑓 ) ) → ( ( 𝑓 ↾t ( ( cls ‘ 𝐽 ) ‘ ( 𝑥 ( ball ‘ 𝐷 ) 𝑅 ) ) ) ∈ ( Fil ‘ ( ( cls ‘ 𝐽 ) ‘ ( 𝑥 ( ball ‘ 𝐷 ) 𝑅 ) ) ) ↔ ¬ ( 𝑋 ∖ ( ( cls ‘ 𝐽 ) ‘ ( 𝑥 ( ball ‘ 𝐷 ) 𝑅 ) ) ) ∈ 𝑓 ) )
52 49 51 mpbird ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ( CauFil ‘ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝑋 ∧ ( 𝑥 ( ball ‘ 𝐷 ) 𝑅 ) ∈ 𝑓 ) ) → ( 𝑓 ↾t ( ( cls ‘ 𝐽 ) ‘ ( 𝑥 ( ball ‘ 𝐷 ) 𝑅 ) ) ) ∈ ( Fil ‘ ( ( cls ‘ 𝐽 ) ‘ ( 𝑥 ( ball ‘ 𝐷 ) 𝑅 ) ) ) )
53 resttopon ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ ( ( cls ‘ 𝐽 ) ‘ ( 𝑥 ( ball ‘ 𝐷 ) 𝑅 ) ) ⊆ 𝑋 ) → ( 𝐽 ↾t ( ( cls ‘ 𝐽 ) ‘ ( 𝑥 ( ball ‘ 𝐷 ) 𝑅 ) ) ) ∈ ( TopOn ‘ ( ( cls ‘ 𝐽 ) ‘ ( 𝑥 ( ball ‘ 𝐷 ) 𝑅 ) ) ) )
54 14 32 53 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ( CauFil ‘ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝑋 ∧ ( 𝑥 ( ball ‘ 𝐷 ) 𝑅 ) ∈ 𝑓 ) ) → ( 𝐽 ↾t ( ( cls ‘ 𝐽 ) ‘ ( 𝑥 ( ball ‘ 𝐷 ) 𝑅 ) ) ) ∈ ( TopOn ‘ ( ( cls ‘ 𝐽 ) ‘ ( 𝑥 ( ball ‘ 𝐷 ) 𝑅 ) ) ) )
55 toponuni ⊢ ( ( 𝐽 ↾t ( ( cls ‘ 𝐽 ) ‘ ( 𝑥 ( ball ‘ 𝐷 ) 𝑅 ) ) ) ∈ ( TopOn ‘ ( ( cls ‘ 𝐽 ) ‘ ( 𝑥 ( ball ‘ 𝐷 ) 𝑅 ) ) ) → ( ( cls ‘ 𝐽 ) ‘ ( 𝑥 ( ball ‘ 𝐷 ) 𝑅 ) ) = ∪ ( 𝐽 ↾t ( ( cls ‘ 𝐽 ) ‘ ( 𝑥 ( ball ‘ 𝐷 ) 𝑅 ) ) ) )
56 54 55 syl ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ( CauFil ‘ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝑋 ∧ ( 𝑥 ( ball ‘ 𝐷 ) 𝑅 ) ∈ 𝑓 ) ) → ( ( cls ‘ 𝐽 ) ‘ ( 𝑥 ( ball ‘ 𝐷 ) 𝑅 ) ) = ∪ ( 𝐽 ↾t ( ( cls ‘ 𝐽 ) ‘ ( 𝑥 ( ball ‘ 𝐷 ) 𝑅 ) ) ) )
57 56 fveq2d ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ( CauFil ‘ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝑋 ∧ ( 𝑥 ( ball ‘ 𝐷 ) 𝑅 ) ∈ 𝑓 ) ) → ( Fil ‘ ( ( cls ‘ 𝐽 ) ‘ ( 𝑥 ( ball ‘ 𝐷 ) 𝑅 ) ) ) = ( Fil ‘ ∪ ( 𝐽 ↾t ( ( cls ‘ 𝐽 ) ‘ ( 𝑥 ( ball ‘ 𝐷 ) 𝑅 ) ) ) ) )
58 52 57 eleqtrd ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ( CauFil ‘ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝑋 ∧ ( 𝑥 ( ball ‘ 𝐷 ) 𝑅 ) ∈ 𝑓 ) ) → ( 𝑓 ↾t ( ( cls ‘ 𝐽 ) ‘ ( 𝑥 ( ball ‘ 𝐷 ) 𝑅 ) ) ) ∈ ( Fil ‘ ∪ ( 𝐽 ↾t ( ( cls ‘ 𝐽 ) ‘ ( 𝑥 ( ball ‘ 𝐷 ) 𝑅 ) ) ) ) )
59 eqid ⊢ ∪ ( 𝐽 ↾t ( ( cls ‘ 𝐽 ) ‘ ( 𝑥 ( ball ‘ 𝐷 ) 𝑅 ) ) ) = ∪ ( 𝐽 ↾t ( ( cls ‘ 𝐽 ) ‘ ( 𝑥 ( ball ‘ 𝐷 ) 𝑅 ) ) )
60 59 fclscmpi ⊢ ( ( ( 𝐽 ↾t ( ( cls ‘ 𝐽 ) ‘ ( 𝑥 ( ball ‘ 𝐷 ) 𝑅 ) ) ) ∈ Comp ∧ ( 𝑓 ↾t ( ( cls ‘ 𝐽 ) ‘ ( 𝑥 ( ball ‘ 𝐷 ) 𝑅 ) ) ) ∈ ( Fil ‘ ∪ ( 𝐽 ↾t ( ( cls ‘ 𝐽 ) ‘ ( 𝑥 ( ball ‘ 𝐷 ) 𝑅 ) ) ) ) ) → ( ( 𝐽 ↾t ( ( cls ‘ 𝐽 ) ‘ ( 𝑥 ( ball ‘ 𝐷 ) 𝑅 ) ) ) fClus ( 𝑓 ↾t ( ( cls ‘ 𝐽 ) ‘ ( 𝑥 ( ball ‘ 𝐷 ) 𝑅 ) ) ) ) ≠ ∅ )
61 45 58 60 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ( CauFil ‘ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝑋 ∧ ( 𝑥 ( ball ‘ 𝐷 ) 𝑅 ) ∈ 𝑓 ) ) → ( ( 𝐽 ↾t ( ( cls ‘ 𝐽 ) ‘ ( 𝑥 ( ball ‘ 𝐷 ) 𝑅 ) ) ) fClus ( 𝑓 ↾t ( ( cls ‘ 𝐽 ) ‘ ( 𝑥 ( ball ‘ 𝐷 ) 𝑅 ) ) ) ) ≠ ∅ )
62 ssn0 ⊢ ( ( ( ( 𝐽 ↾t ( ( cls ‘ 𝐽 ) ‘ ( 𝑥 ( ball ‘ 𝐷 ) 𝑅 ) ) ) fClus ( 𝑓 ↾t ( ( cls ‘ 𝐽 ) ‘ ( 𝑥 ( ball ‘ 𝐷 ) 𝑅 ) ) ) ) ⊆ ( 𝐽 fLim 𝑓 ) ∧ ( ( 𝐽 ↾t ( ( cls ‘ 𝐽 ) ‘ ( 𝑥 ( ball ‘ 𝐷 ) 𝑅 ) ) ) fClus ( 𝑓 ↾t ( ( cls ‘ 𝐽 ) ‘ ( 𝑥 ( ball ‘ 𝐷 ) 𝑅 ) ) ) ) ≠ ∅ ) → ( 𝐽 fLim 𝑓 ) ≠ ∅ )
63 44 61 62 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ( CauFil ‘ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝑋 ∧ ( 𝑥 ( ball ‘ 𝐷 ) 𝑅 ) ∈ 𝑓 ) ) → ( 𝐽 fLim 𝑓 ) ≠ ∅ )
64 11 63 rexlimddv ⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( CauFil ‘ 𝐷 ) ) → ( 𝐽 fLim 𝑓 ) ≠ ∅ )
65 64 ralrimiva ⊢ ( 𝜑 → ∀ 𝑓 ∈ ( CauFil ‘ 𝐷 ) ( 𝐽 fLim 𝑓 ) ≠ ∅ )
66 1 iscmet ⊢ ( 𝐷 ∈ ( CMet ‘ 𝑋 ) ↔ ( 𝐷 ∈ ( Met ‘ 𝑋 ) ∧ ∀ 𝑓 ∈ ( CauFil ‘ 𝐷 ) ( 𝐽 fLim 𝑓 ) ≠ ∅ ) )
67 2 65 66 sylanbrc ⊢ ( 𝜑 → 𝐷 ∈ ( CMet ‘ 𝑋 ) )