This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.
Metamath Proof Explorer
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 ‘ 𝑋 ) ) |