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≠∅↔∃xx∈F
7 5 6 sylib ⊢F∈fBas⁡∅→∃xx∈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≠∅