Metamath Proof Explorer

Theorem filfbas

Description: A filter is a filter base. (Contributed by Jeff Hankins, 2-Sep-2009) (Revised by Mario Carneiro, 28-Jul-2015)

Ref Expression
Assertion filfbas 
|- ( F e. ( Fil ` X ) -> F e. ( fBas ` X ) )

Proof

Step Hyp Ref Expression
1 isfil 
 |-  ( F e. ( Fil ` X ) <-> ( F e. ( fBas ` X ) /\ A. x e. ~P X ( ( F i^i ~P x ) =/= (/) -> x e. F ) ) )
2 1 simplbi 
 |-  ( F e. ( Fil ` X ) -> F e. ( fBas ` X ) )