Theorem ufilss

Description: For any subset of the base set of an ultrafilter, either the set is in the ultrafilter or the complement is. (Contributed by Jeff Hankins, 1-Dec-2009) (Revised by Mario Carneiro, 29-Jul-2015)

	Ref	Expression
Assertion	ufilss	$$⊢\left(F\in \mathrm{UFil}\left(X\right)\wedge S\subseteq X\right)\to \left(S\in F\vee X\setminus S\in F\right)$$

Proof

Step	Hyp	Ref	Expression
1		elfvdm	$$⊢F\in \mathrm{UFil}\left(X\right)\to X\in \mathrm{dom}\mathrm{UFil}$$
2		elpw2g	$$⊢X\in \mathrm{dom}\mathrm{UFil}\to \left(S\in 𝒫X\leftrightarrow S\subseteq X\right)$$
3	1 2	syl	$$⊢F\in \mathrm{UFil}\left(X\right)\to \left(S\in 𝒫X\leftrightarrow S\subseteq X\right)$$
4		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)$$
5		eleq1	$$⊢x=S\to \left(x\in F\leftrightarrow S\in F\right)$$
6		difeq2	$$⊢x=S\to X\setminus x=X\setminus S$$
7	6	eleq1d	$$⊢x=S\to \left(X\setminus x\in F\leftrightarrow X\setminus S\in F\right)$$
8	5 7	orbi12d	$$⊢x=S\to \left(\left(x\in F\vee X\setminus x\in F\right)\leftrightarrow \left(S\in F\vee X\setminus S\in F\right)\right)$$
9	8	rspccv	$$⊢\forall x\in 𝒫X\left(x\in F\vee X\setminus x\in F\right)\to \left(S\in 𝒫X\to \left(S\in F\vee X\setminus S\in F\right)\right)$$
10	4 9	simplbiim	$$⊢F\in \mathrm{UFil}\left(X\right)\to \left(S\in 𝒫X\to \left(S\in F\vee X\setminus S\in F\right)\right)$$
11	3 10	sylbird	$$⊢F\in \mathrm{UFil}\left(X\right)\to \left(S\subseteq X\to \left(S\in F\vee X\setminus S\in F\right)\right)$$
12	11	imp	$$⊢\left(F\in \mathrm{UFil}\left(X\right)\wedge S\subseteq X\right)\to \left(S\in F\vee X\setminus S\in F\right)$$