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 ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝐹 ∈ ( CauFilu𝑈 ) ) → 𝐹 ∈ ( fBas ‘ 𝑋 ) )

Proof

Step Hyp Ref Expression
1 iscfilu ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) → ( 𝐹 ∈ ( CauFilu𝑈 ) ↔ ( 𝐹 ∈ ( fBas ‘ 𝑋 ) ∧ ∀ 𝑣𝑈𝑎𝐹 ( 𝑎 × 𝑎 ) ⊆ 𝑣 ) ) )
2 1 simprbda ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝐹 ∈ ( CauFilu𝑈 ) ) → 𝐹 ∈ ( fBas ‘ 𝑋 ) )