# Metamath Proof Explorer

## Theorem fibas

Description: A collection of finite intersections is a basis. The initial set is a subbasis for the topology. (Contributed by Jeff Hankins, 25-Aug-2009) (Revised by Mario Carneiro, 24-Nov-2013)

Ref Expression
Assertion fibas ${⊢}\mathrm{fi}\left({A}\right)\in \mathrm{TopBases}$

### Proof

Step Hyp Ref Expression
1 fvex ${⊢}\mathrm{fi}\left({A}\right)\in \mathrm{V}$
2 fiin ${⊢}\left({x}\in \mathrm{fi}\left({A}\right)\wedge {y}\in \mathrm{fi}\left({A}\right)\right)\to {x}\cap {y}\in \mathrm{fi}\left({A}\right)$
3 2 rgen2 ${⊢}\forall {x}\in \mathrm{fi}\left({A}\right)\phantom{\rule{.4em}{0ex}}\forall {y}\in \mathrm{fi}\left({A}\right)\phantom{\rule{.4em}{0ex}}{x}\cap {y}\in \mathrm{fi}\left({A}\right)$
4 fiinbas ${⊢}\left(\mathrm{fi}\left({A}\right)\in \mathrm{V}\wedge \forall {x}\in \mathrm{fi}\left({A}\right)\phantom{\rule{.4em}{0ex}}\forall {y}\in \mathrm{fi}\left({A}\right)\phantom{\rule{.4em}{0ex}}{x}\cap {y}\in \mathrm{fi}\left({A}\right)\right)\to \mathrm{fi}\left({A}\right)\in \mathrm{TopBases}$
5 1 3 4 mp2an ${⊢}\mathrm{fi}\left({A}\right)\in \mathrm{TopBases}$