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	$⊢ φ \to D \in Met (X)$
	relcmpcmet.3	$⊢ φ \to R \in ℝ^{+}$
	relcmpcmet.4	$⊢ (φ \land x \in X) \to J ↾_{𝑡} cls (J) (x ball (D) R) \in Comp$
Assertion	relcmpcmet	$⊢ φ \to D \in CMet (X)$

Proof

Step	Hyp	Ref	Expression
1		relcmpcmet.1	$⊢ J = MetOpen (D)$
2		relcmpcmet.2	$⊢ φ \to D \in Met (X)$
3		relcmpcmet.3	$⊢ φ \to R \in ℝ^{+}$
4		relcmpcmet.4	$⊢ (φ \land x \in X) \to J ↾_{𝑡} cls (J) (x ball (D) R) \in Comp$
5		metxmet	$⊢ D \in Met (X) \to D \in ∞Met (X)$
6	2 5	syl	$⊢ φ \to D \in ∞Met (X)$
7	6	adantr	$⊢ (φ \land f \in CauFil (D)) \to D \in ∞Met (X)$
8		simpr	$⊢ (φ \land f \in CauFil (D)) \to f \in CauFil (D)$
9	3	adantr	$⊢ (φ \land f \in CauFil (D)) \to R \in ℝ^{+}$
10		cfil3i	$⊢ (D \in ∞Met (X) \land f \in CauFil (D) \land R \in ℝ^{+}) \to \exists x \in X x ball (D) R \in f$
11	7 8 9 10	syl3anc	$⊢ (φ \land f \in CauFil (D)) \to \exists x \in X x ball (D) R \in f$
12	6	ad2antrr	$⊢ ((φ \land f \in CauFil (D)) \land (x \in X \land x ball (D) R \in f)) \to D \in ∞Met (X)$
13	1	mopntopon	$⊢ D \in ∞Met (X) \to J \in TopOn (X)$
14	12 13	syl	$⊢ ((φ \land f \in CauFil (D)) \land (x \in X \land x ball (D) R \in f)) \to J \in TopOn (X)$
15		cfilfil	$⊢ (D \in ∞Met (X) \land f \in CauFil (D)) \to f \in Fil (X)$
16	6 15	sylan	$⊢ (φ \land f \in CauFil (D)) \to f \in Fil (X)$
17	16	adantr	$⊢ ((φ \land f \in CauFil (D)) \land (x \in X \land x ball (D) R \in f)) \to f \in Fil (X)$
18		simprr	$⊢ ((φ \land f \in CauFil (D)) \land (x \in X \land x ball (D) R \in f)) \to x ball (D) R \in f$
19		topontop	$⊢ J \in TopOn (X) \to J \in Top$
20	14 19	syl	$⊢ ((φ \land f \in CauFil (D)) \land (x \in X \land x ball (D) R \in f)) \to J \in Top$
21		simprl	$⊢ ((φ \land f \in CauFil (D)) \land (x \in X \land x ball (D) R \in f)) \to x \in X$
22	3	rpxrd	$⊢ φ \to R \in ℝ^{*}$
23	22	ad2antrr	$⊢ ((φ \land f \in CauFil (D)) \land (x \in X \land x ball (D) R \in f)) \to R \in ℝ^{*}$
24		blssm	$⊢ (D \in ∞Met (X) \land x \in X \land R \in ℝ^{*}) \to x ball (D) R \subseteq X$
25	12 21 23 24	syl3anc	$⊢ ((φ \land f \in CauFil (D)) \land (x \in X \land x ball (D) R \in f)) \to x ball (D) R \subseteq X$
26		toponuni	$⊢ J \in TopOn (X) \to X = ⋃ J$
27	14 26	syl	$⊢ ((φ \land f \in CauFil (D)) \land (x \in X \land x ball (D) R \in f)) \to X = ⋃ J$
28	25 27	sseqtrd	$⊢ ((φ \land f \in CauFil (D)) \land (x \in X \land x ball (D) R \in f)) \to x ball (D) R \subseteq ⋃ J$
29		eqid	$⊢ ⋃ J = ⋃ J$
30	29	clsss3	$⊢ (J \in Top \land x ball (D) R \subseteq ⋃ J) \to cls (J) (x ball (D) R) \subseteq ⋃ J$
31	20 28 30	syl2anc	$⊢ ((φ \land f \in CauFil (D)) \land (x \in X \land x ball (D) R \in f)) \to cls (J) (x ball (D) R) \subseteq ⋃ J$
32	31 27	sseqtrrd	$⊢ ((φ \land f \in CauFil (D)) \land (x \in X \land x ball (D) R \in f)) \to cls (J) (x ball (D) R) \subseteq X$
33	29	sscls	$⊢ (J \in Top \land x ball (D) R \subseteq ⋃ J) \to x ball (D) R \subseteq cls (J) (x ball (D) R)$
34	20 28 33	syl2anc	$⊢ ((φ \land f \in CauFil (D)) \land (x \in X \land x ball (D) R \in f)) \to x ball (D) R \subseteq cls (J) (x ball (D) R)$
35		filss	$⊢ (f \in Fil (X) \land (x ball (D) R \in f \land cls (J) (x ball (D) R) \subseteq X \land x ball (D) R \subseteq cls (J) (x ball (D) R))) \to cls (J) (x ball (D) R) \in f$
36	17 18 32 34 35	syl13anc	$⊢ ((φ \land f \in CauFil (D)) \land (x \in X \land x ball (D) R \in f)) \to cls (J) (x ball (D) R) \in f$
37		fclsrest	$⊢ (J \in TopOn (X) \land f \in Fil (X) \land cls (J) (x ball (D) R) \in f) \to (J ↾_{𝑡} cls (J) (x ball (D) R)) fClus (f ↾_{𝑡} cls (J) (x ball (D) R)) = (J fClus f) \cap cls (J) (x ball (D) R)$
38	14 17 36 37	syl3anc	$⊢ ((φ \land f \in CauFil (D)) \land (x \in X \land x ball (D) R \in f)) \to (J ↾_{𝑡} cls (J) (x ball (D) R)) fClus (f ↾_{𝑡} cls (J) (x ball (D) R)) = (J fClus f) \cap cls (J) (x ball (D) R)$
39		inss1	$⊢ (J fClus f) \cap cls (J) (x ball (D) R) \subseteq J fClus f$
40		eqid	$⊢ dom dom D = dom dom D$
41	1 40	cfilfcls	$⊢ f \in CauFil (D) \to J fClus f = J fLim f$
42	41	ad2antlr	$⊢ ((φ \land f \in CauFil (D)) \land (x \in X \land x ball (D) R \in f)) \to J fClus f = J fLim f$
43	39 42	sseqtrid	$⊢ ((φ \land f \in CauFil (D)) \land (x \in X \land x ball (D) R \in f)) \to (J fClus f) \cap cls (J) (x ball (D) R) \subseteq J fLim f$
44	38 43	eqsstrd	$⊢ ((φ \land f \in CauFil (D)) \land (x \in X \land x ball (D) R \in f)) \to (J ↾_{𝑡} cls (J) (x ball (D) R)) fClus (f ↾_{𝑡} cls (J) (x ball (D) R)) \subseteq J fLim f$
45	4	ad2ant2r	$⊢ ((φ \land f \in CauFil (D)) \land (x \in X \land x ball (D) R \in f)) \to J ↾_{𝑡} cls (J) (x ball (D) R) \in Comp$
46		filfbas	$⊢ f \in Fil (X) \to f \in fBas (X)$
47	17 46	syl	$⊢ ((φ \land f \in CauFil (D)) \land (x \in X \land x ball (D) R \in f)) \to f \in fBas (X)$
48		fbncp	$⊢ (f \in fBas (X) \land cls (J) (x ball (D) R) \in f) \to \neg X ∖ cls (J) (x ball (D) R) \in f$
49	47 36 48	syl2anc	$⊢ ((φ \land f \in CauFil (D)) \land (x \in X \land x ball (D) R \in f)) \to \neg X ∖ cls (J) (x ball (D) R) \in f$
50		trfil3	$⊢ (f \in Fil (X) \land cls (J) (x ball (D) R) \subseteq X) \to (f ↾_{𝑡} cls (J) (x ball (D) R) \in Fil (cls (J) (x ball (D) R)) \leftrightarrow \neg X ∖ cls (J) (x ball (D) R) \in f)$
51	17 32 50	syl2anc	$⊢ ((φ \land f \in CauFil (D)) \land (x \in X \land x ball (D) R \in f)) \to (f ↾_{𝑡} cls (J) (x ball (D) R) \in Fil (cls (J) (x ball (D) R)) \leftrightarrow \neg X ∖ cls (J) (x ball (D) R) \in f)$
52	49 51	mpbird	$⊢ ((φ \land f \in CauFil (D)) \land (x \in X \land x ball (D) R \in f)) \to f ↾_{𝑡} cls (J) (x ball (D) R) \in Fil (cls (J) (x ball (D) R))$
53		resttopon	$⊢ (J \in TopOn (X) \land cls (J) (x ball (D) R) \subseteq X) \to J ↾_{𝑡} cls (J) (x ball (D) R) \in TopOn (cls (J) (x ball (D) R))$
54	14 32 53	syl2anc	$⊢ ((φ \land f \in CauFil (D)) \land (x \in X \land x ball (D) R \in f)) \to J ↾_{𝑡} cls (J) (x ball (D) R) \in TopOn (cls (J) (x ball (D) R))$
55		toponuni	$⊢ J ↾_{𝑡} cls (J) (x ball (D) R) \in TopOn (cls (J) (x ball (D) R)) \to cls (J) (x ball (D) R) = ⋃ (J ↾_{𝑡} cls (J) (x ball (D) R))$
56	54 55	syl	$⊢ ((φ \land f \in CauFil (D)) \land (x \in X \land x ball (D) R \in f)) \to cls (J) (x ball (D) R) = ⋃ (J ↾_{𝑡} cls (J) (x ball (D) R))$
57	56	fveq2d	$⊢ ((φ \land f \in CauFil (D)) \land (x \in X \land x ball (D) R \in f)) \to Fil (cls (J) (x ball (D) R)) = Fil (⋃ (J ↾_{𝑡} cls (J) (x ball (D) R)))$
58	52 57	eleqtrd	$⊢ ((φ \land f \in CauFil (D)) \land (x \in X \land x ball (D) R \in f)) \to f ↾_{𝑡} cls (J) (x ball (D) R) \in Fil (⋃ (J ↾_{𝑡} cls (J) (x ball (D) R)))$
59		eqid	$⊢ ⋃ (J ↾_{𝑡} cls (J) (x ball (D) R)) = ⋃ (J ↾_{𝑡} cls (J) (x ball (D) R))$
60	59	fclscmpi	$⊢ (J ↾_{𝑡} cls (J) (x ball (D) R) \in Comp \land f ↾_{𝑡} cls (J) (x ball (D) R) \in Fil (⋃ (J ↾_{𝑡} cls (J) (x ball (D) R)))) \to (J ↾_{𝑡} cls (J) (x ball (D) R)) fClus (f ↾_{𝑡} cls (J) (x ball (D) R)) \neq \emptyset$
61	45 58 60	syl2anc	$⊢ ((φ \land f \in CauFil (D)) \land (x \in X \land x ball (D) R \in f)) \to (J ↾_{𝑡} cls (J) (x ball (D) R)) fClus (f ↾_{𝑡} cls (J) (x ball (D) R)) \neq \emptyset$
62		ssn0	$⊢ ((J ↾_{𝑡} cls (J) (x ball (D) R)) fClus (f ↾_{𝑡} cls (J) (x ball (D) R)) \subseteq J fLim f \land (J ↾_{𝑡} cls (J) (x ball (D) R)) fClus (f ↾_{𝑡} cls (J) (x ball (D) R)) \neq \emptyset) \to J fLim f \neq \emptyset$
63	44 61 62	syl2anc	$⊢ ((φ \land f \in CauFil (D)) \land (x \in X \land x ball (D) R \in f)) \to J fLim f \neq \emptyset$
64	11 63	rexlimddv	$⊢ (φ \land f \in CauFil (D)) \to J fLim f \neq \emptyset$
65	64	ralrimiva	$⊢ φ \to \forall f \in CauFil (D) J fLim f \neq \emptyset$
66	1	iscmet	$⊢ D \in CMet (X) \leftrightarrow (D \in Met (X) \land \forall f \in CauFil (D) J fLim f \neq \emptyset)$
67	2 65 66	sylanbrc	$⊢ φ \to D \in CMet (X)$

Metamath Proof Explorer

Theorem relcmpcmet

Proof