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 e. Top /\ A e. J ) -> A e. ( J |`t A ) )

Proof

Step	Hyp	Ref	Expression
1		simpr	|- ( ( J e. Top /\ A e. J ) -> A e. J )
2		ssidd	|- ( ( J e. Top /\ A e. J ) -> A C_ A )
3		restopn2	|- ( ( J e. Top /\ A e. J ) -> ( A e. ( J |`t A ) <-> ( A e. J /\ A C_ A ) ) )
4	1 2 3	mpbir2and	|- ( ( J e. Top /\ A e. J ) -> A e. ( J |`t A ) )