Theorem acufl

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

	Ref	Expression
Assertion	acufl	$$⊢\mathrm{CHOICE}\to \mathrm{UFL}=\mathrm{V}$$

Proof

Step	Hyp	Ref	Expression
1		vex	$$⊢x\in \mathrm{V}$$
2	1	pwex	$$⊢𝒫x\in \mathrm{V}$$
3	2	pwex	$$⊢𝒫𝒫x\in \mathrm{V}$$
4		dfac10	$$⊢\mathrm{CHOICE}\leftrightarrow \mathrm{dom}\mathrm{card}=\mathrm{V}$$
5	4	biimpi	$$⊢\mathrm{CHOICE}\to \mathrm{dom}\mathrm{card}=\mathrm{V}$$
6	3 5	eleqtrrid	$$⊢\mathrm{CHOICE}\to 𝒫𝒫x\in \mathrm{dom}\mathrm{card}$$
7		numufl	$$⊢𝒫𝒫x\in \mathrm{dom}\mathrm{card}\to x\in \mathrm{UFL}$$
8	6 7	syl	$$⊢\mathrm{CHOICE}\to x\in \mathrm{UFL}$$
9	1	a1i	$$⊢\mathrm{CHOICE}\to x\in \mathrm{V}$$
10	8 9	2thd	$$⊢\mathrm{CHOICE}\to \left(x\in \mathrm{UFL}\leftrightarrow x\in \mathrm{V}\right)$$
11	10	eqrdv	$$⊢\mathrm{CHOICE}\to \mathrm{UFL}=\mathrm{V}$$