Theorem toplly

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

	Ref	Expression
Assertion	toplly	|- Locally Top = Top

Proof

Step	Hyp	Ref	Expression
1		llytop	|- ( j e. Locally Top -> j e. Top )
2	1	ssriv	|- Locally Top C_ Top
3		resttop	|- ( ( j e. Top /\ x e. j ) -> ( j |`t x ) e. Top )
4	3	adantl	|- ( ( T. /\ ( j e. Top /\ x e. j ) ) -> ( j |`t x ) e. Top )
5		ssidd	|- ( T. -> Top C_ Top )
6	4 5	restlly	|- ( T. -> Top C_ Locally Top )
7	6	mptru	|- Top C_ Locally Top
8	2 7	eqssi	|- Locally Top = Top