This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 e. ( Fil ` X ) -> F C_ ~P X )

Proof

Step Hyp Ref Expression
1 filfbas 
 |-  ( F e. ( Fil ` X ) -> F e. ( fBas ` X ) )
2 fbsspw 
 |-  ( F e. ( fBas ` X ) -> F C_ ~P X )
3 1 2 syl 
 |-  ( F e. ( Fil ` X ) -> F C_ ~P X )