Metamath Proof Explorer


Theorem topmtcl

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 XVSTopOnX𝒫XSTopOnX

Proof

Step Hyp Ref Expression
1 toponmre XVTopOnXMoore𝒫X
2 mrerintcl TopOnXMoore𝒫XSTopOnX𝒫XSTopOnX
3 1 2 sylan XVSTopOnX𝒫XSTopOnX