Metamath Proof Explorer

Theorem llytop

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

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

Proof

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