Metamath Proof Explorer


Theorem fbasne0

Description: There are no empty filter bases. (Contributed by Jeff Hankins, 1-Sep-2009) (Revised by Mario Carneiro, 28-Jul-2015)

Ref Expression
Assertion fbasne0 ( 𝐹 ∈ ( 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 simpr1 ( ( 𝐹 ⊆ 𝒫 𝐵 ∧ ( 𝐹 ≠ ∅ ∧ ∅ ∉ 𝐹 ∧ ∀ 𝑥𝐹𝑦𝐹 ( 𝐹 ∩ 𝒫 ( 𝑥𝑦 ) ) ≠ ∅ ) ) → 𝐹 ≠ ∅ )
6 4 5 syl ( 𝐹 ∈ ( fBas ‘ 𝐵 ) → 𝐹 ≠ ∅ )