Theorem restcls2lem

Description: A closed set in a subspace topology is a subset of the subspace. (Contributed by Zhi Wang, 2-Sep-2024)

	Ref	Expression
Hypotheses	restcls2.1	$$⊢\phi \to J\in \mathrm{Top}$$
	restcls2.2	$$⊢\phi \to X=\bigcup J$$
	restcls2.3	$$⊢\phi \to Y\subseteq X$$
	restcls2.4	$$⊢\phi \to K=J{\upharpoonright }_{𝑡}Y$$
	restcls2.5	$$⊢\phi \to S\in \mathrm{Clsd}\left(K\right)$$
Assertion	restcls2lem	$$⊢\phi \to S\subseteq Y$$

Proof

Step	Hyp	Ref	Expression
1		restcls2.1	$$⊢\phi \to J\in \mathrm{Top}$$
2		restcls2.2	$$⊢\phi \to X=\bigcup J$$
3		restcls2.3	$$⊢\phi \to Y\subseteq X$$
4		restcls2.4	$$⊢\phi \to K=J{\upharpoonright }_{𝑡}Y$$
5		restcls2.5	$$⊢\phi \to S\in \mathrm{Clsd}\left(K\right)$$
6		eqid	$$⊢\bigcup K=\bigcup K$$
7	6	cldss	$$⊢S\in \mathrm{Clsd}\left(K\right)\to S\subseteq \bigcup K$$
8	5 7	syl	$$⊢\phi \to S\subseteq \bigcup K$$
9	3 2	sseqtrd	$$⊢\phi \to Y\subseteq \bigcup J$$
10		eqid	$$⊢\bigcup J=\bigcup J$$
11	10	restuni	$$⊢\left(J\in \mathrm{Top}\wedge Y\subseteq \bigcup J\right)\to Y=\bigcup \left(J{\upharpoonright }_{𝑡}Y\right)$$
12	1 9 11	syl2anc	$$⊢\phi \to Y=\bigcup \left(J{\upharpoonright }_{𝑡}Y\right)$$
13	4	unieqd	$$⊢\phi \to \bigcup K=\bigcup \left(J{\upharpoonright }_{𝑡}Y\right)$$
14	12 13	eqtr4d	$$⊢\phi \to Y=\bigcup K$$
15	8 14	sseqtrrd	$$⊢\phi \to S\subseteq Y$$