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 ∞Met X F CauFil D Y × Y X filGen F CauFil D

Proof

Step Hyp Ref Expression
1 xmetres D ∞Met X D Y × Y ∞Met X Y
2 iscfil2 D Y × Y ∞Met X Y F CauFil D Y × Y F Fil X Y x + y F u y v y u D Y × Y v < x
3 2 simplbda D Y × Y ∞Met X Y F CauFil D Y × Y x + y F u y v y u D Y × Y v < x
4 1 3 sylan D ∞Met X F CauFil D Y × Y x + y F u y v y u D Y × Y v < x
5 cfilfil D Y × Y ∞Met X Y F CauFil D Y × Y F Fil X Y
6 1 5 sylan D ∞Met X F CauFil D Y × Y F Fil X Y
7 filelss F Fil X Y y F y X Y
8 6 7 sylan D ∞Met X F CauFil D Y × Y y F y X Y
9 inss2 X Y Y
10 8 9 sstrdi D ∞Met X F CauFil D Y × Y y F y Y
11 10 sselda D ∞Met X F CauFil D Y × Y y F u y u Y
12 10 sselda D ∞Met X F CauFil D Y × Y y F v y v Y
13 11 12 anim12dan D ∞Met X F CauFil D Y × Y y F u y v y u Y v Y
14 ovres u Y v Y u D Y × Y v = u D v
15 13 14 syl D ∞Met X F CauFil D Y × Y y F u y v y u D Y × Y v = u D v
16 15 breq1d D ∞Met X F CauFil D Y × Y y F u y v y u D Y × Y v < x u D v < x
17 16 2ralbidva D ∞Met X F CauFil D Y × Y y F u y v y u D Y × Y v < x u y v y u D v < x
18 17 rexbidva D ∞Met X F CauFil D Y × Y y F u y v y u D Y × Y v < x y F u y v y u D v < x
19 18 ralbidv D ∞Met X F CauFil D Y × Y x + y F u y v y u D Y × Y v < x x + y F u y v y u D v < x
20 4 19 mpbid D ∞Met X F CauFil D Y × Y x + y F u y v y u D v < x
21 filfbas F Fil X Y F fBas X Y
22 6 21 syl D ∞Met X F CauFil D Y × Y F fBas X Y
23 filsspw F Fil X Y F 𝒫 X Y
24 6 23 syl D ∞Met X F CauFil D Y × Y F 𝒫 X Y
25 inss1 X Y X
26 25 sspwi 𝒫 X Y 𝒫 X
27 24 26 sstrdi D ∞Met X F CauFil D Y × Y F 𝒫 X
28 elfvdm D ∞Met X X dom ∞Met
29 28 adantr D ∞Met X F CauFil D Y × Y X dom ∞Met
30 fbasweak F fBas X Y F 𝒫 X X dom ∞Met F fBas X
31 22 27 29 30 syl3anc D ∞Met X F CauFil D Y × Y F fBas X
32 fgcfil D ∞Met X F fBas X X filGen F CauFil D x + y F u y v y u D v < x
33 31 32 syldan D ∞Met X F CauFil D Y × Y X filGen F CauFil D x + y F u y v y u D v < x
34 20 33 mpbird D ∞Met X F CauFil D Y × Y X filGen F CauFil D