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