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	⊢ ( 𝑗 ∈ Locally Top → 𝑗 ∈ Top )
2	1	ssriv	⊢ Locally Top ⊆ Top
3		resttop	⊢ ( ( 𝑗 ∈ Top ∧ 𝑥 ∈ 𝑗 ) → ( 𝑗 ↾t 𝑥 ) ∈ Top )
4	3	adantl	⊢ ( ( ⊤ ∧ ( 𝑗 ∈ Top ∧ 𝑥 ∈ 𝑗 ) ) → ( 𝑗 ↾t 𝑥 ) ∈ Top )
5		ssidd	⊢ ( ⊤ → Top ⊆ Top )
6	4 5	restlly	⊢ ( ⊤ → Top ⊆ Locally Top )
7	6	mptru	⊢ Top ⊆ Locally Top
8	2 7	eqssi	⊢ Locally Top = Top