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 ‘ 𝐵 ) )