Theorem restclssep

Description: Two disjoint closed sets in a subspace topology are separated in the original topology. (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$$
	restclssep.7	$$⊢\phi \to T\in \mathrm{Clsd}\left(K\right)$$
Assertion	restclssep	$$⊢\phi \to \left(S\cap \mathrm{cls}\left(J\right)\left(T\right)=\varnothing \wedge \mathrm{cls}\left(J\right)\left(S\right)\cap T=\varnothing \right)$$

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		restclssep.7	$$⊢\phi \to T\in \mathrm{Clsd}\left(K\right)$$
8		incom	$$⊢\mathrm{cls}\left(J\right)\left(T\right)\cap S=S\cap \mathrm{cls}\left(J\right)\left(T\right)$$
9		incom	$$⊢S\cap T=T\cap S$$
10	9 6	eqtr3id	$$⊢\phi \to T\cap S=\varnothing$$
11	1 2 3 4 5	restcls2lem	$$⊢\phi \to S\subseteq Y$$
12	1 2 3 4 7 10 11	restclsseplem	$$⊢\phi \to \mathrm{cls}\left(J\right)\left(T\right)\cap S=\varnothing$$
13	8 12	eqtr3id	$$⊢\phi \to S\cap \mathrm{cls}\left(J\right)\left(T\right)=\varnothing$$
14	1 2 3 4 7	restcls2lem	$$⊢\phi \to T\subseteq Y$$
15	1 2 3 4 5 6 14	restclsseplem	$$⊢\phi \to \mathrm{cls}\left(J\right)\left(S\right)\cap T=\varnothing$$
16	13 15	jca	$$⊢\phi \to \left(S\cap \mathrm{cls}\left(J\right)\left(T\right)=\varnothing \wedge \mathrm{cls}\left(J\right)\left(S\right)\cap T=\varnothing \right)$$