Theorem toprestsubel

Description: A subset is open in the topology it generates via restriction. (Contributed by Glauco Siliprandi, 21-Dec-2024)

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

Proof

Step	Hyp	Ref	Expression
1		toprestsubel.1	|- ( ph -> J e. Top )
2		toprestsubel.2	|- ( ph -> A C_ U. J )
3		eqid	|- U. J = U. J
4	3	topopn	|- ( J e. Top -> U. J e. J )
5	1 4	syl	|- ( ph -> U. J e. J )
6	1 5 2	restsubel	|- ( ph -> A e. ( J |`t A ) )