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

Metamath Proof Explorer

Theorem restopnssd

Description: A topology restricted to an open set is a subset of the original topology. (Contributed by Glauco Siliprandi, 21-Dec-2024)

Ref Expression
Hypotheses restopnssd.1 ⊢ ( 𝜑 → 𝐽 ∈ Top )
restopnssd.2 ⊢ ( 𝜑 → 𝐴 ∈ 𝐽 )
Assertion restopnssd ( 𝜑 → ( 𝐽 ↾t 𝐴 ) ⊆ 𝐽 )

Proof

Step Hyp Ref Expression
1 restopnssd.1 ⊢ ( 𝜑 → 𝐽 ∈ Top )
2 restopnssd.2 ⊢ ( 𝜑 → 𝐴 ∈ 𝐽 )
3 simpr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐽 ↾t 𝐴 ) ) → 𝑥 ∈ ( 𝐽 ↾t 𝐴 ) )
4 1 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐽 ↾t 𝐴 ) ) → 𝐽 ∈ Top )
5 2 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐽 ↾t 𝐴 ) ) → 𝐴 ∈ 𝐽 )
6 restopn2 ⊢ ( ( 𝐽 ∈ Top ∧ 𝐴 ∈ 𝐽 ) → ( 𝑥 ∈ ( 𝐽 ↾t 𝐴 ) ↔ ( 𝑥 ∈ 𝐽 ∧ 𝑥 ⊆ 𝐴 ) ) )
7 4 5 6 syl2anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐽 ↾t 𝐴 ) ) → ( 𝑥 ∈ ( 𝐽 ↾t 𝐴 ) ↔ ( 𝑥 ∈ 𝐽 ∧ 𝑥 ⊆ 𝐴 ) ) )
8 3 7 mpbid ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐽 ↾t 𝐴 ) ) → ( 𝑥 ∈ 𝐽 ∧ 𝑥 ⊆ 𝐴 ) )
9 8 simpld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐽 ↾t 𝐴 ) ) → 𝑥 ∈ 𝐽 )
10 9 ssd ⊢ ( 𝜑 → ( 𝐽 ↾t 𝐴 ) ⊆ 𝐽 )