Description: A Cauchy filter base is a filter base. (Contributed by Thierry Arnoux, 19-Nov-2017)
Ref | Expression | ||
---|---|---|---|
Assertion | cfilufbas | |- ( ( U e. ( UnifOn ` X ) /\ F e. ( CauFilU ` U ) ) -> F e. ( fBas ` X ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | iscfilu | |- ( U e. ( UnifOn ` X ) -> ( F e. ( CauFilU ` U ) <-> ( F e. ( fBas ` X ) /\ A. v e. U E. a e. F ( a X. a ) C_ v ) ) ) |
|
2 | 1 | simprbda | |- ( ( U e. ( UnifOn ` X ) /\ F e. ( CauFilU ` U ) ) -> F e. ( fBas ` X ) ) |