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	⊢ 𝑥 ∈ V
2	1	pwex	⊢ 𝒫 𝑥 ∈ V
3	2	pwex	⊢ 𝒫 𝒫 𝑥 ∈ V
4		dfac10	⊢ ( CHOICE ↔ dom card = V )
5	4	biimpi	⊢ ( CHOICE → dom card = V )
6	3 5	eleqtrrid	⊢ ( CHOICE → 𝒫 𝒫 𝑥 ∈ dom card )
7		numufl	⊢ ( 𝒫 𝒫 𝑥 ∈ dom card → 𝑥 ∈ UFL )
8	6 7	syl	⊢ ( CHOICE → 𝑥 ∈ UFL )
9	1	a1i	⊢ ( CHOICE → 𝑥 ∈ V )
10	8 9	2thd	⊢ ( CHOICE → ( 𝑥 ∈ UFL ↔ 𝑥 ∈ V ) )
11	10	eqrdv	⊢ ( CHOICE → UFL = V )