Metamath Proof Explorer


Theorem fbsspw

Description: A filter base on a set is a subset of the power set. (Contributed by Stefan O'Rear, 28-Jul-2015)

Ref Expression
Assertion fbsspw FfBasBF𝒫B

Proof

Step Hyp Ref Expression
1 elfvdm FfBasBBdomfBas
2 isfbas BdomfBasFfBasBF𝒫BFFxFyFF𝒫xy
3 1 2 syl FfBasBFfBasBF𝒫BFFxFyFF𝒫xy
4 3 ibi FfBasBF𝒫BFFxFyFF𝒫xy
5 4 simpld FfBasBF𝒫B