Theorem numufl

Description: Consequence of filssufilg : a set whose double powerset is well-orderable satisfies the ultrafilter lemma. (Contributed by Mario Carneiro, 26-Aug-2015)

	Ref	Expression
Assertion	numufl	|- ( ~P ~P X e. dom card -> X e. UFL )

Proof

Step	Hyp	Ref	Expression
1		filssufilg	|- ( ( f e. ( Fil ` X ) /\ ~P ~P X e. dom card ) -> E. g e. ( UFil ` X ) f C_ g )
2	1	ancoms	|- ( ( ~P ~P X e. dom card /\ f e. ( Fil ` X ) ) -> E. g e. ( UFil ` X ) f C_ g )
3	2	ralrimiva	|- ( ~P ~P X e. dom card -> A. f e. ( Fil ` X ) E. g e. ( UFil ` X ) f C_ g )
4		pwexr	|- ( ~P ~P X e. dom card -> ~P X e. _V )
5		pwexb	|- ( X e. _V <-> ~P X e. _V )
6	4 5	sylibr	|- ( ~P ~P X e. dom card -> X e. _V )
7		isufl	|- ( X e. _V -> ( X e. UFL <-> A. f e. ( Fil ` X ) E. g e. ( UFil ` X ) f C_ g ) )
8	6 7	syl	|- ( ~P ~P X e. dom card -> ( X e. UFL <-> A. f e. ( Fil ` X ) E. g e. ( UFil ` X ) f C_ g ) )
9	3 8	mpbird	|- ( ~P ~P X e. dom card -> X e. UFL )