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 𝐴 ) )