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