Metamath Proof Explorer


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 φJTop
sepdisj.2 φSJ
sepdisj.3 φclsJST=
Assertion sepdisj φST=

Proof

Step Hyp Ref Expression
1 sepdisj.1 φJTop
2 sepdisj.2 φSJ
3 sepdisj.3 φclsJST=
4 eqid J=J
5 4 sscls JTopSJSclsJS
6 1 2 5 syl2anc φSclsJS
7 6 3 ssdisjd φST=