toplly

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

		Ref	Expression
	Assertion	toplly	$⊢ LocallyTop=Top$

Step	Hyp	Ref	Expression
1		llytop	$⊢ j \in LocallyTop\toj \in Top$
2	1	ssriv	$⊢ LocallyTop\subseteqTop$
3		resttop	$⊢ (j \in Top \land x \in j) \to j ↾_{𝑡} x \in Top$
4	3	adantl	$⊢ (⊤ \land (j \in Top \land x \in j)) \to j ↾_{𝑡} x \in Top$
5		ssidd	$⊢ ⊤ \to Top \subseteq Top$
6	4 5	restlly	$⊢ ⊤ \to Top \subseteq LocallyTop$
7	6	mptru	$⊢ Top \subseteq LocallyTop$
8	2 7	eqssi	$⊢ LocallyTop=Top$

Metamath Proof Explorer