This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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