Theorem sepdisj

Description: Separated sets are disjoint. Note that in general separatedness also requires T C_ U. J and ( S i^i ( ( clsJ )T ) ) = (/) as well but they are unnecessary here. (Contributed by Zhi Wang, 7-Sep-2024)

	Ref	Expression
Hypotheses	sepdisj.1	$$⊢\phi \to J\in \mathrm{Top}$$
	sepdisj.2	$$⊢\phi \to S\subseteq \bigcup J$$
	sepdisj.3	$$⊢\phi \to \mathrm{cls}\left(J\right)\left(S\right)\cap T=\varnothing$$
Assertion	sepdisj	$$⊢\phi \to S\cap T=\varnothing$$

Proof

Step	Hyp	Ref	Expression
1		sepdisj.1	$$⊢\phi \to J\in \mathrm{Top}$$
2		sepdisj.2	$$⊢\phi \to S\subseteq \bigcup J$$
3		sepdisj.3	$$⊢\phi \to \mathrm{cls}\left(J\right)\left(S\right)\cap T=\varnothing$$
4		eqid	$$⊢\bigcup J=\bigcup J$$
5	4	sscls	$$⊢\left(J\in \mathrm{Top}\wedge S\subseteq \bigcup J\right)\to S\subseteq \mathrm{cls}\left(J\right)\left(S\right)$$
6	1 2 5	syl2anc	$$⊢\phi \to S\subseteq \mathrm{cls}\left(J\right)\left(S\right)$$
7	6 3	ssdisjd	$$⊢\phi \to S\cap T=\varnothing$$