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

Metamath Proof Explorer

Theorem filssufil

Description: A filter is contained in some ultrafilter. (Requires the Axiom of Choice, via numth3 .) (Contributed by Jeff Hankins, 2-Dec-2009) (Revised by Stefan O'Rear, 29-Jul-2015)

		Ref	Expression
	Assertion	filssufil	$⊢ F \in Fil (X) \to \exists f \in UFil (X) F \subseteq f$

Proof

Step	Hyp	Ref	Expression
1		filtop	$⊢ F \in Fil (X) \to X \in F$
2		pwexg	$⊢ X \in F \to 𝒫 X \in V$
3		pwexg	$⊢ 𝒫 X \in V \to 𝒫 𝒫 X \in V$
4		numth3	$⊢ 𝒫 𝒫 X \in V \to 𝒫 𝒫 X \in dom card$
5	1 2 3 4	4syl	$⊢ F \in Fil (X) \to 𝒫 𝒫 X \in dom card$
6		filssufilg	$⊢ (F \in Fil (X) \land 𝒫 𝒫 X \in dom card) \to \exists f \in UFil (X) F \subseteq f$
7	5 6	mpdan	$⊢ F \in Fil (X) \to \exists f \in UFil (X) F \subseteq f$