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 ( 𝑍 = ( ∪ 𝐽 ∖ 𝑋 ) → ( 𝑌 ∈ ( ( Clsd ‘ 𝐽 ) ∩ 𝒫 𝑍 ) ↔ ( 𝑌 ∈ ( Clsd ‘ 𝐽 ) ∧ ( 𝑋 ∩ 𝑌 ) = ∅ ) ) )

Proof

Step Hyp Ref Expression
1 elin ⊢ ( 𝑌 ∈ ( ( Clsd ‘ 𝐽 ) ∩ 𝒫 𝑍 ) ↔ ( 𝑌 ∈ ( Clsd ‘ 𝐽 ) ∧ 𝑌 ∈ 𝒫 𝑍 ) )
2 simpl ⊢ ( ( 𝑍 = ( ∪ 𝐽 ∖ 𝑋 ) ∧ 𝑌 ∈ ( Clsd ‘ 𝐽 ) ) → 𝑍 = ( ∪ 𝐽 ∖ 𝑋 ) )
3 cldrcl ⊢ ( 𝑌 ∈ ( Clsd ‘ 𝐽 ) → 𝐽 ∈ Top )
4 clduni ⊢ ( 𝐽 ∈ Top → ∪ ( Clsd ‘ 𝐽 ) = ∪ 𝐽 )
5 4 difeq1d ⊢ ( 𝐽 ∈ Top → ( ∪ ( Clsd ‘ 𝐽 ) ∖ 𝑋 ) = ( ∪ 𝐽 ∖ 𝑋 ) )
6 3 5 syl ⊢ ( 𝑌 ∈ ( Clsd ‘ 𝐽 ) → ( ∪ ( Clsd ‘ 𝐽 ) ∖ 𝑋 ) = ( ∪ 𝐽 ∖ 𝑋 ) )
7 6 adantl ⊢ ( ( 𝑍 = ( ∪ 𝐽 ∖ 𝑋 ) ∧ 𝑌 ∈ ( Clsd ‘ 𝐽 ) ) → ( ∪ ( Clsd ‘ 𝐽 ) ∖ 𝑋 ) = ( ∪ 𝐽 ∖ 𝑋 ) )
8 2 7 eqtr4d ⊢ ( ( 𝑍 = ( ∪ 𝐽 ∖ 𝑋 ) ∧ 𝑌 ∈ ( Clsd ‘ 𝐽 ) ) → 𝑍 = ( ∪ ( Clsd ‘ 𝐽 ) ∖ 𝑋 ) )
9 opndisj ⊢ ( 𝑍 = ( ∪ ( Clsd ‘ 𝐽 ) ∖ 𝑋 ) → ( 𝑌 ∈ ( ( Clsd ‘ 𝐽 ) ∩ 𝒫 𝑍 ) ↔ ( 𝑌 ∈ ( Clsd ‘ 𝐽 ) ∧ ( 𝑋 ∩ 𝑌 ) = ∅ ) ) )
10 1 9 bitr3id ⊢ ( 𝑍 = ( ∪ ( Clsd ‘ 𝐽 ) ∖ 𝑋 ) → ( ( 𝑌 ∈ ( Clsd ‘ 𝐽 ) ∧ 𝑌 ∈ 𝒫 𝑍 ) ↔ ( 𝑌 ∈ ( Clsd ‘ 𝐽 ) ∧ ( 𝑋 ∩ 𝑌 ) = ∅ ) ) )
11 10 pm5.32dra ⊢ ( ( 𝑍 = ( ∪ ( Clsd ‘ 𝐽 ) ∖ 𝑋 ) ∧ 𝑌 ∈ ( Clsd ‘ 𝐽 ) ) → ( 𝑌 ∈ 𝒫 𝑍 ↔ ( 𝑋 ∩ 𝑌 ) = ∅ ) )
12 8 11 sylancom ⊢ ( ( 𝑍 = ( ∪ 𝐽 ∖ 𝑋 ) ∧ 𝑌 ∈ ( Clsd ‘ 𝐽 ) ) → ( 𝑌 ∈ 𝒫 𝑍 ↔ ( 𝑋 ∩ 𝑌 ) = ∅ ) )
13 12 pm5.32da ⊢ ( 𝑍 = ( ∪ 𝐽 ∖ 𝑋 ) → ( ( 𝑌 ∈ ( Clsd ‘ 𝐽 ) ∧ 𝑌 ∈ 𝒫 𝑍 ) ↔ ( 𝑌 ∈ ( Clsd ‘ 𝐽 ) ∧ ( 𝑋 ∩ 𝑌 ) = ∅ ) ) )
14 1 13 bitrid ⊢ ( 𝑍 = ( ∪ 𝐽 ∖ 𝑋 ) → ( 𝑌 ∈ ( ( Clsd ‘ 𝐽 ) ∩ 𝒫 𝑍 ) ↔ ( 𝑌 ∈ ( Clsd ‘ 𝐽 ) ∧ ( 𝑋 ∩ 𝑌 ) = ∅ ) ) )