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 ‘ 𝑋 ) )

Metamath Proof Explorer

Theorem relcmpcmet

Proof