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 
|- ( ( D e. ( *Met ` X ) /\ F e. ( CauFil ` D ) /\ R e. RR+ ) -> E. x e. X ( x ( ball ` D ) R ) e. F )

Proof

Step Hyp Ref Expression
1 cfili 
 |-  ( ( F e. ( CauFil ` D ) /\ R e. RR+ ) -> E. s e. F A. x e. s A. y e. s ( x D y ) < R )
2 1 3adant1 
 |-  ( ( D e. ( *Met ` X ) /\ F e. ( CauFil ` D ) /\ R e. RR+ ) -> E. s e. F A. x e. s A. y e. s ( x D y ) < R )
3 cfilfil 
 |-  ( ( D e. ( *Met ` X ) /\ F e. ( CauFil ` D ) ) -> F e. ( Fil ` X ) )
4 3 3adant3 
 |-  ( ( D e. ( *Met ` X ) /\ F e. ( CauFil ` D ) /\ R e. RR+ ) -> F e. ( Fil ` X ) )
5 fileln0 
 |-  ( ( F e. ( Fil ` X ) /\ s e. F ) -> s =/= (/) )
6 4 5 sylan 
 |-  ( ( ( D e. ( *Met ` X ) /\ F e. ( CauFil ` D ) /\ R e. RR+ ) /\ s e. F ) -> s =/= (/) )
7 r19.2z 
 |-  ( ( s =/= (/) /\ A. x e. s A. y e. s ( x D y ) < R ) -> E. x e. s A. y e. s ( x D y ) < R )
8 7 ex 
 |-  ( s =/= (/) -> ( A. x e. s A. y e. s ( x D y ) < R -> E. x e. s A. y e. s ( x D y ) < R ) )
9 6 8 syl 
 |-  ( ( ( D e. ( *Met ` X ) /\ F e. ( CauFil ` D ) /\ R e. RR+ ) /\ s e. F ) -> ( A. x e. s A. y e. s ( x D y ) < R -> E. x e. s A. y e. s ( x D y ) < R ) )
10 filelss 
 |-  ( ( F e. ( Fil ` X ) /\ s e. F ) -> s C_ X )
11 4 10 sylan 
 |-  ( ( ( D e. ( *Met ` X ) /\ F e. ( CauFil ` D ) /\ R e. RR+ ) /\ s e. F ) -> s C_ X )
12 ssrexv 
 |-  ( s C_ X -> ( E. x e. s A. y e. s ( x D y ) < R -> E. x e. X A. y e. s ( x D y ) < R ) )
13 11 12 syl 
 |-  ( ( ( D e. ( *Met ` X ) /\ F e. ( CauFil ` D ) /\ R e. RR+ ) /\ s e. F ) -> ( E. x e. s A. y e. s ( x D y ) < R -> E. x e. X A. y e. s ( x D y ) < R ) )
14 dfss3 
 |-  ( s C_ ( x ( ball ` D ) R ) <-> A. y e. s y e. ( x ( ball ` D ) R ) )
15 simpl1 
 |-  ( ( ( D e. ( *Met ` X ) /\ F e. ( CauFil ` D ) /\ R e. RR+ ) /\ s e. F ) -> D e. ( *Met ` X ) )
16 15 ad2antrr 
 |-  ( ( ( ( ( D e. ( *Met ` X ) /\ F e. ( CauFil ` D ) /\ R e. RR+ ) /\ s e. F ) /\ x e. X ) /\ y e. s ) -> D e. ( *Met ` X ) )
17 simpll3 
 |-  ( ( ( ( D e. ( *Met ` X ) /\ F e. ( CauFil ` D ) /\ R e. RR+ ) /\ s e. F ) /\ x e. X ) -> R e. RR+ )
18 17 rpxrd 
 |-  ( ( ( ( D e. ( *Met ` X ) /\ F e. ( CauFil ` D ) /\ R e. RR+ ) /\ s e. F ) /\ x e. X ) -> R e. RR* )
19 18 adantr 
 |-  ( ( ( ( ( D e. ( *Met ` X ) /\ F e. ( CauFil ` D ) /\ R e. RR+ ) /\ s e. F ) /\ x e. X ) /\ y e. s ) -> R e. RR* )
20 simplr 
 |-  ( ( ( ( ( D e. ( *Met ` X ) /\ F e. ( CauFil ` D ) /\ R e. RR+ ) /\ s e. F ) /\ x e. X ) /\ y e. s ) -> x e. X )
21 11 adantr 
 |-  ( ( ( ( D e. ( *Met ` X ) /\ F e. ( CauFil ` D ) /\ R e. RR+ ) /\ s e. F ) /\ x e. X ) -> s C_ X )
22 21 sselda 
 |-  ( ( ( ( ( D e. ( *Met ` X ) /\ F e. ( CauFil ` D ) /\ R e. RR+ ) /\ s e. F ) /\ x e. X ) /\ y e. s ) -> y e. X )
23 elbl2 
 |-  ( ( ( D e. ( *Met ` X ) /\ R e. RR* ) /\ ( x e. X /\ y e. X ) ) -> ( y e. ( x ( ball ` D ) R ) <-> ( x D y ) < R ) )
24 16 19 20 22 23 syl22anc 
 |-  ( ( ( ( ( D e. ( *Met ` X ) /\ F e. ( CauFil ` D ) /\ R e. RR+ ) /\ s e. F ) /\ x e. X ) /\ y e. s ) -> ( y e. ( x ( ball ` D ) R ) <-> ( x D y ) < R ) )
25 24 ralbidva 
 |-  ( ( ( ( D e. ( *Met ` X ) /\ F e. ( CauFil ` D ) /\ R e. RR+ ) /\ s e. F ) /\ x e. X ) -> ( A. y e. s y e. ( x ( ball ` D ) R ) <-> A. y e. s ( x D y ) < R ) )
26 14 25 bitrid 
 |-  ( ( ( ( D e. ( *Met ` X ) /\ F e. ( CauFil ` D ) /\ R e. RR+ ) /\ s e. F ) /\ x e. X ) -> ( s C_ ( x ( ball ` D ) R ) <-> A. y e. s ( x D y ) < R ) )
27 4 ad2antrr 
 |-  ( ( ( ( D e. ( *Met ` X ) /\ F e. ( CauFil ` D ) /\ R e. RR+ ) /\ s e. F ) /\ x e. X ) -> F e. ( Fil ` X ) )
28 simplr 
 |-  ( ( ( ( D e. ( *Met ` X ) /\ F e. ( CauFil ` D ) /\ R e. RR+ ) /\ s e. F ) /\ x e. X ) -> s e. F )
29 15 adantr 
 |-  ( ( ( ( D e. ( *Met ` X ) /\ F e. ( CauFil ` D ) /\ R e. RR+ ) /\ s e. F ) /\ x e. X ) -> D e. ( *Met ` X ) )
30 simpr 
 |-  ( ( ( ( D e. ( *Met ` X ) /\ F e. ( CauFil ` D ) /\ R e. RR+ ) /\ s e. F ) /\ x e. X ) -> x e. X )
31 blssm 
 |-  ( ( D e. ( *Met ` X ) /\ x e. X /\ R e. RR* ) -> ( x ( ball ` D ) R ) C_ X )
32 29 30 18 31 syl3anc 
 |-  ( ( ( ( D e. ( *Met ` X ) /\ F e. ( CauFil ` D ) /\ R e. RR+ ) /\ s e. F ) /\ x e. X ) -> ( x ( ball ` D ) R ) C_ X )
33 filss 
 |-  ( ( F e. ( Fil ` X ) /\ ( s e. F /\ ( x ( ball ` D ) R ) C_ X /\ s C_ ( x ( ball ` D ) R ) ) ) -> ( x ( ball ` D ) R ) e. F )
34 33 3exp2 
 |-  ( F e. ( Fil ` X ) -> ( s e. F -> ( ( x ( ball ` D ) R ) C_ X -> ( s C_ ( x ( ball ` D ) R ) -> ( x ( ball ` D ) R ) e. F ) ) ) )
35 27 28 32 34 syl3c 
 |-  ( ( ( ( D e. ( *Met ` X ) /\ F e. ( CauFil ` D ) /\ R e. RR+ ) /\ s e. F ) /\ x e. X ) -> ( s C_ ( x ( ball ` D ) R ) -> ( x ( ball ` D ) R ) e. F ) )
36 26 35 sylbird 
 |-  ( ( ( ( D e. ( *Met ` X ) /\ F e. ( CauFil ` D ) /\ R e. RR+ ) /\ s e. F ) /\ x e. X ) -> ( A. y e. s ( x D y ) < R -> ( x ( ball ` D ) R ) e. F ) )
37 36 reximdva 
 |-  ( ( ( D e. ( *Met ` X ) /\ F e. ( CauFil ` D ) /\ R e. RR+ ) /\ s e. F ) -> ( E. x e. X A. y e. s ( x D y ) < R -> E. x e. X ( x ( ball ` D ) R ) e. F ) )
38 9 13 37 3syld 
 |-  ( ( ( D e. ( *Met ` X ) /\ F e. ( CauFil ` D ) /\ R e. RR+ ) /\ s e. F ) -> ( A. x e. s A. y e. s ( x D y ) < R -> E. x e. X ( x ( ball ` D ) R ) e. F ) )
39 38 rexlimdva 
 |-  ( ( D e. ( *Met ` X ) /\ F e. ( CauFil ` D ) /\ R e. RR+ ) -> ( E. s e. F A. x e. s A. y e. s ( x D y ) < R -> E. x e. X ( x ( ball ` D ) R ) e. F ) )
40 2 39 mpd 
 |-  ( ( D e. ( *Met ` X ) /\ F e. ( CauFil ` D ) /\ R e. RR+ ) -> E. x e. X ( x ( ball ` D ) R ) e. F )