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

Metamath Proof Explorer

Theorem fbncp

Description: A filter base does not contain complements of its elements. (Contributed by Mario Carneiro, 26-Nov-2013) (Revised by Stefan O'Rear, 28-Jul-2015)

		Ref	Expression
	Assertion	fbncp	$⊢ (F \in fBas (X) \land A \in F) \to \neg B ∖ A \in F$

Proof

Step	Hyp	Ref	Expression
1		0nelfb	$⊢ F \in fBas (X) \to \neg \emptyset \in F$
2	1	adantr	$⊢ (F \in fBas (X) \land A \in F) \to \neg \emptyset \in F$
3		fbasssin	$⊢ (F \in fBas (X) \land A \in F \land B ∖ A \in F) \to \exists x \in F x \subseteq A \cap (B ∖ A)$
4		disjdif	$⊢ A \cap (B ∖ A) = \emptyset$
5	4	sseq2i	$⊢ x \subseteq A \cap (B ∖ A) \leftrightarrow x \subseteq \emptyset$
6		ss0	$⊢ x \subseteq \emptyset \to x = \emptyset$
7	5 6	sylbi	$⊢ x \subseteq A \cap (B ∖ A) \to x = \emptyset$
8		eleq1	$⊢ x = \emptyset \to (x \in F \leftrightarrow \emptyset \in F)$
9	8	biimpac	$⊢ (x \in F \land x = \emptyset) \to \emptyset \in F$
10	7 9	sylan2	$⊢ (x \in F \land x \subseteq A \cap (B ∖ A)) \to \emptyset \in F$
11	10	rexlimiva	$⊢ \exists x \in F x \subseteq A \cap (B ∖ A) \to \emptyset \in F$
12	3 11	syl	$⊢ (F \in fBas (X) \land A \in F \land B ∖ A \in F) \to \emptyset \in F$
13	12	3expia	$⊢ (F \in fBas (X) \land A \in F) \to (B ∖ A \in F \to \emptyset \in F)$
14	2 13	mtod	$⊢ (F \in fBas (X) \land A \in F) \to \neg B ∖ A \in F$