Metamath Proof Explorer


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