Theorem filfbas

Description: A filter is a filter base. (Contributed by Jeff Hankins, 2-Sep-2009) (Revised by Mario Carneiro, 28-Jul-2015)

	Ref	Expression
Assertion	filfbas	$$⊢F\in \mathrm{Fil}\left(X\right)\to F\in \mathrm{fBas}\left(X\right)$$

Proof

Step	Hyp	Ref	Expression
1		isfil	$$⊢F\in \mathrm{Fil}\left(X\right)\leftrightarrow \left(F\in \mathrm{fBas}\left(X\right)\wedge \forall x\in 𝒫X\left(F\cap 𝒫x\ne \varnothing \to x\in F\right)\right)$$
2	1	simplbi	$$⊢F\in \mathrm{Fil}\left(X\right)\to F\in \mathrm{fBas}\left(X\right)$$