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	⊢ ( 𝜑 → 𝐽 ∈ Top )
	sepdisj.2	⊢ ( 𝜑 → 𝑆 ⊆ ∪ 𝐽 )
	sepdisj.3	⊢ ( 𝜑 → ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∩ 𝑇 ) = ∅ )
Assertion	sepdisj	⊢ ( 𝜑 → ( 𝑆 ∩ 𝑇 ) = ∅ )

Proof

Step	Hyp	Ref	Expression
1		sepdisj.1	⊢ ( 𝜑 → 𝐽 ∈ Top )
2		sepdisj.2	⊢ ( 𝜑 → 𝑆 ⊆ ∪ 𝐽 )
3		sepdisj.3	⊢ ( 𝜑 → ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∩ 𝑇 ) = ∅ )
4		eqid	⊢ ∪ 𝐽 = ∪ 𝐽
5	4	sscls	⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ ∪ 𝐽 ) → 𝑆 ⊆ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) )
6	1 2 5	syl2anc	⊢ ( 𝜑 → 𝑆 ⊆ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) )
7	6 3	ssdisjd	⊢ ( 𝜑 → ( 𝑆 ∩ 𝑇 ) = ∅ )