This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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

Proof

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