Metamath Proof Explorer


Theorem fiinbas

Description: If a set is closed under finite intersection, then it is a basis for a topology. (Contributed by Jeff Madsen, 2-Sep-2009)

Ref Expression
Assertion fiinbas BCxByBxyBBTopBases

Proof

Step Hyp Ref Expression
1 ssid xyxy
2 eleq2 w=xyzwzxy
3 sseq1 w=xywxyxyxy
4 2 3 anbi12d w=xyzwwxyzxyxyxy
5 4 rspcev xyBzxyxyxywBzwwxy
6 1 5 mpanr2 xyBzxywBzwwxy
7 6 ralrimiva xyBzxywBzwwxy
8 7 a1i BCxyBzxywBzwwxy
9 8 ralimdv BCyBxyByBzxywBzwwxy
10 9 ralimdv BCxByBxyBxByBzxywBzwwxy
11 isbasis2g BCBTopBasesxByBzxywBzwwxy
12 10 11 sylibrd BCxByBxyBBTopBases
13 12 imp BCxByBxyBBTopBases