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