Metamath Proof Explorer

Theorem clddisj

Description: Two ways of saying that two closed sets are disjoint, if J is a topology and X is a closed set. An alternative proof is similar to that of opndisj with elssuni replaced by the combination of cldss and eqid . (Contributed by Zhi Wang, 6-Sep-2024)

Ref Expression
Assertion clddisj ⊢ Z = ⋃ J ∖ X → Y ∈ Clsd ⁡ J ∩ 𝒫 Z ↔ Y ∈ Clsd ⁡ J ∧ X ∩ Y = ∅

Proof

Step Hyp Ref Expression
1 elin ⊢ Y ∈ Clsd ⁡ J ∩ 𝒫 Z ↔ Y ∈ Clsd ⁡ J ∧ Y ∈ 𝒫 Z
2 simpl ⊢ Z = ⋃ J ∖ X ∧ Y ∈ Clsd ⁡ J → Z = ⋃ J ∖ X
3 cldrcl ⊢ Y ∈ Clsd ⁡ J → J ∈ Top
4 clduni ⊢ J ∈ Top → ⋃ Clsd ⁡ J = ⋃ J
5 4 difeq1d ⊢ J ∈ Top → ⋃ Clsd ⁡ J ∖ X = ⋃ J ∖ X
6 3 5 syl ⊢ Y ∈ Clsd ⁡ J → ⋃ Clsd ⁡ J ∖ X = ⋃ J ∖ X
7 6 adantl ⊢ Z = ⋃ J ∖ X ∧ Y ∈ Clsd ⁡ J → ⋃ Clsd ⁡ J ∖ X = ⋃ J ∖ X
8 2 7 eqtr4d ⊢ Z = ⋃ J ∖ X ∧ Y ∈ Clsd ⁡ J → Z = ⋃ Clsd ⁡ J ∖ X
9 opndisj ⊢ Z = ⋃ Clsd ⁡ J ∖ X → Y ∈ Clsd ⁡ J ∩ 𝒫 Z ↔ Y ∈ Clsd ⁡ J ∧ X ∩ Y = ∅
10 1 9 bitr3id ⊢ Z = ⋃ Clsd ⁡ J ∖ X → Y ∈ Clsd ⁡ J ∧ Y ∈ 𝒫 Z ↔ Y ∈ Clsd ⁡ J ∧ X ∩ Y = ∅
11 10 pm5.32dar ⊢ Z = ⋃ Clsd ⁡ J ∖ X ∧ Y ∈ Clsd ⁡ J → Y ∈ 𝒫 Z ↔ X ∩ Y = ∅
12 8 11 sylancom ⊢ Z = ⋃ J ∖ X ∧ Y ∈ Clsd ⁡ J → Y ∈ 𝒫 Z ↔ X ∩ Y = ∅
13 12 pm5.32da ⊢ Z = ⋃ J ∖ X → Y ∈ Clsd ⁡ J ∧ Y ∈ 𝒫 Z ↔ Y ∈ Clsd ⁡ J ∧ X ∩ Y = ∅
14 1 13 bitrid ⊢ Z = ⋃ J ∖ X → Y ∈ Clsd ⁡ J ∩ 𝒫 Z ↔ Y ∈ Clsd ⁡ J ∧ X ∩ Y = ∅