cfil3i

Description: A Cauchy filter contains balls of any pre-chosen size. (Contributed by Mario Carneiro, 15-Oct-2015)

		Ref	Expression
	Assertion	cfil3i	$⊢ (D \in ∞Met (X) \land F \in CauFil (D) \land R \in ℝ^{+}) \to \exists x \in X x ball (D) R \in F$

Proof

Step	Hyp	Ref	Expression
1		cfili	$⊢ (F \in CauFil (D) \land R \in ℝ^{+}) \to \exists s \in F \forall x \in s \forall y \in s x D y < R$
2	1	3adant1	$⊢ (D \in ∞Met (X) \land F \in CauFil (D) \land R \in ℝ^{+}) \to \exists s \in F \forall x \in s \forall y \in s x D y < R$
3		cfilfil	$⊢ (D \in ∞Met (X) \land F \in CauFil (D)) \to F \in Fil (X)$
4	3	3adant3	$⊢ (D \in ∞Met (X) \land F \in CauFil (D) \land R \in ℝ^{+}) \to F \in Fil (X)$
5		fileln0	$⊢ (F \in Fil (X) \land s \in F) \to s \neq \emptyset$
6	4 5	sylan	$⊢ ((D \in ∞Met (X) \land F \in CauFil (D) \land R \in ℝ^{+}) \land s \in F) \to s \neq \emptyset$
7		r19.2z	$⊢ (s \neq \emptyset \land \forall x \in s \forall y \in s x D y < R) \to \exists x \in s \forall y \in s x D y < R$
8	7	ex	$⊢ s \neq \emptyset \to (\forall x \in s \forall y \in s x D y < R \to \exists x \in s \forall y \in s x D y < R)$
9	6 8	syl	$⊢ ((D \in ∞Met (X) \land F \in CauFil (D) \land R \in ℝ^{+}) \land s \in F) \to (\forall x \in s \forall y \in s x D y < R \to \exists x \in s \forall y \in s x D y < R)$
10		filelss	$⊢ (F \in Fil (X) \land s \in F) \to s \subseteq X$
11	4 10	sylan	$⊢ ((D \in ∞Met (X) \land F \in CauFil (D) \land R \in ℝ^{+}) \land s \in F) \to s \subseteq X$
12		ssrexv	$⊢ s \subseteq X \to (\exists x \in s \forall y \in s x D y < R \to \exists x \in X \forall y \in s x D y < R)$
13	11 12	syl	$⊢ ((D \in ∞Met (X) \land F \in CauFil (D) \land R \in ℝ^{+}) \land s \in F) \to (\exists x \in s \forall y \in s x D y < R \to \exists x \in X \forall y \in s x D y < R)$
14		dfss3	$⊢ s \subseteq x ball (D) R \leftrightarrow \forall y \in s y \in (x ball (D) R)$
15		simpl1	$⊢ ((D \in ∞Met (X) \land F \in CauFil (D) \land R \in ℝ^{+}) \land s \in F) \to D \in ∞Met (X)$
16	15	ad2antrr	$⊢ ((((D \in ∞Met (X) \land F \in CauFil (D) \land R \in ℝ^{+}) \land s \in F) \land x \in X) \land y \in s) \to D \in ∞Met (X)$
17		simpll3	$⊢ (((D \in ∞Met (X) \land F \in CauFil (D) \land R \in ℝ^{+}) \land s \in F) \land x \in X) \to R \in ℝ^{+}$
18	17	rpxrd	$⊢ (((D \in ∞Met (X) \land F \in CauFil (D) \land R \in ℝ^{+}) \land s \in F) \land x \in X) \to R \in ℝ^{*}$
19	18	adantr	$⊢ ((((D \in ∞Met (X) \land F \in CauFil (D) \land R \in ℝ^{+}) \land s \in F) \land x \in X) \land y \in s) \to R \in ℝ^{*}$
20		simplr	$⊢ ((((D \in ∞Met (X) \land F \in CauFil (D) \land R \in ℝ^{+}) \land s \in F) \land x \in X) \land y \in s) \to x \in X$
21	11	adantr	$⊢ (((D \in ∞Met (X) \land F \in CauFil (D) \land R \in ℝ^{+}) \land s \in F) \land x \in X) \to s \subseteq X$
22	21	sselda	$⊢ ((((D \in ∞Met (X) \land F \in CauFil (D) \land R \in ℝ^{+}) \land s \in F) \land x \in X) \land y \in s) \to y \in X$
23		elbl2	$⊢ ((D \in ∞Met (X) \land R \in ℝ^{*}) \land (x \in X \land y \in X)) \to (y \in (x ball (D) R) \leftrightarrow x D y < R)$
24	16 19 20 22 23	syl22anc	$⊢ ((((D \in ∞Met (X) \land F \in CauFil (D) \land R \in ℝ^{+}) \land s \in F) \land x \in X) \land y \in s) \to (y \in (x ball (D) R) \leftrightarrow x D y < R)$
25	24	ralbidva	$⊢ (((D \in ∞Met (X) \land F \in CauFil (D) \land R \in ℝ^{+}) \land s \in F) \land x \in X) \to (\forall y \in s y \in (x ball (D) R) \leftrightarrow \forall y \in s x D y < R)$
26	14 25	bitrid	$⊢ (((D \in ∞Met (X) \land F \in CauFil (D) \land R \in ℝ^{+}) \land s \in F) \land x \in X) \to (s \subseteq x ball (D) R \leftrightarrow \forall y \in s x D y < R)$
27	4	ad2antrr	$⊢ (((D \in ∞Met (X) \land F \in CauFil (D) \land R \in ℝ^{+}) \land s \in F) \land x \in X) \to F \in Fil (X)$
28		simplr	$⊢ (((D \in ∞Met (X) \land F \in CauFil (D) \land R \in ℝ^{+}) \land s \in F) \land x \in X) \to s \in F$
29	15	adantr	$⊢ (((D \in ∞Met (X) \land F \in CauFil (D) \land R \in ℝ^{+}) \land s \in F) \land x \in X) \to D \in ∞Met (X)$
30		simpr	$⊢ (((D \in ∞Met (X) \land F \in CauFil (D) \land R \in ℝ^{+}) \land s \in F) \land x \in X) \to x \in X$
31		blssm	$⊢ (D \in ∞Met (X) \land x \in X \land R \in ℝ^{*}) \to x ball (D) R \subseteq X$
32	29 30 18 31	syl3anc	$⊢ (((D \in ∞Met (X) \land F \in CauFil (D) \land R \in ℝ^{+}) \land s \in F) \land x \in X) \to x ball (D) R \subseteq X$
33		filss	$⊢ (F \in Fil (X) \land (s \in F \land x ball (D) R \subseteq X \land s \subseteq x ball (D) R)) \to x ball (D) R \in F$
34	33	3exp2	$⊢ F \in Fil (X) \to (s \in F \to (x ball (D) R \subseteq X \to (s \subseteq x ball (D) R \to x ball (D) R \in F)))$
35	27 28 32 34	syl3c	$⊢ (((D \in ∞Met (X) \land F \in CauFil (D) \land R \in ℝ^{+}) \land s \in F) \land x \in X) \to (s \subseteq x ball (D) R \to x ball (D) R \in F)$
36	26 35	sylbird	$⊢ (((D \in ∞Met (X) \land F \in CauFil (D) \land R \in ℝ^{+}) \land s \in F) \land x \in X) \to (\forall y \in s x D y < R \to x ball (D) R \in F)$
37	36	reximdva	$⊢ ((D \in ∞Met (X) \land F \in CauFil (D) \land R \in ℝ^{+}) \land s \in F) \to (\exists x \in X \forall y \in s x D y < R \to \exists x \in X x ball (D) R \in F)$
38	9 13 37	3syld	$⊢ ((D \in ∞Met (X) \land F \in CauFil (D) \land R \in ℝ^{+}) \land s \in F) \to (\forall x \in s \forall y \in s x D y < R \to \exists x \in X x ball (D) R \in F)$
39	38	rexlimdva	$⊢ (D \in ∞Met (X) \land F \in CauFil (D) \land R \in ℝ^{+}) \to (\exists s \in F \forall x \in s \forall y \in s x D y < R \to \exists x \in X x ball (D) R \in F)$
40	2 39	mpd	$⊢ (D \in ∞Met (X) \land F \in CauFil (D) \land R \in ℝ^{+}) \to \exists x \in X x ball (D) R \in F$

Metamath Proof Explorer

Theorem cfil3i

Proof