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 ( ( 𝐽 ∈ Top ∧ 𝐴𝐽 ) → 𝐴 ∈ ( 𝐽t 𝐴 ) )

Proof

Step Hyp Ref Expression
1 simpr ( ( 𝐽 ∈ Top ∧ 𝐴𝐽 ) → 𝐴𝐽 )
2 ssidd ( ( 𝐽 ∈ Top ∧ 𝐴𝐽 ) → 𝐴𝐴 )
3 restopn2 ( ( 𝐽 ∈ Top ∧ 𝐴𝐽 ) → ( 𝐴 ∈ ( 𝐽t 𝐴 ) ↔ ( 𝐴𝐽𝐴𝐴 ) ) )
4 1 2 3 mpbir2and ( ( 𝐽 ∈ Top ∧ 𝐴𝐽 ) → 𝐴 ∈ ( 𝐽t 𝐴 ) )