Metamath Proof Explorer


Theorem fiufl

Description: A finite set satisfies the ultrafilter lemma. (Contributed by Mario Carneiro, 26-Aug-2015)

Ref Expression
Assertion fiufl XFinXUFL

Proof

Step Hyp Ref Expression
1 pwfi XFin𝒫XFin
2 pwfi 𝒫XFin𝒫𝒫XFin
3 finnum 𝒫𝒫XFin𝒫𝒫Xdomcard
4 numufl 𝒫𝒫XdomcardXUFL
5 3 4 syl 𝒫𝒫XFinXUFL
6 2 5 sylbi 𝒫XFinXUFL
7 1 6 sylbi XFinXUFL