This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ) )