Theorem acufl

Description: The axiom of choice implies the ultrafilter lemma. (Contributed by Mario Carneiro, 26-Aug-2015)

	Ref	Expression
Assertion	acufl	|- ( CHOICE -> UFL = _V )

Proof

Step	Hyp	Ref	Expression
1		vex	|- x e. _V
2	1	pwex	|- ~P x e. _V
3	2	pwex	|- ~P ~P x e. _V
4		dfac10	|- ( CHOICE <-> dom card = _V )
5	4	biimpi	|- ( CHOICE -> dom card = _V )
6	3 5	eleqtrrid	|- ( CHOICE -> ~P ~P x e. dom card )
7		numufl	|- ( ~P ~P x e. dom card -> x e. UFL )
8	6 7	syl	|- ( CHOICE -> x e. UFL )
9	1	a1i	|- ( CHOICE -> x e. _V )
10	8 9	2thd	|- ( CHOICE -> ( x e. UFL <-> x e. _V ) )
11	10	eqrdv	|- ( CHOICE -> UFL = _V )