This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem fiufl

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

		Ref	Expression
	Assertion	fiufl	$⊢ X \in Fin \to X \in UFL$

Step	Hyp	Ref	Expression
1		pwfi	$⊢ X \in Fin \leftrightarrow 𝒫 X \in Fin$
2		pwfi	$⊢ 𝒫 X \in Fin \leftrightarrow 𝒫 𝒫 X \in Fin$
3		finnum	$⊢ 𝒫 𝒫 X \in Fin \to 𝒫 𝒫 X \in dom card$
4		numufl	$⊢ 𝒫 𝒫 X \in dom card \to X \in UFL$
5	3 4	syl	$⊢ 𝒫 𝒫 X \in Fin \to X \in UFL$
6	2 5	sylbi	$⊢ 𝒫 X \in Fin \to X \in UFL$
7	1 6	sylbi	$⊢ X \in Fin \to X \in UFL$