Metamath Proof Explorer

Theorem 0nelfb

Description: No filter base contains the empty set. (Contributed by Jeff Hankins, 1-Sep-2009) (Revised by Mario Carneiro, 28-Jul-2015)

Ref Expression
Assertion 0nelfb 
|- ( F e. ( fBas ` B ) -> -. (/) e. F )

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 simpr2 
 |-  ( ( F C_ ~P B /\ ( F =/= (/) /\ (/) e/ F /\ A. x e. F A. y e. F ( F i^i ~P ( x i^i y ) ) =/= (/) ) ) -> (/) e/ F )
6 4 5 syl 
 |-  ( F e. ( fBas ` B ) -> (/) e/ F )
7 df-nel 
 |-  ( (/) e/ F <-> -. (/) e. F )
8 6 7 sylib 
 |-  ( F e. ( fBas ` B ) -> -. (/) e. F )