Theorem restclsseplem

Description: Lemma for restclssep . (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)$$
	restclsseplem.6	$$⊢\phi \to S\cap T=\varnothing$$
	restclsseplem.7	$$⊢\phi \to T\subseteq Y$$
Assertion	restclsseplem	$$⊢\phi \to \mathrm{cls}\left(J\right)\left(S\right)\cap T=\varnothing$$

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		restclsseplem.6	$$⊢\phi \to S\cap T=\varnothing$$
7		restclsseplem.7	$$⊢\phi \to T\subseteq Y$$
8	1 2 3 4 5	restcls2	$$⊢\phi \to S=\mathrm{cls}\left(J\right)\left(S\right)\cap Y$$
9	8	ineq1d	$$⊢\phi \to S\cap T=\left(\mathrm{cls}\left(J\right)\left(S\right)\cap Y\right)\cap T$$
10		inass	$$⊢\left(\mathrm{cls}\left(J\right)\left(S\right)\cap Y\right)\cap T=\mathrm{cls}\left(J\right)\left(S\right)\cap \left(Y\cap T\right)$$
11	9 10	eqtrdi	$$⊢\phi \to S\cap T=\mathrm{cls}\left(J\right)\left(S\right)\cap \left(Y\cap T\right)$$
12		sseqin2	$$⊢T\subseteq Y\leftrightarrow Y\cap T=T$$
13	7 12	sylib	$$⊢\phi \to Y\cap T=T$$
14	13	ineq2d	$$⊢\phi \to \mathrm{cls}\left(J\right)\left(S\right)\cap \left(Y\cap T\right)=\mathrm{cls}\left(J\right)\left(S\right)\cap T$$
15	11 6 14	3eqtr3rd	$$⊢\phi \to \mathrm{cls}\left(J\right)\left(S\right)\cap T=\varnothing$$