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