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 ⊢ φ → J ∈ Top
restopnssd.2 ⊢ φ → A ∈ J
Assertion restopnssd ⊢ φ → J ↾ 𝑡 A ⊆ J

Proof

Step Hyp Ref Expression
1 restopnssd.1 ⊢ φ → J ∈ Top
2 restopnssd.2 ⊢ φ → A ∈ J
3 simpr ⊢ φ ∧ x ∈ J ↾ 𝑡 A → x ∈ J ↾ 𝑡 A
4 1 adantr ⊢ φ ∧ x ∈ J ↾ 𝑡 A → J ∈ Top
5 2 adantr ⊢ φ ∧ x ∈ J ↾ 𝑡 A → A ∈ J
6 restopn2 ⊢ J ∈ Top ∧ A ∈ J → x ∈ J ↾ 𝑡 A ↔ x ∈ J ∧ x ⊆ A
7 4 5 6 syl2anc ⊢ φ ∧ x ∈ J ↾ 𝑡 A → x ∈ J ↾ 𝑡 A ↔ x ∈ J ∧ x ⊆ A
8 3 7 mpbid ⊢ φ ∧ x ∈ J ↾ 𝑡 A → x ∈ J ∧ x ⊆ A
9 8 simpld ⊢ φ ∧ x ∈ J ↾ 𝑡 A → x ∈ J
10 9 ssd ⊢ φ → J ↾ 𝑡 A ⊆ J