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 ⊢ ( 𝜑 → 𝐽 ∈ Top )
toprestsubel.2 ⊢ ( 𝜑 → 𝐴 ⊆ ∪ 𝐽 )
Assertion toprestsubel ( 𝜑 → 𝐴 ∈ ( 𝐽 ↾t 𝐴 ) )

Proof

Step Hyp Ref Expression
1 toprestsubel.1 ⊢ ( 𝜑 → 𝐽 ∈ Top )
2 toprestsubel.2 ⊢ ( 𝜑 → 𝐴 ⊆ ∪ 𝐽 )
3 eqid ⊢ ∪ 𝐽 = ∪ 𝐽
4 3 topopn ⊢ ( 𝐽 ∈ Top → ∪ 𝐽 ∈ 𝐽 )
5 1 4 syl ⊢ ( 𝜑 → ∪ 𝐽 ∈ 𝐽 )
6 1 5 2 restsubel ⊢ ( 𝜑 → 𝐴 ∈ ( 𝐽 ↾t 𝐴 ) )