Metamath Proof Explorer

Theorem topnlly

Description: A topology is n-locally a topology. (Contributed by Mario Carneiro, 2-Mar-2015)

Ref Expression
Assertion topnlly 
|- N-Locally Top = Top

Proof

Step Hyp Ref Expression
1 toplly 
 |-  Locally Top = Top
2 loclly 
 |-  ( Locally Top = Top <-> N-Locally Top = Top )
3 1 2 mpbi 
 |-  N-Locally Top = Top