Theorem fiufl

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

	Ref	Expression
Assertion	fiufl	⊢ ( 𝑋 ∈ Fin → 𝑋 ∈ UFL )

Proof

Step	Hyp	Ref	Expression
1		pwfi	⊢ ( 𝑋 ∈ Fin ↔ 𝒫 𝑋 ∈ Fin )
2		pwfi	⊢ ( 𝒫 𝑋 ∈ Fin ↔ 𝒫 𝒫 𝑋 ∈ Fin )
3		finnum	⊢ ( 𝒫 𝒫 𝑋 ∈ Fin → 𝒫 𝒫 𝑋 ∈ dom card )
4		numufl	⊢ ( 𝒫 𝒫 𝑋 ∈ dom card → 𝑋 ∈ UFL )
5	3 4	syl	⊢ ( 𝒫 𝒫 𝑋 ∈ Fin → 𝑋 ∈ UFL )
6	2 5	sylbi	⊢ ( 𝒫 𝑋 ∈ Fin → 𝑋 ∈ UFL )
7	1 6	sylbi	⊢ ( 𝑋 ∈ Fin → 𝑋 ∈ UFL )