This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem 0nelfb

Description: No filter base contains the empty set. (Contributed by Jeff Hankins, 1-Sep-2009) (Revised by Mario Carneiro, 28-Jul-2015)

Ref Expression
Assertion 0nelfb ( 𝐹 ∈ ( fBas ‘ 𝐵 ) → ¬ ∅ ∈ 𝐹 )

Proof

Step Hyp Ref Expression
1 elfvdm ⊢ ( 𝐹 ∈ ( fBas ‘ 𝐵 ) → 𝐵 ∈ dom fBas )
2 isfbas ⊢ ( 𝐵 ∈ dom fBas → ( 𝐹 ∈ ( fBas ‘ 𝐵 ) ↔ ( 𝐹 ⊆ 𝒫 𝐵 ∧ ( 𝐹 ≠ ∅ ∧ ∅ ∉ 𝐹 ∧ ∀ 𝑥 ∈ 𝐹 ∀ 𝑦 ∈ 𝐹 ( 𝐹 ∩ 𝒫 ( 𝑥 ∩ 𝑦 ) ) ≠ ∅ ) ) ) )
3 1 2 syl ⊢ ( 𝐹 ∈ ( fBas ‘ 𝐵 ) → ( 𝐹 ∈ ( fBas ‘ 𝐵 ) ↔ ( 𝐹 ⊆ 𝒫 𝐵 ∧ ( 𝐹 ≠ ∅ ∧ ∅ ∉ 𝐹 ∧ ∀ 𝑥 ∈ 𝐹 ∀ 𝑦 ∈ 𝐹 ( 𝐹 ∩ 𝒫 ( 𝑥 ∩ 𝑦 ) ) ≠ ∅ ) ) ) )
4 3 ibi ⊢ ( 𝐹 ∈ ( fBas ‘ 𝐵 ) → ( 𝐹 ⊆ 𝒫 𝐵 ∧ ( 𝐹 ≠ ∅ ∧ ∅ ∉ 𝐹 ∧ ∀ 𝑥 ∈ 𝐹 ∀ 𝑦 ∈ 𝐹 ( 𝐹 ∩ 𝒫 ( 𝑥 ∩ 𝑦 ) ) ≠ ∅ ) ) )
5 simpr2 ⊢ ( ( 𝐹 ⊆ 𝒫 𝐵 ∧ ( 𝐹 ≠ ∅ ∧ ∅ ∉ 𝐹 ∧ ∀ 𝑥 ∈ 𝐹 ∀ 𝑦 ∈ 𝐹 ( 𝐹 ∩ 𝒫 ( 𝑥 ∩ 𝑦 ) ) ≠ ∅ ) ) → ∅ ∉ 𝐹 )
6 4 5 syl ⊢ ( 𝐹 ∈ ( fBas ‘ 𝐵 ) → ∅ ∉ 𝐹 )
7 df-nel ⊢ ( ∅ ∉ 𝐹 ↔ ¬ ∅ ∈ 𝐹 )
8 6 7 sylib ⊢ ( 𝐹 ∈ ( fBas ‘ 𝐵 ) → ¬ ∅ ∈ 𝐹 )