Metamath Proof Explorer

Theorem iscfil3

Description: A filter is Cauchy iff it contains a ball of any chosen size. (Contributed by Mario Carneiro, 15-Oct-2015)

Ref Expression
Assertion iscfil3 
|- ( D e. ( *Met ` X ) -> ( F e. ( CauFil ` D ) <-> ( F e. ( Fil ` X ) /\ A. r e. RR+ E. x e. X ( x ( ball ` D ) r ) e. F ) ) )

Proof

Step Hyp Ref Expression
1 cfilfil 
 |-  ( ( D e. ( *Met ` X ) /\ F e. ( CauFil ` D ) ) -> F e. ( Fil ` X ) )
2 cfil3i 
 |-  ( ( D e. ( *Met ` X ) /\ F e. ( CauFil ` D ) /\ r e. RR+ ) -> E. x e. X ( x ( ball ` D ) r ) e. F )
3 2 3expa 
 |-  ( ( ( D e. ( *Met ` X ) /\ F e. ( CauFil ` D ) ) /\ r e. RR+ ) -> E. x e. X ( x ( ball ` D ) r ) e. F )
4 3 ralrimiva 
 |-  ( ( D e. ( *Met ` X ) /\ F e. ( CauFil ` D ) ) -> A. r e. RR+ E. x e. X ( x ( ball ` D ) r ) e. F )
5 1 4 jca 
 |-  ( ( D e. ( *Met ` X ) /\ F e. ( CauFil ` D ) ) -> ( F e. ( Fil ` X ) /\ A. r e. RR+ E. x e. X ( x ( ball ` D ) r ) e. F ) )
6 simprl 
 |-  ( ( D e. ( *Met ` X ) /\ ( F e. ( Fil ` X ) /\ A. r e. RR+ E. x e. X ( x ( ball ` D ) r ) e. F ) ) -> F e. ( Fil ` X ) )
7 rphalfcl 
 |-  ( s e. RR+ -> ( s / 2 ) e. RR+ )
8 7 adantl 
 |-  ( ( ( D e. ( *Met ` X ) /\ F e. ( Fil ` X ) ) /\ s e. RR+ ) -> ( s / 2 ) e. RR+ )
9 oveq2 
 |-  ( r = ( s / 2 ) -> ( x ( ball ` D ) r ) = ( x ( ball ` D ) ( s / 2 ) ) )
10 9 eleq1d 
 |-  ( r = ( s / 2 ) -> ( ( x ( ball ` D ) r ) e. F <-> ( x ( ball ` D ) ( s / 2 ) ) e. F ) )
11 10 rexbidv 
 |-  ( r = ( s / 2 ) -> ( E. x e. X ( x ( ball ` D ) r ) e. F <-> E. x e. X ( x ( ball ` D ) ( s / 2 ) ) e. F ) )
12 11 rspcv 
 |-  ( ( s / 2 ) e. RR+ -> ( A. r e. RR+ E. x e. X ( x ( ball ` D ) r ) e. F -> E. x e. X ( x ( ball ` D ) ( s / 2 ) ) e. F ) )
13 8 12 syl 
 |-  ( ( ( D e. ( *Met ` X ) /\ F e. ( Fil ` X ) ) /\ s e. RR+ ) -> ( A. r e. RR+ E. x e. X ( x ( ball ` D ) r ) e. F -> E. x e. X ( x ( ball ` D ) ( s / 2 ) ) e. F ) )
14 simprr 
 |-  ( ( ( ( D e. ( *Met ` X ) /\ F e. ( Fil ` X ) ) /\ s e. RR+ ) /\ ( x e. X /\ ( x ( ball ` D ) ( s / 2 ) ) e. F ) ) -> ( x ( ball ` D ) ( s / 2 ) ) e. F )
15 simp-4l 
 |-  ( ( ( ( ( D e. ( *Met ` X ) /\ F e. ( Fil ` X ) ) /\ s e. RR+ ) /\ ( x e. X /\ ( x ( ball ` D ) ( s / 2 ) ) e. F ) ) /\ ( u e. ( x ( ball ` D ) ( s / 2 ) ) /\ v e. ( x ( ball ` D ) ( s / 2 ) ) ) ) -> D e. ( *Met ` X ) )
16 simplrl 
 |-  ( ( ( ( ( D e. ( *Met ` X ) /\ F e. ( Fil ` X ) ) /\ s e. RR+ ) /\ ( x e. X /\ ( x ( ball ` D ) ( s / 2 ) ) e. F ) ) /\ ( u e. ( x ( ball ` D ) ( s / 2 ) ) /\ v e. ( x ( ball ` D ) ( s / 2 ) ) ) ) -> x e. X )
17 simpllr 
 |-  ( ( ( ( ( D e. ( *Met ` X ) /\ F e. ( Fil ` X ) ) /\ s e. RR+ ) /\ ( x e. X /\ ( x ( ball ` D ) ( s / 2 ) ) e. F ) ) /\ ( u e. ( x ( ball ` D ) ( s / 2 ) ) /\ v e. ( x ( ball ` D ) ( s / 2 ) ) ) ) -> s e. RR+ )
18 17 rpred 
 |-  ( ( ( ( ( D e. ( *Met ` X ) /\ F e. ( Fil ` X ) ) /\ s e. RR+ ) /\ ( x e. X /\ ( x ( ball ` D ) ( s / 2 ) ) e. F ) ) /\ ( u e. ( x ( ball ` D ) ( s / 2 ) ) /\ v e. ( x ( ball ` D ) ( s / 2 ) ) ) ) -> s e. RR )
19 simprl 
 |-  ( ( ( ( ( D e. ( *Met ` X ) /\ F e. ( Fil ` X ) ) /\ s e. RR+ ) /\ ( x e. X /\ ( x ( ball ` D ) ( s / 2 ) ) e. F ) ) /\ ( u e. ( x ( ball ` D ) ( s / 2 ) ) /\ v e. ( x ( ball ` D ) ( s / 2 ) ) ) ) -> u e. ( x ( ball ` D ) ( s / 2 ) ) )
20 blhalf 
 |-  ( ( ( D e. ( *Met ` X ) /\ x e. X ) /\ ( s e. RR /\ u e. ( x ( ball ` D ) ( s / 2 ) ) ) ) -> ( x ( ball ` D ) ( s / 2 ) ) C_ ( u ( ball ` D ) s ) )
21 15 16 18 19 20 syl22anc 
 |-  ( ( ( ( ( D e. ( *Met ` X ) /\ F e. ( Fil ` X ) ) /\ s e. RR+ ) /\ ( x e. X /\ ( x ( ball ` D ) ( s / 2 ) ) e. F ) ) /\ ( u e. ( x ( ball ` D ) ( s / 2 ) ) /\ v e. ( x ( ball ` D ) ( s / 2 ) ) ) ) -> ( x ( ball ` D ) ( s / 2 ) ) C_ ( u ( ball ` D ) s ) )
22 simprr 
 |-  ( ( ( ( ( D e. ( *Met ` X ) /\ F e. ( Fil ` X ) ) /\ s e. RR+ ) /\ ( x e. X /\ ( x ( ball ` D ) ( s / 2 ) ) e. F ) ) /\ ( u e. ( x ( ball ` D ) ( s / 2 ) ) /\ v e. ( x ( ball ` D ) ( s / 2 ) ) ) ) -> v e. ( x ( ball ` D ) ( s / 2 ) ) )
23 21 22 sseldd 
 |-  ( ( ( ( ( D e. ( *Met ` X ) /\ F e. ( Fil ` X ) ) /\ s e. RR+ ) /\ ( x e. X /\ ( x ( ball ` D ) ( s / 2 ) ) e. F ) ) /\ ( u e. ( x ( ball ` D ) ( s / 2 ) ) /\ v e. ( x ( ball ` D ) ( s / 2 ) ) ) ) -> v e. ( u ( ball ` D ) s ) )
24 17 rpxrd 
 |-  ( ( ( ( ( D e. ( *Met ` X ) /\ F e. ( Fil ` X ) ) /\ s e. RR+ ) /\ ( x e. X /\ ( x ( ball ` D ) ( s / 2 ) ) e. F ) ) /\ ( u e. ( x ( ball ` D ) ( s / 2 ) ) /\ v e. ( x ( ball ` D ) ( s / 2 ) ) ) ) -> s e. RR* )
25 17 7 syl 
 |-  ( ( ( ( ( D e. ( *Met ` X ) /\ F e. ( Fil ` X ) ) /\ s e. RR+ ) /\ ( x e. X /\ ( x ( ball ` D ) ( s / 2 ) ) e. F ) ) /\ ( u e. ( x ( ball ` D ) ( s / 2 ) ) /\ v e. ( x ( ball ` D ) ( s / 2 ) ) ) ) -> ( s / 2 ) e. RR+ )
26 25 rpxrd 
 |-  ( ( ( ( ( D e. ( *Met ` X ) /\ F e. ( Fil ` X ) ) /\ s e. RR+ ) /\ ( x e. X /\ ( x ( ball ` D ) ( s / 2 ) ) e. F ) ) /\ ( u e. ( x ( ball ` D ) ( s / 2 ) ) /\ v e. ( x ( ball ` D ) ( s / 2 ) ) ) ) -> ( s / 2 ) e. RR* )
27 blssm 
 |-  ( ( D e. ( *Met ` X ) /\ x e. X /\ ( s / 2 ) e. RR* ) -> ( x ( ball ` D ) ( s / 2 ) ) C_ X )
28 15 16 26 27 syl3anc 
 |-  ( ( ( ( ( D e. ( *Met ` X ) /\ F e. ( Fil ` X ) ) /\ s e. RR+ ) /\ ( x e. X /\ ( x ( ball ` D ) ( s / 2 ) ) e. F ) ) /\ ( u e. ( x ( ball ` D ) ( s / 2 ) ) /\ v e. ( x ( ball ` D ) ( s / 2 ) ) ) ) -> ( x ( ball ` D ) ( s / 2 ) ) C_ X )
29 28 19 sseldd 
 |-  ( ( ( ( ( D e. ( *Met ` X ) /\ F e. ( Fil ` X ) ) /\ s e. RR+ ) /\ ( x e. X /\ ( x ( ball ` D ) ( s / 2 ) ) e. F ) ) /\ ( u e. ( x ( ball ` D ) ( s / 2 ) ) /\ v e. ( x ( ball ` D ) ( s / 2 ) ) ) ) -> u e. X )
30 28 22 sseldd 
 |-  ( ( ( ( ( D e. ( *Met ` X ) /\ F e. ( Fil ` X ) ) /\ s e. RR+ ) /\ ( x e. X /\ ( x ( ball ` D ) ( s / 2 ) ) e. F ) ) /\ ( u e. ( x ( ball ` D ) ( s / 2 ) ) /\ v e. ( x ( ball ` D ) ( s / 2 ) ) ) ) -> v e. X )
31 elbl2 
 |-  ( ( ( D e. ( *Met ` X ) /\ s e. RR* ) /\ ( u e. X /\ v e. X ) ) -> ( v e. ( u ( ball ` D ) s ) <-> ( u D v ) < s ) )
32 15 24 29 30 31 syl22anc 
 |-  ( ( ( ( ( D e. ( *Met ` X ) /\ F e. ( Fil ` X ) ) /\ s e. RR+ ) /\ ( x e. X /\ ( x ( ball ` D ) ( s / 2 ) ) e. F ) ) /\ ( u e. ( x ( ball ` D ) ( s / 2 ) ) /\ v e. ( x ( ball ` D ) ( s / 2 ) ) ) ) -> ( v e. ( u ( ball ` D ) s ) <-> ( u D v ) < s ) )
33 23 32 mpbid 
 |-  ( ( ( ( ( D e. ( *Met ` X ) /\ F e. ( Fil ` X ) ) /\ s e. RR+ ) /\ ( x e. X /\ ( x ( ball ` D ) ( s / 2 ) ) e. F ) ) /\ ( u e. ( x ( ball ` D ) ( s / 2 ) ) /\ v e. ( x ( ball ` D ) ( s / 2 ) ) ) ) -> ( u D v ) < s )
34 33 ralrimivva 
 |-  ( ( ( ( D e. ( *Met ` X ) /\ F e. ( Fil ` X ) ) /\ s e. RR+ ) /\ ( x e. X /\ ( x ( ball ` D ) ( s / 2 ) ) e. F ) ) -> A. u e. ( x ( ball ` D ) ( s / 2 ) ) A. v e. ( x ( ball ` D ) ( s / 2 ) ) ( u D v ) < s )
35 raleq 
 |-  ( y = ( x ( ball ` D ) ( s / 2 ) ) -> ( A. v e. y ( u D v ) < s <-> A. v e. ( x ( ball ` D ) ( s / 2 ) ) ( u D v ) < s ) )
36 35 raleqbi1dv 
 |-  ( y = ( x ( ball ` D ) ( s / 2 ) ) -> ( A. u e. y A. v e. y ( u D v ) < s <-> A. u e. ( x ( ball ` D ) ( s / 2 ) ) A. v e. ( x ( ball ` D ) ( s / 2 ) ) ( u D v ) < s ) )
37 36 rspcev 
 |-  ( ( ( x ( ball ` D ) ( s / 2 ) ) e. F /\ A. u e. ( x ( ball ` D ) ( s / 2 ) ) A. v e. ( x ( ball ` D ) ( s / 2 ) ) ( u D v ) < s ) -> E. y e. F A. u e. y A. v e. y ( u D v ) < s )
38 14 34 37 syl2anc 
 |-  ( ( ( ( D e. ( *Met ` X ) /\ F e. ( Fil ` X ) ) /\ s e. RR+ ) /\ ( x e. X /\ ( x ( ball ` D ) ( s / 2 ) ) e. F ) ) -> E. y e. F A. u e. y A. v e. y ( u D v ) < s )
39 38 rexlimdvaa 
 |-  ( ( ( D e. ( *Met ` X ) /\ F e. ( Fil ` X ) ) /\ s e. RR+ ) -> ( E. x e. X ( x ( ball ` D ) ( s / 2 ) ) e. F -> E. y e. F A. u e. y A. v e. y ( u D v ) < s ) )
40 13 39 syld 
 |-  ( ( ( D e. ( *Met ` X ) /\ F e. ( Fil ` X ) ) /\ s e. RR+ ) -> ( A. r e. RR+ E. x e. X ( x ( ball ` D ) r ) e. F -> E. y e. F A. u e. y A. v e. y ( u D v ) < s ) )
41 40 ralrimdva 
 |-  ( ( D e. ( *Met ` X ) /\ F e. ( Fil ` X ) ) -> ( A. r e. RR+ E. x e. X ( x ( ball ` D ) r ) e. F -> A. s e. RR+ E. y e. F A. u e. y A. v e. y ( u D v ) < s ) )
42 41 impr 
 |-  ( ( D e. ( *Met ` X ) /\ ( F e. ( Fil ` X ) /\ A. r e. RR+ E. x e. X ( x ( ball ` D ) r ) e. F ) ) -> A. s e. RR+ E. y e. F A. u e. y A. v e. y ( u D v ) < s )
43 iscfil2 
 |-  ( D e. ( *Met ` X ) -> ( F e. ( CauFil ` D ) <-> ( F e. ( Fil ` X ) /\ A. s e. RR+ E. y e. F A. u e. y A. v e. y ( u D v ) < s ) ) )
44 43 adantr 
 |-  ( ( D e. ( *Met ` X ) /\ ( F e. ( Fil ` X ) /\ A. r e. RR+ E. x e. X ( x ( ball ` D ) r ) e. F ) ) -> ( F e. ( CauFil ` D ) <-> ( F e. ( Fil ` X ) /\ A. s e. RR+ E. y e. F A. u e. y A. v e. y ( u D v ) < s ) ) )
45 6 42 44 mpbir2and 
 |-  ( ( D e. ( *Met ` X ) /\ ( F e. ( Fil ` X ) /\ A. r e. RR+ E. x e. X ( x ( ball ` D ) r ) e. F ) ) -> F e. ( CauFil ` D ) )
46 5 45 impbida 
 |-  ( D e. ( *Met ` X ) -> ( F e. ( CauFil ` D ) <-> ( F e. ( Fil ` X ) /\ A. r e. RR+ E. x e. X ( x ( ball ` D ) r ) e. F ) ) )