flimcfil

Description: Every convergent filter in a metric space is a Cauchy filter. (Contributed by Mario Carneiro, 15-Oct-2015)

		Ref	Expression
	Hypothesis	lmcau.1	$⊢ J = MetOpen (D)$
	Assertion	flimcfil	$⊢ (D \in ∞Met (X) \land A \in (J fLim F)) \to F \in CauFil (D)$

Proof

Step	Hyp	Ref	Expression
1		lmcau.1	$⊢ J = MetOpen (D)$
2		eqid	$⊢ ⋃ J = ⋃ J$
3	2	flimfil	$⊢ A \in (J fLim F) \to F \in Fil (⋃ J)$
4	3	adantl	$⊢ (D \in ∞Met (X) \land A \in (J fLim F)) \to F \in Fil (⋃ J)$
5	1	mopnuni	$⊢ D \in ∞Met (X) \to X = ⋃ J$
6	5	adantr	$⊢ (D \in ∞Met (X) \land A \in (J fLim F)) \to X = ⋃ J$
7	6	fveq2d	$⊢ (D \in ∞Met (X) \land A \in (J fLim F)) \to Fil (X) = Fil (⋃ J)$
8	4 7	eleqtrrd	$⊢ (D \in ∞Met (X) \land A \in (J fLim F)) \to F \in Fil (X)$
9	2	flimelbas	$⊢ A \in (J fLim F) \to A \in ⋃ J$
10	9	ad2antlr	$⊢ ((D \in ∞Met (X) \land A \in (J fLim F)) \land x \in ℝ^{+}) \to A \in ⋃ J$
11	5	ad2antrr	$⊢ ((D \in ∞Met (X) \land A \in (J fLim F)) \land x \in ℝ^{+}) \to X = ⋃ J$
12	10 11	eleqtrrd	$⊢ ((D \in ∞Met (X) \land A \in (J fLim F)) \land x \in ℝ^{+}) \to A \in X$
13		simplr	$⊢ ((D \in ∞Met (X) \land A \in (J fLim F)) \land x \in ℝ^{+}) \to A \in (J fLim F)$
14	1	mopntop	$⊢ D \in ∞Met (X) \to J \in Top$
15	14	ad2antrr	$⊢ ((D \in ∞Met (X) \land A \in (J fLim F)) \land x \in ℝ^{+}) \to J \in Top$
16		simpll	$⊢ ((D \in ∞Met (X) \land A \in (J fLim F)) \land x \in ℝ^{+}) \to D \in ∞Met (X)$
17		rpxr	$⊢ x \in ℝ^{+} \to x \in ℝ^{*}$
18	17	adantl	$⊢ ((D \in ∞Met (X) \land A \in (J fLim F)) \land x \in ℝ^{+}) \to x \in ℝ^{*}$
19	1	blopn	$⊢ (D \in ∞Met (X) \land A \in X \land x \in ℝ^{*}) \to A ball (D) x \in J$
20	16 12 18 19	syl3anc	$⊢ ((D \in ∞Met (X) \land A \in (J fLim F)) \land x \in ℝ^{+}) \to A ball (D) x \in J$
21		simpr	$⊢ ((D \in ∞Met (X) \land A \in (J fLim F)) \land x \in ℝ^{+}) \to x \in ℝ^{+}$
22		blcntr	$⊢ (D \in ∞Met (X) \land A \in X \land x \in ℝ^{+}) \to A \in (A ball (D) x)$
23	16 12 21 22	syl3anc	$⊢ ((D \in ∞Met (X) \land A \in (J fLim F)) \land x \in ℝ^{+}) \to A \in (A ball (D) x)$
24		opnneip	$⊢ (J \in Top \land A ball (D) x \in J \land A \in (A ball (D) x)) \to A ball (D) x \in nei (J) (\{A\})$
25	15 20 23 24	syl3anc	$⊢ ((D \in ∞Met (X) \land A \in (J fLim F)) \land x \in ℝ^{+}) \to A ball (D) x \in nei (J) (\{A\})$
26		flimnei	$⊢ (A \in (J fLim F) \land A ball (D) x \in nei (J) (\{A\})) \to A ball (D) x \in F$
27	13 25 26	syl2anc	$⊢ ((D \in ∞Met (X) \land A \in (J fLim F)) \land x \in ℝ^{+}) \to A ball (D) x \in F$
28		oveq1	$⊢ y = A \to y ball (D) x = A ball (D) x$
29	28	eleq1d	$⊢ y = A \to (y ball (D) x \in F \leftrightarrow A ball (D) x \in F)$
30	29	rspcev	$⊢ (A \in X \land A ball (D) x \in F) \to \exists y \in X y ball (D) x \in F$
31	12 27 30	syl2anc	$⊢ ((D \in ∞Met (X) \land A \in (J fLim F)) \land x \in ℝ^{+}) \to \exists y \in X y ball (D) x \in F$
32	31	ralrimiva	$⊢ (D \in ∞Met (X) \land A \in (J fLim F)) \to \forall x \in ℝ^{+} \exists y \in X y ball (D) x \in F$
33		iscfil3	$⊢ D \in ∞Met (X) \to (F \in CauFil (D) \leftrightarrow (F \in Fil (X) \land \forall x \in ℝ^{+} \exists y \in X y ball (D) x \in F))$
34	33	adantr	$⊢ (D \in ∞Met (X) \land A \in (J fLim F)) \to (F \in CauFil (D) \leftrightarrow (F \in Fil (X) \land \forall x \in ℝ^{+} \exists y \in X y ball (D) x \in F))$
35	8 32 34	mpbir2and	$⊢ (D \in ∞Met (X) \land A \in (J fLim F)) \to F \in CauFil (D)$

Metamath Proof Explorer

Theorem flimcfil

Proof