acufl

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

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

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

Metamath Proof Explorer