Theorem cfil3i

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

	Ref	Expression
Assertion	cfil3i	⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐹 ∈ ( CauFil ‘ 𝐷 ) ∧ 𝑅 ∈ ℝ+ ) → ∃ 𝑥 ∈ 𝑋 ( 𝑥 ( ball ‘ 𝐷 ) 𝑅 ) ∈ 𝐹 )

Proof

Step	Hyp	Ref	Expression
1		cfili	⊢ ( ( 𝐹 ∈ ( CauFil ‘ 𝐷 ) ∧ 𝑅 ∈ ℝ+ ) → ∃ 𝑠 ∈ 𝐹 ∀ 𝑥 ∈ 𝑠 ∀ 𝑦 ∈ 𝑠 ( 𝑥 𝐷 𝑦 ) < 𝑅 )
2	1	3adant1	⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐹 ∈ ( CauFil ‘ 𝐷 ) ∧ 𝑅 ∈ ℝ+ ) → ∃ 𝑠 ∈ 𝐹 ∀ 𝑥 ∈ 𝑠 ∀ 𝑦 ∈ 𝑠 ( 𝑥 𝐷 𝑦 ) < 𝑅 )
3		cfilfil	⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐹 ∈ ( CauFil ‘ 𝐷 ) ) → 𝐹 ∈ ( Fil ‘ 𝑋 ) )
4	3	3adant3	⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐹 ∈ ( CauFil ‘ 𝐷 ) ∧ 𝑅 ∈ ℝ+ ) → 𝐹 ∈ ( Fil ‘ 𝑋 ) )
5		fileln0	⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑠 ∈ 𝐹 ) → 𝑠 ≠ ∅ )
6	4 5	sylan	⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐹 ∈ ( CauFil ‘ 𝐷 ) ∧ 𝑅 ∈ ℝ+ ) ∧ 𝑠 ∈ 𝐹 ) → 𝑠 ≠ ∅ )
7		r19.2z	⊢ ( ( 𝑠 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝑠 ∀ 𝑦 ∈ 𝑠 ( 𝑥 𝐷 𝑦 ) < 𝑅 ) → ∃ 𝑥 ∈ 𝑠 ∀ 𝑦 ∈ 𝑠 ( 𝑥 𝐷 𝑦 ) < 𝑅 )
8	7	ex	⊢ ( 𝑠 ≠ ∅ → ( ∀ 𝑥 ∈ 𝑠 ∀ 𝑦 ∈ 𝑠 ( 𝑥 𝐷 𝑦 ) < 𝑅 → ∃ 𝑥 ∈ 𝑠 ∀ 𝑦 ∈ 𝑠 ( 𝑥 𝐷 𝑦 ) < 𝑅 ) )
9	6 8	syl	⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐹 ∈ ( CauFil ‘ 𝐷 ) ∧ 𝑅 ∈ ℝ+ ) ∧ 𝑠 ∈ 𝐹 ) → ( ∀ 𝑥 ∈ 𝑠 ∀ 𝑦 ∈ 𝑠 ( 𝑥 𝐷 𝑦 ) < 𝑅 → ∃ 𝑥 ∈ 𝑠 ∀ 𝑦 ∈ 𝑠 ( 𝑥 𝐷 𝑦 ) < 𝑅 ) )
10		filelss	⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑠 ∈ 𝐹 ) → 𝑠 ⊆ 𝑋 )
11	4 10	sylan	⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐹 ∈ ( CauFil ‘ 𝐷 ) ∧ 𝑅 ∈ ℝ+ ) ∧ 𝑠 ∈ 𝐹 ) → 𝑠 ⊆ 𝑋 )
12		ssrexv	⊢ ( 𝑠 ⊆ 𝑋 → ( ∃ 𝑥 ∈ 𝑠 ∀ 𝑦 ∈ 𝑠 ( 𝑥 𝐷 𝑦 ) < 𝑅 → ∃ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑠 ( 𝑥 𝐷 𝑦 ) < 𝑅 ) )
13	11 12	syl	⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐹 ∈ ( CauFil ‘ 𝐷 ) ∧ 𝑅 ∈ ℝ+ ) ∧ 𝑠 ∈ 𝐹 ) → ( ∃ 𝑥 ∈ 𝑠 ∀ 𝑦 ∈ 𝑠 ( 𝑥 𝐷 𝑦 ) < 𝑅 → ∃ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑠 ( 𝑥 𝐷 𝑦 ) < 𝑅 ) )
14		dfss3	⊢ ( 𝑠 ⊆ ( 𝑥 ( ball ‘ 𝐷 ) 𝑅 ) ↔ ∀ 𝑦 ∈ 𝑠 𝑦 ∈ ( 𝑥 ( ball ‘ 𝐷 ) 𝑅 ) )
15		simpl1	⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐹 ∈ ( CauFil ‘ 𝐷 ) ∧ 𝑅 ∈ ℝ+ ) ∧ 𝑠 ∈ 𝐹 ) → 𝐷 ∈ ( ∞Met ‘ 𝑋 ) )
16	15	ad2antrr	⊢ ( ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐹 ∈ ( CauFil ‘ 𝐷 ) ∧ 𝑅 ∈ ℝ+ ) ∧ 𝑠 ∈ 𝐹 ) ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑦 ∈ 𝑠 ) → 𝐷 ∈ ( ∞Met ‘ 𝑋 ) )
17		simpll3	⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐹 ∈ ( CauFil ‘ 𝐷 ) ∧ 𝑅 ∈ ℝ+ ) ∧ 𝑠 ∈ 𝐹 ) ∧ 𝑥 ∈ 𝑋 ) → 𝑅 ∈ ℝ+ )
18	17	rpxrd	⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐹 ∈ ( CauFil ‘ 𝐷 ) ∧ 𝑅 ∈ ℝ+ ) ∧ 𝑠 ∈ 𝐹 ) ∧ 𝑥 ∈ 𝑋 ) → 𝑅 ∈ ℝ* )
19	18	adantr	⊢ ( ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐹 ∈ ( CauFil ‘ 𝐷 ) ∧ 𝑅 ∈ ℝ+ ) ∧ 𝑠 ∈ 𝐹 ) ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑦 ∈ 𝑠 ) → 𝑅 ∈ ℝ* )
20		simplr	⊢ ( ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐹 ∈ ( CauFil ‘ 𝐷 ) ∧ 𝑅 ∈ ℝ+ ) ∧ 𝑠 ∈ 𝐹 ) ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑦 ∈ 𝑠 ) → 𝑥 ∈ 𝑋 )
21	11	adantr	⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐹 ∈ ( CauFil ‘ 𝐷 ) ∧ 𝑅 ∈ ℝ+ ) ∧ 𝑠 ∈ 𝐹 ) ∧ 𝑥 ∈ 𝑋 ) → 𝑠 ⊆ 𝑋 )
22	21	sselda	⊢ ( ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐹 ∈ ( CauFil ‘ 𝐷 ) ∧ 𝑅 ∈ ℝ+ ) ∧ 𝑠 ∈ 𝐹 ) ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑦 ∈ 𝑠 ) → 𝑦 ∈ 𝑋 )
23		elbl2	⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑅 ∈ ℝ* ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → ( 𝑦 ∈ ( 𝑥 ( ball ‘ 𝐷 ) 𝑅 ) ↔ ( 𝑥 𝐷 𝑦 ) < 𝑅 ) )
24	16 19 20 22 23	syl22anc	⊢ ( ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐹 ∈ ( CauFil ‘ 𝐷 ) ∧ 𝑅 ∈ ℝ+ ) ∧ 𝑠 ∈ 𝐹 ) ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑦 ∈ 𝑠 ) → ( 𝑦 ∈ ( 𝑥 ( ball ‘ 𝐷 ) 𝑅 ) ↔ ( 𝑥 𝐷 𝑦 ) < 𝑅 ) )
25	24	ralbidva	⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐹 ∈ ( CauFil ‘ 𝐷 ) ∧ 𝑅 ∈ ℝ+ ) ∧ 𝑠 ∈ 𝐹 ) ∧ 𝑥 ∈ 𝑋 ) → ( ∀ 𝑦 ∈ 𝑠 𝑦 ∈ ( 𝑥 ( ball ‘ 𝐷 ) 𝑅 ) ↔ ∀ 𝑦 ∈ 𝑠 ( 𝑥 𝐷 𝑦 ) < 𝑅 ) )
26	14 25	bitrid	⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐹 ∈ ( CauFil ‘ 𝐷 ) ∧ 𝑅 ∈ ℝ+ ) ∧ 𝑠 ∈ 𝐹 ) ∧ 𝑥 ∈ 𝑋 ) → ( 𝑠 ⊆ ( 𝑥 ( ball ‘ 𝐷 ) 𝑅 ) ↔ ∀ 𝑦 ∈ 𝑠 ( 𝑥 𝐷 𝑦 ) < 𝑅 ) )
27	4	ad2antrr	⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐹 ∈ ( CauFil ‘ 𝐷 ) ∧ 𝑅 ∈ ℝ+ ) ∧ 𝑠 ∈ 𝐹 ) ∧ 𝑥 ∈ 𝑋 ) → 𝐹 ∈ ( Fil ‘ 𝑋 ) )
28		simplr	⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐹 ∈ ( CauFil ‘ 𝐷 ) ∧ 𝑅 ∈ ℝ+ ) ∧ 𝑠 ∈ 𝐹 ) ∧ 𝑥 ∈ 𝑋 ) → 𝑠 ∈ 𝐹 )
29	15	adantr	⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐹 ∈ ( CauFil ‘ 𝐷 ) ∧ 𝑅 ∈ ℝ+ ) ∧ 𝑠 ∈ 𝐹 ) ∧ 𝑥 ∈ 𝑋 ) → 𝐷 ∈ ( ∞Met ‘ 𝑋 ) )
30		simpr	⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐹 ∈ ( CauFil ‘ 𝐷 ) ∧ 𝑅 ∈ ℝ+ ) ∧ 𝑠 ∈ 𝐹 ) ∧ 𝑥 ∈ 𝑋 ) → 𝑥 ∈ 𝑋 )
31		blssm	⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑥 ∈ 𝑋 ∧ 𝑅 ∈ ℝ* ) → ( 𝑥 ( ball ‘ 𝐷 ) 𝑅 ) ⊆ 𝑋 )
32	29 30 18 31	syl3anc	⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐹 ∈ ( CauFil ‘ 𝐷 ) ∧ 𝑅 ∈ ℝ+ ) ∧ 𝑠 ∈ 𝐹 ) ∧ 𝑥 ∈ 𝑋 ) → ( 𝑥 ( ball ‘ 𝐷 ) 𝑅 ) ⊆ 𝑋 )
33		filss	⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ ( 𝑠 ∈ 𝐹 ∧ ( 𝑥 ( ball ‘ 𝐷 ) 𝑅 ) ⊆ 𝑋 ∧ 𝑠 ⊆ ( 𝑥 ( ball ‘ 𝐷 ) 𝑅 ) ) ) → ( 𝑥 ( ball ‘ 𝐷 ) 𝑅 ) ∈ 𝐹 )
34	33	3exp2	⊢ ( 𝐹 ∈ ( Fil ‘ 𝑋 ) → ( 𝑠 ∈ 𝐹 → ( ( 𝑥 ( ball ‘ 𝐷 ) 𝑅 ) ⊆ 𝑋 → ( 𝑠 ⊆ ( 𝑥 ( ball ‘ 𝐷 ) 𝑅 ) → ( 𝑥 ( ball ‘ 𝐷 ) 𝑅 ) ∈ 𝐹 ) ) ) )
35	27 28 32 34	syl3c	⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐹 ∈ ( CauFil ‘ 𝐷 ) ∧ 𝑅 ∈ ℝ+ ) ∧ 𝑠 ∈ 𝐹 ) ∧ 𝑥 ∈ 𝑋 ) → ( 𝑠 ⊆ ( 𝑥 ( ball ‘ 𝐷 ) 𝑅 ) → ( 𝑥 ( ball ‘ 𝐷 ) 𝑅 ) ∈ 𝐹 ) )
36	26 35	sylbird	⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐹 ∈ ( CauFil ‘ 𝐷 ) ∧ 𝑅 ∈ ℝ+ ) ∧ 𝑠 ∈ 𝐹 ) ∧ 𝑥 ∈ 𝑋 ) → ( ∀ 𝑦 ∈ 𝑠 ( 𝑥 𝐷 𝑦 ) < 𝑅 → ( 𝑥 ( ball ‘ 𝐷 ) 𝑅 ) ∈ 𝐹 ) )
37	36	reximdva	⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐹 ∈ ( CauFil ‘ 𝐷 ) ∧ 𝑅 ∈ ℝ+ ) ∧ 𝑠 ∈ 𝐹 ) → ( ∃ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑠 ( 𝑥 𝐷 𝑦 ) < 𝑅 → ∃ 𝑥 ∈ 𝑋 ( 𝑥 ( ball ‘ 𝐷 ) 𝑅 ) ∈ 𝐹 ) )
38	9 13 37	3syld	⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐹 ∈ ( CauFil ‘ 𝐷 ) ∧ 𝑅 ∈ ℝ+ ) ∧ 𝑠 ∈ 𝐹 ) → ( ∀ 𝑥 ∈ 𝑠 ∀ 𝑦 ∈ 𝑠 ( 𝑥 𝐷 𝑦 ) < 𝑅 → ∃ 𝑥 ∈ 𝑋 ( 𝑥 ( ball ‘ 𝐷 ) 𝑅 ) ∈ 𝐹 ) )
39	38	rexlimdva	⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐹 ∈ ( CauFil ‘ 𝐷 ) ∧ 𝑅 ∈ ℝ+ ) → ( ∃ 𝑠 ∈ 𝐹 ∀ 𝑥 ∈ 𝑠 ∀ 𝑦 ∈ 𝑠 ( 𝑥 𝐷 𝑦 ) < 𝑅 → ∃ 𝑥 ∈ 𝑋 ( 𝑥 ( ball ‘ 𝐷 ) 𝑅 ) ∈ 𝐹 ) )
40	2 39	mpd	⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐹 ∈ ( CauFil ‘ 𝐷 ) ∧ 𝑅 ∈ ℝ+ ) → ∃ 𝑥 ∈ 𝑋 ( 𝑥 ( ball ‘ 𝐷 ) 𝑅 ) ∈ 𝐹 )