Theorem filsspw

Description: A filter is a subset of the power set of the base set. (Contributed by Stefan O'Rear, 28-Jul-2015)

	Ref	Expression
Assertion	filsspw	$$⊢F\in \mathrm{Fil}\left(X\right)\to F\subseteq 𝒫X$$

Proof

Step	Hyp	Ref	Expression
1		filfbas	$$⊢F\in \mathrm{Fil}\left(X\right)\to F\in \mathrm{fBas}\left(X\right)$$
2		fbsspw	$$⊢F\in \mathrm{fBas}\left(X\right)\to F\subseteq 𝒫X$$
3	1 2	syl	$$⊢F\in \mathrm{Fil}\left(X\right)\to F\subseteq 𝒫X$$