Metamath Proof Explorer

Theorem numufl

Description: Consequence of filssufilg : a set whose double powerset is well-orderable satisfies the ultrafilter lemma. (Contributed by Mario Carneiro, 26-Aug-2015)

		Ref	Expression
	Assertion	numufl	$⊢ 𝒫 𝒫 X \in dom card \to X \in UFL$

Proof

Step	Hyp	Ref	Expression
1		filssufilg	$⊢ (f \in Fil (X) \land 𝒫 𝒫 X \in dom card) \to \exists g \in UFil (X) f \subseteq g$
2	1	ancoms	$⊢ (𝒫 𝒫 X \in dom card \land f \in Fil (X)) \to \exists g \in UFil (X) f \subseteq g$
3	2	ralrimiva	$⊢ 𝒫 𝒫 X \in dom card \to \forall f \in Fil (X) \exists g \in UFil (X) f \subseteq g$
4		pwexr	$⊢ 𝒫 𝒫 X \in dom card \to 𝒫 X \in V$
5		pwexb	$⊢ X \in V \leftrightarrow 𝒫 X \in V$
6	4 5	sylibr	$⊢ 𝒫 𝒫 X \in dom card \to X \in V$
7		isufl	$⊢ X \in V \to (X \in UFL \leftrightarrow \forall f \in Fil (X) \exists g \in UFil (X) f \subseteq g)$
8	6 7	syl	$⊢ 𝒫 𝒫 X \in dom card \to (X \in UFL \leftrightarrow \forall f \in Fil (X) \exists g \in UFil (X) f \subseteq g)$
9	3 8	mpbird	$⊢ 𝒫 𝒫 X \in dom card \to X \in UFL$