Metamath Proof Explorer

Theorem cfilres

Description: Cauchy filter on a metric subspace. (Contributed by Mario Carneiro, 15-Oct-2015)

Ref Expression
Assertion cfilres 
|- ( ( D e. ( *Met ` X ) /\ F e. ( Fil ` X ) /\ Y e. F ) -> ( F e. ( CauFil ` D ) <-> ( F |`t Y ) e. ( CauFil ` ( D |` ( Y X. Y ) ) ) ) )

Proof

Step Hyp Ref Expression
1 simp2 
 |-  ( ( D e. ( *Met ` X ) /\ F e. ( Fil ` X ) /\ Y e. F ) -> F e. ( Fil ` X ) )
2 filfbas 
 |-  ( F e. ( Fil ` X ) -> F e. ( fBas ` X ) )
3 1 2 syl 
 |-  ( ( D e. ( *Met ` X ) /\ F e. ( Fil ` X ) /\ Y e. F ) -> F e. ( fBas ` X ) )
4 simp3 
 |-  ( ( D e. ( *Met ` X ) /\ F e. ( Fil ` X ) /\ Y e. F ) -> Y e. F )
5 fbncp 
 |-  ( ( F e. ( fBas ` X ) /\ Y e. F ) -> -. ( X \ Y ) e. F )
6 3 4 5 syl2anc 
 |-  ( ( D e. ( *Met ` X ) /\ F e. ( Fil ` X ) /\ Y e. F ) -> -. ( X \ Y ) e. F )
7 filelss 
 |-  ( ( F e. ( Fil ` X ) /\ Y e. F ) -> Y C_ X )
8 7 3adant1 
 |-  ( ( D e. ( *Met ` X ) /\ F e. ( Fil ` X ) /\ Y e. F ) -> Y C_ X )
9 trfil3 
 |-  ( ( F e. ( Fil ` X ) /\ Y C_ X ) -> ( ( F |`t Y ) e. ( Fil ` Y ) <-> -. ( X \ Y ) e. F ) )
10 1 8 9 syl2anc 
 |-  ( ( D e. ( *Met ` X ) /\ F e. ( Fil ` X ) /\ Y e. F ) -> ( ( F |`t Y ) e. ( Fil ` Y ) <-> -. ( X \ Y ) e. F ) )
11 6 10 mpbird 
 |-  ( ( D e. ( *Met ` X ) /\ F e. ( Fil ` X ) /\ Y e. F ) -> ( F |`t Y ) e. ( Fil ` Y ) )
12 11 adantr 
 |-  ( ( ( D e. ( *Met ` X ) /\ F e. ( Fil ` X ) /\ Y e. F ) /\ F e. ( CauFil ` D ) ) -> ( F |`t Y ) e. ( Fil ` Y ) )
13 cfili 
 |-  ( ( F e. ( CauFil ` D ) /\ x e. RR+ ) -> E. s e. F A. u e. s A. v e. s ( u D v ) < x )
14 13 adantll 
 |-  ( ( ( ( D e. ( *Met ` X ) /\ F e. ( Fil ` X ) /\ Y e. F ) /\ F e. ( CauFil ` D ) ) /\ x e. RR+ ) -> E. s e. F A. u e. s A. v e. s ( u D v ) < x )
15 simpll2 
 |-  ( ( ( ( D e. ( *Met ` X ) /\ F e. ( Fil ` X ) /\ Y e. F ) /\ F e. ( CauFil ` D ) ) /\ x e. RR+ ) -> F e. ( Fil ` X ) )
16 simpll3 
 |-  ( ( ( ( D e. ( *Met ` X ) /\ F e. ( Fil ` X ) /\ Y e. F ) /\ F e. ( CauFil ` D ) ) /\ x e. RR+ ) -> Y e. F )
17 15 16 jca 
 |-  ( ( ( ( D e. ( *Met ` X ) /\ F e. ( Fil ` X ) /\ Y e. F ) /\ F e. ( CauFil ` D ) ) /\ x e. RR+ ) -> ( F e. ( Fil ` X ) /\ Y e. F ) )
18 elrestr 
 |-  ( ( F e. ( Fil ` X ) /\ Y e. F /\ s e. F ) -> ( s i^i Y ) e. ( F |`t Y ) )
19 18 3expa 
 |-  ( ( ( F e. ( Fil ` X ) /\ Y e. F ) /\ s e. F ) -> ( s i^i Y ) e. ( F |`t Y ) )
20 17 19 sylan 
 |-  ( ( ( ( ( D e. ( *Met ` X ) /\ F e. ( Fil ` X ) /\ Y e. F ) /\ F e. ( CauFil ` D ) ) /\ x e. RR+ ) /\ s e. F ) -> ( s i^i Y ) e. ( F |`t Y ) )
21 inss1 
 |-  ( s i^i Y ) C_ s
22 ss2ralv 
 |-  ( ( s i^i Y ) C_ s -> ( A. u e. s A. v e. s ( u D v ) < x -> A. u e. ( s i^i Y ) A. v e. ( s i^i Y ) ( u D v ) < x ) )
23 21 22 ax-mp 
 |-  ( A. u e. s A. v e. s ( u D v ) < x -> A. u e. ( s i^i Y ) A. v e. ( s i^i Y ) ( u D v ) < x )
24 elinel2 
 |-  ( u e. ( s i^i Y ) -> u e. Y )
25 elinel2 
 |-  ( v e. ( s i^i Y ) -> v e. Y )
26 ovres 
 |-  ( ( u e. Y /\ v e. Y ) -> ( u ( D |` ( Y X. Y ) ) v ) = ( u D v ) )
27 26 breq1d 
 |-  ( ( u e. Y /\ v e. Y ) -> ( ( u ( D |` ( Y X. Y ) ) v ) < x <-> ( u D v ) < x ) )
28 24 25 27 syl2an 
 |-  ( ( u e. ( s i^i Y ) /\ v e. ( s i^i Y ) ) -> ( ( u ( D |` ( Y X. Y ) ) v ) < x <-> ( u D v ) < x ) )
29 28 ralbidva 
 |-  ( u e. ( s i^i Y ) -> ( A. v e. ( s i^i Y ) ( u ( D |` ( Y X. Y ) ) v ) < x <-> A. v e. ( s i^i Y ) ( u D v ) < x ) )
30 29 ralbiia 
 |-  ( A. u e. ( s i^i Y ) A. v e. ( s i^i Y ) ( u ( D |` ( Y X. Y ) ) v ) < x <-> A. u e. ( s i^i Y ) A. v e. ( s i^i Y ) ( u D v ) < x )
31 23 30 sylibr 
 |-  ( A. u e. s A. v e. s ( u D v ) < x -> A. u e. ( s i^i Y ) A. v e. ( s i^i Y ) ( u ( D |` ( Y X. Y ) ) v ) < x )
32 raleq 
 |-  ( y = ( s i^i Y ) -> ( A. v e. y ( u ( D |` ( Y X. Y ) ) v ) < x <-> A. v e. ( s i^i Y ) ( u ( D |` ( Y X. Y ) ) v ) < x ) )
33 32 raleqbi1dv 
 |-  ( y = ( s i^i Y ) -> ( A. u e. y A. v e. y ( u ( D |` ( Y X. Y ) ) v ) < x <-> A. u e. ( s i^i Y ) A. v e. ( s i^i Y ) ( u ( D |` ( Y X. Y ) ) v ) < x ) )
34 33 rspcev 
 |-  ( ( ( s i^i Y ) e. ( F |`t Y ) /\ A. u e. ( s i^i Y ) A. v e. ( s i^i Y ) ( u ( D |` ( Y X. Y ) ) v ) < x ) -> E. y e. ( F |`t Y ) A. u e. y A. v e. y ( u ( D |` ( Y X. Y ) ) v ) < x )
35 34 ex 
 |-  ( ( s i^i Y ) e. ( F |`t Y ) -> ( A. u e. ( s i^i Y ) A. v e. ( s i^i Y ) ( u ( D |` ( Y X. Y ) ) v ) < x -> E. y e. ( F |`t Y ) A. u e. y A. v e. y ( u ( D |` ( Y X. Y ) ) v ) < x ) )
36 20 31 35 syl2im 
 |-  ( ( ( ( ( D e. ( *Met ` X ) /\ F e. ( Fil ` X ) /\ Y e. F ) /\ F e. ( CauFil ` D ) ) /\ x e. RR+ ) /\ s e. F ) -> ( A. u e. s A. v e. s ( u D v ) < x -> E. y e. ( F |`t Y ) A. u e. y A. v e. y ( u ( D |` ( Y X. Y ) ) v ) < x ) )
37 36 rexlimdva 
 |-  ( ( ( ( D e. ( *Met ` X ) /\ F e. ( Fil ` X ) /\ Y e. F ) /\ F e. ( CauFil ` D ) ) /\ x e. RR+ ) -> ( E. s e. F A. u e. s A. v e. s ( u D v ) < x -> E. y e. ( F |`t Y ) A. u e. y A. v e. y ( u ( D |` ( Y X. Y ) ) v ) < x ) )
38 14 37 mpd 
 |-  ( ( ( ( D e. ( *Met ` X ) /\ F e. ( Fil ` X ) /\ Y e. F ) /\ F e. ( CauFil ` D ) ) /\ x e. RR+ ) -> E. y e. ( F |`t Y ) A. u e. y A. v e. y ( u ( D |` ( Y X. Y ) ) v ) < x )
39 38 ralrimiva 
 |-  ( ( ( D e. ( *Met ` X ) /\ F e. ( Fil ` X ) /\ Y e. F ) /\ F e. ( CauFil ` D ) ) -> A. x e. RR+ E. y e. ( F |`t Y ) A. u e. y A. v e. y ( u ( D |` ( Y X. Y ) ) v ) < x )
40 simp1 
 |-  ( ( D e. ( *Met ` X ) /\ F e. ( Fil ` X ) /\ Y e. F ) -> D e. ( *Met ` X ) )
41 xmetres2 
 |-  ( ( D e. ( *Met ` X ) /\ Y C_ X ) -> ( D |` ( Y X. Y ) ) e. ( *Met ` Y ) )
42 40 8 41 syl2anc 
 |-  ( ( D e. ( *Met ` X ) /\ F e. ( Fil ` X ) /\ Y e. F ) -> ( D |` ( Y X. Y ) ) e. ( *Met ` Y ) )
43 42 adantr 
 |-  ( ( ( D e. ( *Met ` X ) /\ F e. ( Fil ` X ) /\ Y e. F ) /\ F e. ( CauFil ` D ) ) -> ( D |` ( Y X. Y ) ) e. ( *Met ` Y ) )
44 iscfil2 
 |-  ( ( D |` ( Y X. Y ) ) e. ( *Met ` Y ) -> ( ( F |`t Y ) e. ( CauFil ` ( D |` ( Y X. Y ) ) ) <-> ( ( F |`t Y ) e. ( Fil ` Y ) /\ A. x e. RR+ E. y e. ( F |`t Y ) A. u e. y A. v e. y ( u ( D |` ( Y X. Y ) ) v ) < x ) ) )
45 43 44 syl 
 |-  ( ( ( D e. ( *Met ` X ) /\ F e. ( Fil ` X ) /\ Y e. F ) /\ F e. ( CauFil ` D ) ) -> ( ( F |`t Y ) e. ( CauFil ` ( D |` ( Y X. Y ) ) ) <-> ( ( F |`t Y ) e. ( Fil ` Y ) /\ A. x e. RR+ E. y e. ( F |`t Y ) A. u e. y A. v e. y ( u ( D |` ( Y X. Y ) ) v ) < x ) ) )
46 12 39 45 mpbir2and 
 |-  ( ( ( D e. ( *Met ` X ) /\ F e. ( Fil ` X ) /\ Y e. F ) /\ F e. ( CauFil ` D ) ) -> ( F |`t Y ) e. ( CauFil ` ( D |` ( Y X. Y ) ) ) )
47 46 ex 
 |-  ( ( D e. ( *Met ` X ) /\ F e. ( Fil ` X ) /\ Y e. F ) -> ( F e. ( CauFil ` D ) -> ( F |`t Y ) e. ( CauFil ` ( D |` ( Y X. Y ) ) ) ) )
48 cfilresi 
 |-  ( ( D e. ( *Met ` X ) /\ ( F |`t Y ) e. ( CauFil ` ( D |` ( Y X. Y ) ) ) ) -> ( X filGen ( F |`t Y ) ) e. ( CauFil ` D ) )
49 48 ex 
 |-  ( D e. ( *Met ` X ) -> ( ( F |`t Y ) e. ( CauFil ` ( D |` ( Y X. Y ) ) ) -> ( X filGen ( F |`t Y ) ) e. ( CauFil ` D ) ) )
50 49 3ad2ant1 
 |-  ( ( D e. ( *Met ` X ) /\ F e. ( Fil ` X ) /\ Y e. F ) -> ( ( F |`t Y ) e. ( CauFil ` ( D |` ( Y X. Y ) ) ) -> ( X filGen ( F |`t Y ) ) e. ( CauFil ` D ) ) )
51 fgtr 
 |-  ( ( F e. ( Fil ` X ) /\ Y e. F ) -> ( X filGen ( F |`t Y ) ) = F )
52 51 3adant1 
 |-  ( ( D e. ( *Met ` X ) /\ F e. ( Fil ` X ) /\ Y e. F ) -> ( X filGen ( F |`t Y ) ) = F )
53 52 eleq1d 
 |-  ( ( D e. ( *Met ` X ) /\ F e. ( Fil ` X ) /\ Y e. F ) -> ( ( X filGen ( F |`t Y ) ) e. ( CauFil ` D ) <-> F e. ( CauFil ` D ) ) )
54 50 53 sylibd 
 |-  ( ( D e. ( *Met ` X ) /\ F e. ( Fil ` X ) /\ Y e. F ) -> ( ( F |`t Y ) e. ( CauFil ` ( D |` ( Y X. Y ) ) ) -> F e. ( CauFil ` D ) ) )
55 47 54 impbid 
 |-  ( ( D e. ( *Met ` X ) /\ F e. ( Fil ` X ) /\ Y e. F ) -> ( F e. ( CauFil ` D ) <-> ( F |`t Y ) e. ( CauFil ` ( D |` ( Y X. Y ) ) ) ) )