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 φ J Top
sepdisj.2 φ S J
sepdisj.3 φ cls J S T =
Assertion sepdisj φ S T =

Proof

Step Hyp Ref Expression
1 sepdisj.1 φ J Top
2 sepdisj.2 φ S J
3 sepdisj.3 φ cls J S T =
4 eqid J = J
5 4 sscls J Top S J S cls J S
6 1 2 5 syl2anc φ S cls J S
7 6 3 ssdisjd φ S T =