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	$$⊢\phi \to J\in \mathrm{Top}$$
	toprestsubel.2	$$⊢\phi \to A\subseteq \bigcup J$$
Assertion	toprestsubel	$$⊢\phi \to A\in \left(J{\upharpoonright }_{𝑡}A\right)$$

Proof

Step	Hyp	Ref	Expression
1		toprestsubel.1	$$⊢\phi \to J\in \mathrm{Top}$$
2		toprestsubel.2	$$⊢\phi \to A\subseteq \bigcup J$$
3		eqid	$$⊢\bigcup J=\bigcup J$$
4	3	topopn	$$⊢J\in \mathrm{Top}\to \bigcup J\in J$$
5	1 4	syl	$$⊢\phi \to \bigcup J\in J$$
6	1 5 2	restsubel	$$⊢\phi \to A\in \left(J{\upharpoonright }_{𝑡}A\right)$$