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