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 \in LocallyA\toJ \in Top$

Step	Hyp	Ref	Expression
1		islly	$⊢ J \in LocallyA\leftrightarrow(J \in Top \land \forall x \in J \forall y \in x \exists u \in (J \cap 𝒫 x) (y \in u \land J ↾_{𝑡} u \in A))$
2	1	simplbi	$⊢ J \in LocallyA\toJ \in Top$