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	⊢ ( ( 𝐹 ∈ ( fBas ‘ 𝑋 ) ∧ 𝐴 ∈ 𝐹 ) → ¬ ( 𝐵 ∖ 𝐴 ) ∈ 𝐹 )

Proof

Step	Hyp	Ref	Expression
1		0nelfb	⊢ ( 𝐹 ∈ ( fBas ‘ 𝑋 ) → ¬ ∅ ∈ 𝐹 )
2	1	adantr	⊢ ( ( 𝐹 ∈ ( fBas ‘ 𝑋 ) ∧ 𝐴 ∈ 𝐹 ) → ¬ ∅ ∈ 𝐹 )
3		fbasssin	⊢ ( ( 𝐹 ∈ ( fBas ‘ 𝑋 ) ∧ 𝐴 ∈ 𝐹 ∧ ( 𝐵 ∖ 𝐴 ) ∈ 𝐹 ) → ∃ 𝑥 ∈ 𝐹 𝑥 ⊆ ( 𝐴 ∩ ( 𝐵 ∖ 𝐴 ) ) )
4		disjdif	⊢ ( 𝐴 ∩ ( 𝐵 ∖ 𝐴 ) ) = ∅
5	4	sseq2i	⊢ ( 𝑥 ⊆ ( 𝐴 ∩ ( 𝐵 ∖ 𝐴 ) ) ↔ 𝑥 ⊆ ∅ )
6		ss0	⊢ ( 𝑥 ⊆ ∅ → 𝑥 = ∅ )
7	5 6	sylbi	⊢ ( 𝑥 ⊆ ( 𝐴 ∩ ( 𝐵 ∖ 𝐴 ) ) → 𝑥 = ∅ )
8		eleq1	⊢ ( 𝑥 = ∅ → ( 𝑥 ∈ 𝐹 ↔ ∅ ∈ 𝐹 ) )
9	8	biimpac	⊢ ( ( 𝑥 ∈ 𝐹 ∧ 𝑥 = ∅ ) → ∅ ∈ 𝐹 )
10	7 9	sylan2	⊢ ( ( 𝑥 ∈ 𝐹 ∧ 𝑥 ⊆ ( 𝐴 ∩ ( 𝐵 ∖ 𝐴 ) ) ) → ∅ ∈ 𝐹 )
11	10	rexlimiva	⊢ ( ∃ 𝑥 ∈ 𝐹 𝑥 ⊆ ( 𝐴 ∩ ( 𝐵 ∖ 𝐴 ) ) → ∅ ∈ 𝐹 )
12	3 11	syl	⊢ ( ( 𝐹 ∈ ( fBas ‘ 𝑋 ) ∧ 𝐴 ∈ 𝐹 ∧ ( 𝐵 ∖ 𝐴 ) ∈ 𝐹 ) → ∅ ∈ 𝐹 )
13	12	3expia	⊢ ( ( 𝐹 ∈ ( fBas ‘ 𝑋 ) ∧ 𝐴 ∈ 𝐹 ) → ( ( 𝐵 ∖ 𝐴 ) ∈ 𝐹 → ∅ ∈ 𝐹 ) )
14	2 13	mtod	⊢ ( ( 𝐹 ∈ ( fBas ‘ 𝑋 ) ∧ 𝐴 ∈ 𝐹 ) → ¬ ( 𝐵 ∖ 𝐴 ) ∈ 𝐹 )