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	⊢ ( 𝐹 ∈ ( Fil ‘ 𝑋 ) → 𝐹 ⊆ 𝒫 𝑋 )

Proof

Step	Hyp	Ref	Expression
1		filfbas	⊢ ( 𝐹 ∈ ( Fil ‘ 𝑋 ) → 𝐹 ∈ ( fBas ‘ 𝑋 ) )
2		fbsspw	⊢ ( 𝐹 ∈ ( fBas ‘ 𝑋 ) → 𝐹 ⊆ 𝒫 𝑋 )
3	1 2	syl	⊢ ( 𝐹 ∈ ( Fil ‘ 𝑋 ) → 𝐹 ⊆ 𝒫 𝑋 )