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

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 ( ( 𝐴 ⊆ 𝐵 ∧ 𝐴 ≠ ∅ ∧ 𝐵 ∈ 𝑉 ) → { 𝐴 } ∈ ( fBas ‘ 𝐵 ) )

Proof

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