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	$$⊢\left(F\in \mathrm{fBas}\left(X\right)\wedge A\in F\right)\to \neg B\setminus A\in F$$

Proof

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