Metamath Proof Explorer

Theorem cfilresi

Description: A Cauchy filter on a metric subspace extends to a Cauchy filter in the larger space. (Contributed by Mario Carneiro, 15-Oct-2015)

Ref Expression
Assertion cfilresi 
|- ( ( D e. ( *Met ` X ) /\ F e. ( CauFil ` ( D |` ( Y X. Y ) ) ) ) -> ( X filGen F ) e. ( CauFil ` D ) )

Proof

Step Hyp Ref Expression
1 xmetres 
 |-  ( D e. ( *Met ` X ) -> ( D |` ( Y X. Y ) ) e. ( *Met ` ( X i^i Y ) ) )
2 iscfil2 
 |-  ( ( D |` ( Y X. Y ) ) e. ( *Met ` ( X i^i Y ) ) -> ( F e. ( CauFil ` ( D |` ( Y X. Y ) ) ) <-> ( F e. ( Fil ` ( X i^i Y ) ) /\ A. x e. RR+ E. y e. F A. u e. y A. v e. y ( u ( D |` ( Y X. Y ) ) v ) < x ) ) )
3 2 simplbda 
 |-  ( ( ( D |` ( Y X. Y ) ) e. ( *Met ` ( X i^i Y ) ) /\ F e. ( CauFil ` ( D |` ( Y X. Y ) ) ) ) -> A. x e. RR+ E. y e. F A. u e. y A. v e. y ( u ( D |` ( Y X. Y ) ) v ) < x )
4 1 3 sylan 
 |-  ( ( D e. ( *Met ` X ) /\ F e. ( CauFil ` ( D |` ( Y X. Y ) ) ) ) -> A. x e. RR+ E. y e. F A. u e. y A. v e. y ( u ( D |` ( Y X. Y ) ) v ) < x )
5 cfilfil 
 |-  ( ( ( D |` ( Y X. Y ) ) e. ( *Met ` ( X i^i Y ) ) /\ F e. ( CauFil ` ( D |` ( Y X. Y ) ) ) ) -> F e. ( Fil ` ( X i^i Y ) ) )
6 1 5 sylan 
 |-  ( ( D e. ( *Met ` X ) /\ F e. ( CauFil ` ( D |` ( Y X. Y ) ) ) ) -> F e. ( Fil ` ( X i^i Y ) ) )
7 filelss 
 |-  ( ( F e. ( Fil ` ( X i^i Y ) ) /\ y e. F ) -> y C_ ( X i^i Y ) )
8 6 7 sylan 
 |-  ( ( ( D e. ( *Met ` X ) /\ F e. ( CauFil ` ( D |` ( Y X. Y ) ) ) ) /\ y e. F ) -> y C_ ( X i^i Y ) )
9 inss2 
 |-  ( X i^i Y ) C_ Y
10 8 9 sstrdi 
 |-  ( ( ( D e. ( *Met ` X ) /\ F e. ( CauFil ` ( D |` ( Y X. Y ) ) ) ) /\ y e. F ) -> y C_ Y )
11 10 sselda 
 |-  ( ( ( ( D e. ( *Met ` X ) /\ F e. ( CauFil ` ( D |` ( Y X. Y ) ) ) ) /\ y e. F ) /\ u e. y ) -> u e. Y )
12 10 sselda 
 |-  ( ( ( ( D e. ( *Met ` X ) /\ F e. ( CauFil ` ( D |` ( Y X. Y ) ) ) ) /\ y e. F ) /\ v e. y ) -> v e. Y )
13 11 12 anim12dan 
 |-  ( ( ( ( D e. ( *Met ` X ) /\ F e. ( CauFil ` ( D |` ( Y X. Y ) ) ) ) /\ y e. F ) /\ ( u e. y /\ v e. y ) ) -> ( u e. Y /\ v e. Y ) )
14 ovres 
 |-  ( ( u e. Y /\ v e. Y ) -> ( u ( D |` ( Y X. Y ) ) v ) = ( u D v ) )
15 13 14 syl 
 |-  ( ( ( ( D e. ( *Met ` X ) /\ F e. ( CauFil ` ( D |` ( Y X. Y ) ) ) ) /\ y e. F ) /\ ( u e. y /\ v e. y ) ) -> ( u ( D |` ( Y X. Y ) ) v ) = ( u D v ) )
16 15 breq1d 
 |-  ( ( ( ( D e. ( *Met ` X ) /\ F e. ( CauFil ` ( D |` ( Y X. Y ) ) ) ) /\ y e. F ) /\ ( u e. y /\ v e. y ) ) -> ( ( u ( D |` ( Y X. Y ) ) v ) < x <-> ( u D v ) < x ) )
17 16 2ralbidva 
 |-  ( ( ( D e. ( *Met ` X ) /\ F e. ( CauFil ` ( D |` ( Y X. Y ) ) ) ) /\ y e. F ) -> ( A. u e. y A. v e. y ( u ( D |` ( Y X. Y ) ) v ) < x <-> A. u e. y A. v e. y ( u D v ) < x ) )
18 17 rexbidva 
 |-  ( ( D e. ( *Met ` X ) /\ F e. ( CauFil ` ( D |` ( Y X. Y ) ) ) ) -> ( E. y e. F A. u e. y A. v e. y ( u ( D |` ( Y X. Y ) ) v ) < x <-> E. y e. F A. u e. y A. v e. y ( u D v ) < x ) )
19 18 ralbidv 
 |-  ( ( D e. ( *Met ` X ) /\ F e. ( CauFil ` ( D |` ( Y X. Y ) ) ) ) -> ( A. x e. RR+ E. y e. F A. u e. y A. v e. y ( u ( D |` ( Y X. Y ) ) v ) < x <-> A. x e. RR+ E. y e. F A. u e. y A. v e. y ( u D v ) < x ) )
20 4 19 mpbid 
 |-  ( ( D e. ( *Met ` X ) /\ F e. ( CauFil ` ( D |` ( Y X. Y ) ) ) ) -> A. x e. RR+ E. y e. F A. u e. y A. v e. y ( u D v ) < x )
21 filfbas 
 |-  ( F e. ( Fil ` ( X i^i Y ) ) -> F e. ( fBas ` ( X i^i Y ) ) )
22 6 21 syl 
 |-  ( ( D e. ( *Met ` X ) /\ F e. ( CauFil ` ( D |` ( Y X. Y ) ) ) ) -> F e. ( fBas ` ( X i^i Y ) ) )
23 filsspw 
 |-  ( F e. ( Fil ` ( X i^i Y ) ) -> F C_ ~P ( X i^i Y ) )
24 6 23 syl 
 |-  ( ( D e. ( *Met ` X ) /\ F e. ( CauFil ` ( D |` ( Y X. Y ) ) ) ) -> F C_ ~P ( X i^i Y ) )
25 inss1 
 |-  ( X i^i Y ) C_ X
26 25 sspwi 
 |-  ~P ( X i^i Y ) C_ ~P X
27 24 26 sstrdi 
 |-  ( ( D e. ( *Met ` X ) /\ F e. ( CauFil ` ( D |` ( Y X. Y ) ) ) ) -> F C_ ~P X )
28 elfvdm 
 |-  ( D e. ( *Met ` X ) -> X e. dom *Met )
29 28 adantr 
 |-  ( ( D e. ( *Met ` X ) /\ F e. ( CauFil ` ( D |` ( Y X. Y ) ) ) ) -> X e. dom *Met )
30 fbasweak 
 |-  ( ( F e. ( fBas ` ( X i^i Y ) ) /\ F C_ ~P X /\ X e. dom *Met ) -> F e. ( fBas ` X ) )
31 22 27 29 30 syl3anc 
 |-  ( ( D e. ( *Met ` X ) /\ F e. ( CauFil ` ( D |` ( Y X. Y ) ) ) ) -> F e. ( fBas ` X ) )
32 fgcfil 
 |-  ( ( D e. ( *Met ` X ) /\ F e. ( fBas ` X ) ) -> ( ( X filGen F ) e. ( CauFil ` D ) <-> A. x e. RR+ E. y e. F A. u e. y A. v e. y ( u D v ) < x ) )
33 31 32 syldan 
 |-  ( ( D e. ( *Met ` X ) /\ F e. ( CauFil ` ( D |` ( Y X. Y ) ) ) ) -> ( ( X filGen F ) e. ( CauFil ` D ) <-> A. x e. RR+ E. y e. F A. u e. y A. v e. y ( u D v ) < x ) )
34 20 33 mpbird 
 |-  ( ( D e. ( *Met ` X ) /\ F e. ( CauFil ` ( D |` ( Y X. Y ) ) ) ) -> ( X filGen F ) e. ( CauFil ` D ) )