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 fiATopBases

Proof

Step Hyp Ref Expression
1 fvex fiAV
2 fiin xfiAyfiAxyfiA
3 2 rgen2 xfiAyfiAxyfiA
4 fiinbas fiAVxfiAyfiAxyfiAfiATopBases
5 1 3 4 mp2an fiATopBases