Theorem restcls2

Description: A closed set in a subspace topology is the closure in the original topology intersecting with 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	restcls2	$$⊢\phi \to S=\mathrm{cls}\left(J\right)\left(S\right)\cap 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	4	fveq2d	$$⊢\phi \to \mathrm{cls}\left(K\right)=\mathrm{cls}\left(J{\upharpoonright }_{𝑡}Y\right)$$
7	6	fveq1d	$$⊢\phi \to \mathrm{cls}\left(K\right)\left(S\right)=\mathrm{cls}\left(J{\upharpoonright }_{𝑡}Y\right)\left(S\right)$$
8		cldcls	$$⊢S\in \mathrm{Clsd}\left(K\right)\to \mathrm{cls}\left(K\right)\left(S\right)=S$$
9	5 8	syl	$$⊢\phi \to \mathrm{cls}\left(K\right)\left(S\right)=S$$
10	3 2	sseqtrd	$$⊢\phi \to Y\subseteq \bigcup J$$
11	1 2 3 4 5	restcls2lem	$$⊢\phi \to S\subseteq Y$$
12		eqid	$$⊢\bigcup J=\bigcup J$$
13		eqid	$$⊢J{\upharpoonright }_{𝑡}Y=J{\upharpoonright }_{𝑡}Y$$
14	12 13	restcls	$$⊢\left(J\in \mathrm{Top}\wedge Y\subseteq \bigcup J\wedge S\subseteq Y\right)\to \mathrm{cls}\left(J{\upharpoonright }_{𝑡}Y\right)\left(S\right)=\mathrm{cls}\left(J\right)\left(S\right)\cap Y$$
15	1 10 11 14	syl3anc	$$⊢\phi \to \mathrm{cls}\left(J{\upharpoonright }_{𝑡}Y\right)\left(S\right)=\mathrm{cls}\left(J\right)\left(S\right)\cap Y$$
16	7 9 15	3eqtr3d	$$⊢\phi \to S=\mathrm{cls}\left(J\right)\left(S\right)\cap Y$$