Metamath Proof Explorer

Theorem nllytop

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

Ref Expression
Assertion nllytop 
|- ( J e. N-Locally A -> J e. Top )

Proof

Step Hyp Ref Expression
1 isnlly 
 |-  ( J e. N-Locally A <-> ( J e. Top /\ A. x e. J A. y e. x E. u e. ( ( ( nei ` J ) ` { y } ) i^i ~P x ) ( J |`t u ) e. A ) )
2 1 simplbi 
 |-  ( J e. N-Locally A -> J e. Top )