Metamath Proof Explorer


Theorem cfilufbas

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 ) )

Proof

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 ) )