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 \mathrm{UFil}\left(X\right)\to F\in \mathrm{Fil}\left(X\right)$$

Proof

Step	Hyp	Ref	Expression
1		isufil	$$⊢F\in \mathrm{UFil}\left(X\right)\leftrightarrow \left(F\in \mathrm{Fil}\left(X\right)\wedge \forall x\in 𝒫X\left(x\in F\vee X\setminus x\in F\right)\right)$$
2	1	simplbi	$$⊢F\in \mathrm{UFil}\left(X\right)\to F\in \mathrm{Fil}\left(X\right)$$