Metamath Proof Explorer

Theorem ufli

Description: Property of a set that satisfies the ultrafilter lemma. (Contributed by Mario Carneiro, 26-Aug-2015)

Ref Expression
Assertion ufli 
|- ( ( X e. UFL /\ F e. ( Fil ` X ) ) -> E. f e. ( UFil ` X ) F C_ f )

Proof

Step Hyp Ref Expression
1 isufl 
 |-  ( X e. UFL -> ( X e. UFL <-> A. g e. ( Fil ` X ) E. f e. ( UFil ` X ) g C_ f ) )
2 1 ibi 
 |-  ( X e. UFL -> A. g e. ( Fil ` X ) E. f e. ( UFil ` X ) g C_ f )
3 sseq1 
 |-  ( g = F -> ( g C_ f <-> F C_ f ) )
4 3 rexbidv 
 |-  ( g = F -> ( E. f e. ( UFil ` X ) g C_ f <-> E. f e. ( UFil ` X ) F C_ f ) )
5 4 rspccva 
 |-  ( ( A. g e. ( Fil ` X ) E. f e. ( UFil ` X ) g C_ f /\ F e. ( Fil ` X ) ) -> E. f e. ( UFil ` X ) F C_ f )
6 2 5 sylan 
 |-  ( ( X e. UFL /\ F e. ( Fil ` X ) ) -> E. f e. ( UFil ` X ) F C_ f )