Metamath Proof Explorer


Theorem isufl

Description: Define the (strong) ultrafilter lemma, parameterized over base sets. A set X satisfies the ultrafilter lemma if every filter on X is a subset of some ultrafilter. (Contributed by Mario Carneiro, 26-Aug-2015)

Ref Expression
Assertion isufl
|- ( X e. V -> ( X e. UFL <-> A. f e. ( Fil ` X ) E. g e. ( UFil ` X ) f C_ g ) )

Proof

Step Hyp Ref Expression
1 fveq2
 |-  ( x = X -> ( Fil ` x ) = ( Fil ` X ) )
2 fveq2
 |-  ( x = X -> ( UFil ` x ) = ( UFil ` X ) )
3 2 rexeqdv
 |-  ( x = X -> ( E. g e. ( UFil ` x ) f C_ g <-> E. g e. ( UFil ` X ) f C_ g ) )
4 1 3 raleqbidv
 |-  ( x = X -> ( A. f e. ( Fil ` x ) E. g e. ( UFil ` x ) f C_ g <-> A. f e. ( Fil ` X ) E. g e. ( UFil ` X ) f C_ g ) )
5 df-ufl
 |-  UFL = { x | A. f e. ( Fil ` x ) E. g e. ( UFil ` x ) f C_ g }
6 4 5 elab2g
 |-  ( X e. V -> ( X e. UFL <-> A. f e. ( Fil ` X ) E. g e. ( UFil ` X ) f C_ g ) )