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

Metamath Proof Explorer

Theorem restopn3

Description: If A is open, then A is open in the restriction to itself. (Contributed by Glauco Siliprandi, 21-Dec-2024)

Ref Expression
Assertion restopn3 ⊢ J ∈ Top ∧ A ∈ J → A ∈ J ↾ 𝑡 A

Proof

Step Hyp Ref Expression
1 simpr ⊢ J ∈ Top ∧ A ∈ J → A ∈ J
2 ssidd ⊢ J ∈ Top ∧ A ∈ J → A ⊆ A
3 restopn2 ⊢ J ∈ Top ∧ A ∈ J → A ∈ J ↾ 𝑡 A ↔ A ∈ J ∧ A ⊆ A
4 1 2 3 mpbir2and ⊢ J ∈ Top ∧ A ∈ J → A ∈ J ↾ 𝑡 A