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

Metamath Proof Explorer

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	$⊢ (F \in UFil (X) \land S \subseteq X) \to (S \in F \lor X ∖ S \in F)$

Proof

Step	Hyp	Ref	Expression
1		elfvdm	$⊢ F \in UFil (X) \to X \in dom UFil$
2		elpw2g	$⊢ X \in dom UFil \to (S \in 𝒫 X \leftrightarrow S \subseteq X)$
3	1 2	syl	$⊢ F \in UFil (X) \to (S \in 𝒫 X \leftrightarrow S \subseteq X)$
4		isufil	$⊢ F \in UFil (X) \leftrightarrow (F \in Fil (X) \land \forall x \in 𝒫 X (x \in F \lor X ∖ x \in F))$
5		eleq1	$⊢ x = S \to (x \in F \leftrightarrow S \in F)$
6		difeq2	$⊢ x = S \to X ∖ x = X ∖ S$
7	6	eleq1d	$⊢ x = S \to (X ∖ x \in F \leftrightarrow X ∖ S \in F)$
8	5 7	orbi12d	$⊢ x = S \to ((x \in F \lor X ∖ x \in F) \leftrightarrow (S \in F \lor X ∖ S \in F))$
9	8	rspccv	$⊢ \forall x \in 𝒫 X (x \in F \lor X ∖ x \in F) \to (S \in 𝒫 X \to (S \in F \lor X ∖ S \in F))$
10	4 9	simplbiim	$⊢ F \in UFil (X) \to (S \in 𝒫 X \to (S \in F \lor X ∖ S \in F))$
11	3 10	sylbird	$⊢ F \in UFil (X) \to (S \subseteq X \to (S \in F \lor X ∖ S \in F))$
12	11	imp	$⊢ (F \in UFil (X) \land S \subseteq X) \to (S \in F \lor X ∖ S \in F)$