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 ( 𝜑𝐽 ∈ 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 ( 𝜑 → ( 𝑆𝑇 ) = ∅ )