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 \in Top \land A \in J) \to A \in (J ↾_{𝑡} A)$

Step	Hyp	Ref	Expression
1		simpr	$⊢ (J \in Top \land A \in J) \to A \in J$
2		ssidd	$⊢ (J \in Top \land A \in J) \to A \subseteq A$
3		restopn2	$⊢ (J \in Top \land A \in J) \to (A \in (J ↾_{𝑡} A) \leftrightarrow (A \in J \land A \subseteq A))$
4	1 2 3	mpbir2and	$⊢ (J \in Top \land A \in J) \to A \in (J ↾_{𝑡} A)$