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	|- ( ph -> J e. Top )
	sepdisj.2	|- ( ph -> S C_ U. J )
	sepdisj.3	|- ( ph -> ( ( ( cls ` J ) ` S ) i^i T ) = (/) )
Assertion	sepdisj	|- ( ph -> ( S i^i T ) = (/) )

Proof

Step	Hyp	Ref	Expression
1		sepdisj.1	|- ( ph -> J e. Top )
2		sepdisj.2	|- ( ph -> S C_ U. J )
3		sepdisj.3	|- ( ph -> ( ( ( cls ` J ) ` S ) i^i T ) = (/) )
4		eqid	|- U. J = U. J
5	4	sscls	|- ( ( J e. Top /\ S C_ U. J ) -> S C_ ( ( cls ` J ) ` S ) )
6	1 2 5	syl2anc	|- ( ph -> S C_ ( ( cls ` J ) ` S ) )
7	6 3	ssdisjd	|- ( ph -> ( S i^i T ) = (/) )