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 ‘ 𝐵 ) → 𝐹 ≠ ∅ )