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

Metamath Proof Explorer

Theorem ufilfil

Description: An ultrafilter is a filter. (Contributed by Jeff Hankins, 1-Dec-2009) (Revised by Mario Carneiro, 29-Jul-2015)

		Ref	Expression
	Assertion	ufilfil	$⊢ F \in UFil (X) \to F \in Fil (X)$

Step	Hyp	Ref	Expression
1		isufil	$⊢ F \in UFil (X) \leftrightarrow (F \in Fil (X) \land \forall x \in 𝒫 X (x \in F \lor X ∖ x \in F))$
2	1	simplbi	$⊢ F \in UFil (X) \to F \in Fil (X)$