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 | |- ( fi ` A ) e. TopBases |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | fvex | |- ( fi ` A ) e. _V |
|
| 2 | fiin | |- ( ( x e. ( fi ` A ) /\ y e. ( fi ` A ) ) -> ( x i^i y ) e. ( fi ` A ) ) |
|
| 3 | 2 | rgen2 | |- A. x e. ( fi ` A ) A. y e. ( fi ` A ) ( x i^i y ) e. ( fi ` A ) |
| 4 | fiinbas | |- ( ( ( fi ` A ) e. _V /\ A. x e. ( fi ` A ) A. y e. ( fi ` A ) ( x i^i y ) e. ( fi ` A ) ) -> ( fi ` A ) e. TopBases ) |
|
| 5 | 1 3 4 | mp2an | |- ( fi ` A ) e. TopBases |