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 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 )