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 ∈ UnifOn ⁡ X ∧ F ∈ CauFilU ⁡ U → F ∈ fBas ⁡ X

Proof

Step Hyp Ref Expression
1 iscfilu ⊢ U ∈ UnifOn ⁡ X → F ∈ CauFilU ⁡ U ↔ F ∈ fBas ⁡ X ∧ ∀ v ∈ U ∃ a ∈ F a × a ⊆ v
2 1 simprbda ⊢ U ∈ UnifOn ⁡ X ∧ F ∈ CauFilU ⁡ U → F ∈ fBas ⁡ X