Metamath Proof Explorer

Theorem ufilfil

Description: An ultrafilter is a filter. (Contributed by Jeff Hankins, 1-Dec-2009) (Revised by Mario Carneiro, 29-Jul-2015)

Ref Expression
Assertion ufilfil 
|- ( F e. ( UFil ` X ) -> F e. ( Fil ` X ) )

Proof

Step Hyp Ref Expression
1 isufil 
 |-  ( F e. ( UFil ` X ) <-> ( F e. ( Fil ` X ) /\ A. x e. ~P X ( x e. F \/ ( X \ x ) e. F ) ) )
2 1 simplbi 
 |-  ( F e. ( UFil ` X ) -> F e. ( Fil ` X ) )