Metamath Proof Explorer


Theorem cfilucfil2

Description: Given a metric D and a uniform structure generated by that metric, Cauchy filter bases on that uniform structure are exactly the filter bases which contain balls of any pre-chosen size. See iscfil . (Contributed by Thierry Arnoux, 1-Dec-2017) (Revised by Thierry Arnoux, 11-Feb-2018)

Ref Expression
Assertion cfilucfil2 X D PsMet X C CauFilU metUnif D C fBas X x + y C D y × y 0 x

Proof

Step Hyp Ref Expression
1 metuval D PsMet X metUnif D = X × X filGen ran a + D -1 0 a
2 1 adantl X D PsMet X metUnif D = X × X filGen ran a + D -1 0 a
3 2 fveq2d X D PsMet X CauFilU metUnif D = CauFilU X × X filGen ran a + D -1 0 a
4 3 eleq2d X D PsMet X C CauFilU metUnif D C CauFilU X × X filGen ran a + D -1 0 a
5 oveq2 a = b 0 a = 0 b
6 5 imaeq2d a = b D -1 0 a = D -1 0 b
7 6 cbvmptv a + D -1 0 a = b + D -1 0 b
8 7 rneqi ran a + D -1 0 a = ran b + D -1 0 b
9 8 cfilucfil X D PsMet X C CauFilU X × X filGen ran a + D -1 0 a C fBas X x + y C D y × y 0 x
10 4 9 bitrd X D PsMet X C CauFilU metUnif D C fBas X x + y C D y × y 0 x