Theorem cfilufbas

Description: A Cauchy filter base is a filter base. (Contributed by Thierry Arnoux, 19-Nov-2017)

	Ref	Expression
Assertion	cfilufbas	$$⊢\left(U\in \mathrm{UnifOn}\left(X\right)\wedge F\in \mathrm{CauFilU}\left(U\right)\right)\to F\in \mathrm{fBas}\left(X\right)$$

Proof

Step	Hyp	Ref	Expression
1		iscfilu	$$⊢U\in \mathrm{UnifOn}\left(X\right)\to \left(F\in \mathrm{CauFilU}\left(U\right)\leftrightarrow \left(F\in \mathrm{fBas}\left(X\right)\wedge \forall v\in U\exists a\in Fa\times a\subseteq v\right)\right)$$
2	1	simprbda	$$⊢\left(U\in \mathrm{UnifOn}\left(X\right)\wedge F\in \mathrm{CauFilU}\left(U\right)\right)\to F\in \mathrm{fBas}\left(X\right)$$