Metamath Proof Explorer

Theorem iscfil2

Description: The property of being a Cauchy filter. (Contributed by Mario Carneiro, 13-Oct-2015)

Ref Expression
Assertion iscfil2 
|- ( D e. ( *Met ` X ) -> ( F e. ( CauFil ` D ) <-> ( F e. ( Fil ` X ) /\ A. x e. RR+ E. y e. F A. z e. y A. w e. y ( z D w ) < x ) ) )

Proof

Step Hyp Ref Expression
1 iscfil 
 |-  ( D e. ( *Met ` X ) -> ( F e. ( CauFil ` D ) <-> ( F e. ( Fil ` X ) /\ A. x e. RR+ E. y e. F ( D " ( y X. y ) ) C_ ( 0 [,) x ) ) ) )
2 xmetf 
 |-  ( D e. ( *Met ` X ) -> D : ( X X. X ) --> RR* )
3 2 ad3antrrr 
 |-  ( ( ( ( D e. ( *Met ` X ) /\ F e. ( Fil ` X ) ) /\ x e. RR+ ) /\ y e. F ) -> D : ( X X. X ) --> RR* )
4 3 ffund 
 |-  ( ( ( ( D e. ( *Met ` X ) /\ F e. ( Fil ` X ) ) /\ x e. RR+ ) /\ y e. F ) -> Fun D )
5 filelss 
 |-  ( ( F e. ( Fil ` X ) /\ y e. F ) -> y C_ X )
6 5 ad4ant24 
 |-  ( ( ( ( D e. ( *Met ` X ) /\ F e. ( Fil ` X ) ) /\ x e. RR+ ) /\ y e. F ) -> y C_ X )
7 xpss12 
 |-  ( ( y C_ X /\ y C_ X ) -> ( y X. y ) C_ ( X X. X ) )
8 6 6 7 syl2anc 
 |-  ( ( ( ( D e. ( *Met ` X ) /\ F e. ( Fil ` X ) ) /\ x e. RR+ ) /\ y e. F ) -> ( y X. y ) C_ ( X X. X ) )
9 3 fdmd 
 |-  ( ( ( ( D e. ( *Met ` X ) /\ F e. ( Fil ` X ) ) /\ x e. RR+ ) /\ y e. F ) -> dom D = ( X X. X ) )
10 8 9 sseqtrrd 
 |-  ( ( ( ( D e. ( *Met ` X ) /\ F e. ( Fil ` X ) ) /\ x e. RR+ ) /\ y e. F ) -> ( y X. y ) C_ dom D )
11 funimassov 
 |-  ( ( Fun D /\ ( y X. y ) C_ dom D ) -> ( ( D " ( y X. y ) ) C_ ( 0 [,) x ) <-> A. z e. y A. w e. y ( z D w ) e. ( 0 [,) x ) ) )
12 4 10 11 syl2anc 
 |-  ( ( ( ( D e. ( *Met ` X ) /\ F e. ( Fil ` X ) ) /\ x e. RR+ ) /\ y e. F ) -> ( ( D " ( y X. y ) ) C_ ( 0 [,) x ) <-> A. z e. y A. w e. y ( z D w ) e. ( 0 [,) x ) ) )
13 0xr 
 |-  0 e. RR*
14 13 a1i 
 |-  ( ( ( ( ( D e. ( *Met ` X ) /\ F e. ( Fil ` X ) ) /\ x e. RR+ ) /\ y e. F ) /\ ( z e. y /\ w e. y ) ) -> 0 e. RR* )
15 simpllr 
 |-  ( ( ( ( ( D e. ( *Met ` X ) /\ F e. ( Fil ` X ) ) /\ x e. RR+ ) /\ y e. F ) /\ ( z e. y /\ w e. y ) ) -> x e. RR+ )
16 15 rpxrd 
 |-  ( ( ( ( ( D e. ( *Met ` X ) /\ F e. ( Fil ` X ) ) /\ x e. RR+ ) /\ y e. F ) /\ ( z e. y /\ w e. y ) ) -> x e. RR* )
17 simp-4l 
 |-  ( ( ( ( ( D e. ( *Met ` X ) /\ F e. ( Fil ` X ) ) /\ x e. RR+ ) /\ y e. F ) /\ ( z e. y /\ w e. y ) ) -> D e. ( *Met ` X ) )
18 6 sselda 
 |-  ( ( ( ( ( D e. ( *Met ` X ) /\ F e. ( Fil ` X ) ) /\ x e. RR+ ) /\ y e. F ) /\ z e. y ) -> z e. X )
19 18 adantrr 
 |-  ( ( ( ( ( D e. ( *Met ` X ) /\ F e. ( Fil ` X ) ) /\ x e. RR+ ) /\ y e. F ) /\ ( z e. y /\ w e. y ) ) -> z e. X )
20 6 sselda 
 |-  ( ( ( ( ( D e. ( *Met ` X ) /\ F e. ( Fil ` X ) ) /\ x e. RR+ ) /\ y e. F ) /\ w e. y ) -> w e. X )
21 20 adantrl 
 |-  ( ( ( ( ( D e. ( *Met ` X ) /\ F e. ( Fil ` X ) ) /\ x e. RR+ ) /\ y e. F ) /\ ( z e. y /\ w e. y ) ) -> w e. X )
22 xmetcl 
 |-  ( ( D e. ( *Met ` X ) /\ z e. X /\ w e. X ) -> ( z D w ) e. RR* )
23 17 19 21 22 syl3anc 
 |-  ( ( ( ( ( D e. ( *Met ` X ) /\ F e. ( Fil ` X ) ) /\ x e. RR+ ) /\ y e. F ) /\ ( z e. y /\ w e. y ) ) -> ( z D w ) e. RR* )
24 xmetge0 
 |-  ( ( D e. ( *Met ` X ) /\ z e. X /\ w e. X ) -> 0 <_ ( z D w ) )
25 17 19 21 24 syl3anc 
 |-  ( ( ( ( ( D e. ( *Met ` X ) /\ F e. ( Fil ` X ) ) /\ x e. RR+ ) /\ y e. F ) /\ ( z e. y /\ w e. y ) ) -> 0 <_ ( z D w ) )
26 elico1 
 |-  ( ( 0 e. RR* /\ x e. RR* ) -> ( ( z D w ) e. ( 0 [,) x ) <-> ( ( z D w ) e. RR* /\ 0 <_ ( z D w ) /\ ( z D w ) < x ) ) )
27 df-3an 
 |-  ( ( ( z D w ) e. RR* /\ 0 <_ ( z D w ) /\ ( z D w ) < x ) <-> ( ( ( z D w ) e. RR* /\ 0 <_ ( z D w ) ) /\ ( z D w ) < x ) )
28 26 27 bitrdi 
 |-  ( ( 0 e. RR* /\ x e. RR* ) -> ( ( z D w ) e. ( 0 [,) x ) <-> ( ( ( z D w ) e. RR* /\ 0 <_ ( z D w ) ) /\ ( z D w ) < x ) ) )
29 28 baibd 
 |-  ( ( ( 0 e. RR* /\ x e. RR* ) /\ ( ( z D w ) e. RR* /\ 0 <_ ( z D w ) ) ) -> ( ( z D w ) e. ( 0 [,) x ) <-> ( z D w ) < x ) )
30 14 16 23 25 29 syl22anc 
 |-  ( ( ( ( ( D e. ( *Met ` X ) /\ F e. ( Fil ` X ) ) /\ x e. RR+ ) /\ y e. F ) /\ ( z e. y /\ w e. y ) ) -> ( ( z D w ) e. ( 0 [,) x ) <-> ( z D w ) < x ) )
31 30 2ralbidva 
 |-  ( ( ( ( D e. ( *Met ` X ) /\ F e. ( Fil ` X ) ) /\ x e. RR+ ) /\ y e. F ) -> ( A. z e. y A. w e. y ( z D w ) e. ( 0 [,) x ) <-> A. z e. y A. w e. y ( z D w ) < x ) )
32 12 31 bitrd 
 |-  ( ( ( ( D e. ( *Met ` X ) /\ F e. ( Fil ` X ) ) /\ x e. RR+ ) /\ y e. F ) -> ( ( D " ( y X. y ) ) C_ ( 0 [,) x ) <-> A. z e. y A. w e. y ( z D w ) < x ) )
33 32 rexbidva 
 |-  ( ( ( D e. ( *Met ` X ) /\ F e. ( Fil ` X ) ) /\ x e. RR+ ) -> ( E. y e. F ( D " ( y X. y ) ) C_ ( 0 [,) x ) <-> E. y e. F A. z e. y A. w e. y ( z D w ) < x ) )
34 33 ralbidva 
 |-  ( ( D e. ( *Met ` X ) /\ F e. ( Fil ` X ) ) -> ( A. x e. RR+ E. y e. F ( D " ( y X. y ) ) C_ ( 0 [,) x ) <-> A. x e. RR+ E. y e. F A. z e. y A. w e. y ( z D w ) < x ) )
35 34 pm5.32da 
 |-  ( D e. ( *Met ` X ) -> ( ( F e. ( Fil ` X ) /\ A. x e. RR+ E. y e. F ( D " ( y X. y ) ) C_ ( 0 [,) x ) ) <-> ( F e. ( Fil ` X ) /\ A. x e. RR+ E. y e. F A. z e. y A. w e. y ( z D w ) < x ) ) )
36 1 35 bitrd 
 |-  ( D e. ( *Met ` X ) -> ( F e. ( CauFil ` D ) <-> ( F e. ( Fil ` X ) /\ A. x e. RR+ E. y e. F A. z e. y A. w e. y ( z D w ) < x ) ) )