Metamath Proof Explorer

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 syl5bb ⊢ ( ( ( ( 𝐷 ∈ ( ∞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 ‘ 𝐷 ) 𝑅 ) ∈ 𝐹 )