Description: The meet of a collection of topologies on X is again a topology on X . (Contributed by Jeff Hankins, 5-Oct-2009) (Proof shortened by Mario Carneiro, 12-Sep-2015)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | topmtcl | |- ( ( X e. V /\ S C_ ( TopOn ` X ) ) -> ( ~P X i^i |^| S ) e. ( TopOn ` X ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | toponmre | |- ( X e. V -> ( TopOn ` X ) e. ( Moore ` ~P X ) ) |
|
| 2 | mrerintcl | |- ( ( ( TopOn ` X ) e. ( Moore ` ~P X ) /\ S C_ ( TopOn ` X ) ) -> ( ~P X i^i |^| S ) e. ( TopOn ` X ) ) |
|
| 3 | 1 2 | sylan | |- ( ( X e. V /\ S C_ ( TopOn ` X ) ) -> ( ~P X i^i |^| S ) e. ( TopOn ` X ) ) |