Metamath Proof Explorer

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 ∈ Locally Top → j ∈ Top
2 1 ssriv ⊢ Locally Top ⊆ Top
3 resttop ⊢ j ∈ Top ∧ x ∈ j → j ↾ 𝑡 x ∈ Top
4 3 adantl ⊢ ⊤ ∧ j ∈ Top ∧ x ∈ j → j ↾ 𝑡 x ∈ 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