This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem toprestsubel

Description: A subset is open in the topology it generates via restriction. (Contributed by Glauco Siliprandi, 21-Dec-2024)

Ref Expression
Hypotheses toprestsubel.1 ⊢ φ → J ∈ Top
toprestsubel.2 ⊢ φ → A ⊆ ⋃ J
Assertion toprestsubel ⊢ φ → A ∈ J ↾ 𝑡 A

Proof

Step Hyp Ref Expression
1 toprestsubel.1 ⊢ φ → J ∈ Top
2 toprestsubel.2 ⊢ φ → A ⊆ ⋃ J
3 eqid ⊢ ⋃ J = ⋃ J
4 3 topopn ⊢ J ∈ Top → ⋃ J ∈ J
5 1 4 syl ⊢ φ → ⋃ J ∈ J
6 1 5 2 restsubel ⊢ φ → A ∈ J ↾ 𝑡 A