Theorem fbsspw

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

	Ref	Expression
Assertion	fbsspw	|- ( F e. ( fBas ` B ) -> F C_ ~P B )

Proof

Step	Hyp	Ref	Expression
1		elfvdm	|- ( F e. ( fBas ` B ) -> B e. dom fBas )
2		isfbas	|- ( B e. dom fBas -> ( F e. ( fBas ` B ) <-> ( F C_ ~P B /\ ( F =/= (/) /\ (/) e/ F /\ A. x e. F A. y e. F ( F i^i ~P ( x i^i y ) ) =/= (/) ) ) ) )
3	1 2	syl	|- ( F e. ( fBas ` B ) -> ( F e. ( fBas ` B ) <-> ( F C_ ~P B /\ ( F =/= (/) /\ (/) e/ F /\ A. x e. F A. y e. F ( F i^i ~P ( x i^i y ) ) =/= (/) ) ) ) )
4	3	ibi	|- ( F e. ( fBas ` B ) -> ( F C_ ~P B /\ ( F =/= (/) /\ (/) e/ F /\ A. x e. F A. y e. F ( F i^i ~P ( x i^i y ) ) =/= (/) ) ) )
5	4	simpld	|- ( F e. ( fBas ` B ) -> F C_ ~P B )