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 e. ( fBas ` X ) /\ A e. F ) -> -. ( B \ A ) e. F )

Proof

Step	Hyp	Ref	Expression
1		0nelfb	|- ( F e. ( fBas ` X ) -> -. (/) e. F )
2	1	adantr	|- ( ( F e. ( fBas ` X ) /\ A e. F ) -> -. (/) e. F )
3		fbasssin	|- ( ( F e. ( fBas ` X ) /\ A e. F /\ ( B \ A ) e. F ) -> E. x e. F x C_ ( A i^i ( B \ A ) ) )
4		disjdif	|- ( A i^i ( B \ A ) ) = (/)
5	4	sseq2i	|- ( x C_ ( A i^i ( B \ A ) ) <-> x C_ (/) )
6		ss0	|- ( x C_ (/) -> x = (/) )
7	5 6	sylbi	|- ( x C_ ( A i^i ( B \ A ) ) -> x = (/) )
8		eleq1	|- ( x = (/) -> ( x e. F <-> (/) e. F ) )
9	8	biimpac	|- ( ( x e. F /\ x = (/) ) -> (/) e. F )
10	7 9	sylan2	|- ( ( x e. F /\ x C_ ( A i^i ( B \ A ) ) ) -> (/) e. F )
11	10	rexlimiva	|- ( E. x e. F x C_ ( A i^i ( B \ A ) ) -> (/) e. F )
12	3 11	syl	|- ( ( F e. ( fBas ` X ) /\ A e. F /\ ( B \ A ) e. F ) -> (/) e. F )
13	12	3expia	|- ( ( F e. ( fBas ` X ) /\ A e. F ) -> ( ( B \ A ) e. F -> (/) e. F ) )
14	2 13	mtod	|- ( ( F e. ( fBas ` X ) /\ A e. F ) -> -. ( B \ A ) e. F )