Theorem restopnssd

Description: A topology restricted to an open set is a subset of the original topology. (Contributed by Glauco Siliprandi, 21-Dec-2024)

	Ref	Expression
Hypotheses	restopnssd.1	|- ( ph -> J e. Top )
	restopnssd.2	|- ( ph -> A e. J )
Assertion	restopnssd	|- ( ph -> ( J |`t A ) C_ J )

Proof

Step	Hyp	Ref	Expression
1		restopnssd.1	|- ( ph -> J e. Top )
2		restopnssd.2	|- ( ph -> A e. J )
3		simpr	|- ( ( ph /\ x e. ( J |`t A ) ) -> x e. ( J |`t A ) )
4	1	adantr	|- ( ( ph /\ x e. ( J |`t A ) ) -> J e. Top )
5	2	adantr	|- ( ( ph /\ x e. ( J |`t A ) ) -> A e. J )
6		restopn2	|- ( ( J e. Top /\ A e. J ) -> ( x e. ( J |`t A ) <-> ( x e. J /\ x C_ A ) ) )
7	4 5 6	syl2anc	|- ( ( ph /\ x e. ( J |`t A ) ) -> ( x e. ( J |`t A ) <-> ( x e. J /\ x C_ A ) ) )
8	3 7	mpbid	|- ( ( ph /\ x e. ( J |`t A ) ) -> ( x e. J /\ x C_ A ) )
9	8	simpld	|- ( ( ph /\ x e. ( J |`t A ) ) -> x e. J )
10	9	ssd	|- ( ph -> ( J |`t A ) C_ J )