Metamath Proof Explorer

Theorem fbdmn0

Description: The domain of a filter base is nonempty. (Contributed by Mario Carneiro, 28-Nov-2013) (Revised by Stefan O'Rear, 28-Jul-2015)

Ref Expression
Assertion fbdmn0 ⊢ F ∈ fBas ⁡ B → B ≠ ∅

Proof

Step Hyp Ref Expression
1 0nelfb ⊢ F ∈ fBas ⁡ B → ¬ ∅ ∈ F
2 fveq2 ⊢ B = ∅ → fBas ⁡ B = fBas ⁡ ∅
3 2 eleq2d ⊢ B = ∅ → F ∈ fBas ⁡ B ↔ F ∈ fBas ⁡ ∅
4 3 biimpd ⊢ B = ∅ → F ∈ fBas ⁡ B → F ∈ fBas ⁡ ∅
5 fbasne0 ⊢ F ∈ fBas ⁡ ∅ → F ≠ ∅
6 n0 ⊢ F ≠ ∅ ↔ ∃ x x ∈ F
7 5 6 sylib ⊢ F ∈ fBas ⁡ ∅ → ∃ x x ∈ F
8 fbelss ⊢ F ∈ fBas ⁡ ∅ ∧ x ∈ F → x ⊆ ∅
9 ss0 ⊢ x ⊆ ∅ → x = ∅
10 8 9 syl ⊢ F ∈ fBas ⁡ ∅ ∧ x ∈ F → x = ∅
11 simpr ⊢ F ∈ fBas ⁡ ∅ ∧ x ∈ F → x ∈ F
12 10 11 eqeltrrd ⊢ F ∈ fBas ⁡ ∅ ∧ x ∈ F → ∅ ∈ F
13 7 12 exlimddv ⊢ F ∈ fBas ⁡ ∅ → ∅ ∈ F
14 4 13 syl6com ⊢ F ∈ fBas ⁡ B → B = ∅ → ∅ ∈ F
15 14 necon3bd ⊢ F ∈ fBas ⁡ B → ¬ ∅ ∈ F → B ≠ ∅
16 1 15 mpd ⊢ F ∈ fBas ⁡ B → B ≠ ∅