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

Metamath Proof Explorer

Theorem ufilb

Description: The complement is in an ultrafilter iff the set is not. (Contributed by Mario Carneiro, 11-Dec-2013) (Revised by Mario Carneiro, 29-Jul-2015)

		Ref	Expression
	Assertion	ufilb	$⊢ (F \in UFil (X) \land S \subseteq X) \to (\neg S \in F \leftrightarrow X ∖ S \in F)$

Proof

Step	Hyp	Ref	Expression
1		ufilss	$⊢ (F \in UFil (X) \land S \subseteq X) \to (S \in F \lor X ∖ S \in F)$
2	1	ord	$⊢ (F \in UFil (X) \land S \subseteq X) \to (\neg S \in F \to X ∖ S \in F)$
3		ufilfil	$⊢ F \in UFil (X) \to F \in Fil (X)$
4		filfbas	$⊢ F \in Fil (X) \to F \in fBas (X)$
5		fbncp	$⊢ (F \in fBas (X) \land S \in F) \to \neg X ∖ S \in F$
6	5	ex	$⊢ F \in fBas (X) \to (S \in F \to \neg X ∖ S \in F)$
7	6	con2d	$⊢ F \in fBas (X) \to (X ∖ S \in F \to \neg S \in F)$
8	3 4 7	3syl	$⊢ F \in UFil (X) \to (X ∖ S \in F \to \neg S \in F)$
9	8	adantr	$⊢ (F \in UFil (X) \land S \subseteq X) \to (X ∖ S \in F \to \neg S \in F)$
10	2 9	impbid	$⊢ (F \in UFil (X) \land S \subseteq X) \to (\neg S \in F \leftrightarrow X ∖ S \in F)$