Metamath Proof Explorer

Theorem snfbas

Description: Condition for a singleton to be a filter base. (Contributed by Stefan O'Rear, 2-Aug-2015)

Ref Expression
Assertion snfbas ⊢ A ⊆ B ∧ A ≠ ∅ ∧ B ∈ V → A ∈ fBas ⁡ B

Proof

Step Hyp Ref Expression
1 ssexg ⊢ A ⊆ B ∧ B ∈ V → A ∈ V
2 1 3adant2 ⊢ A ⊆ B ∧ A ≠ ∅ ∧ B ∈ V → A ∈ V
3 simp2 ⊢ A ⊆ B ∧ A ≠ ∅ ∧ B ∈ V → A ≠ ∅
4 snfil ⊢ A ∈ V ∧ A ≠ ∅ → A ∈ Fil ⁡ A
5 2 3 4 syl2anc ⊢ A ⊆ B ∧ A ≠ ∅ ∧ B ∈ V → A ∈ Fil ⁡ A
6 filfbas ⊢ A ∈ Fil ⁡ A → A ∈ fBas ⁡ A
7 5 6 syl ⊢ A ⊆ B ∧ A ≠ ∅ ∧ B ∈ V → A ∈ fBas ⁡ A
8 simp1 ⊢ A ⊆ B ∧ A ≠ ∅ ∧ B ∈ V → A ⊆ B
9 elpw2g ⊢ B ∈ V → A ∈ 𝒫 B ↔ A ⊆ B
10 9 3ad2ant3 ⊢ A ⊆ B ∧ A ≠ ∅ ∧ B ∈ V → A ∈ 𝒫 B ↔ A ⊆ B
11 8 10 mpbird ⊢ A ⊆ B ∧ A ≠ ∅ ∧ B ∈ V → A ∈ 𝒫 B
12 11 snssd ⊢ A ⊆ B ∧ A ≠ ∅ ∧ B ∈ V → A ⊆ 𝒫 B
13 simp3 ⊢ A ⊆ B ∧ A ≠ ∅ ∧ B ∈ V → B ∈ V
14 fbasweak ⊢ A ∈ fBas ⁡ A ∧ A ⊆ 𝒫 B ∧ B ∈ V → A ∈ fBas ⁡ B
15 7 12 13 14 syl3anc ⊢ A ⊆ B ∧ A ≠ ∅ ∧ B ∈ V → A ∈ fBas ⁡ B