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 \to (Y \in (Clsd (J) \cap 𝒫 Z) \leftrightarrow (Y \in Clsd (J) \land X \cap Y = \emptyset))$

Proof

Step	Hyp	Ref	Expression
1		elin	$⊢ Y \in (Clsd (J) \cap 𝒫 Z) \leftrightarrow (Y \in Clsd (J) \land Y \in 𝒫 Z)$
2		simpl	$⊢ (Z = ⋃ J ∖ X \land Y \in Clsd (J)) \to Z = ⋃ J ∖ X$
3		cldrcl	$⊢ Y \in Clsd (J) \to J \in Top$
4		clduni	$⊢ J \in Top \to ⋃ Clsd (J) = ⋃ J$
5	4	difeq1d	$⊢ J \in Top \to ⋃ Clsd (J) ∖ X = ⋃ J ∖ X$
6	3 5	syl	$⊢ Y \in Clsd (J) \to ⋃ Clsd (J) ∖ X = ⋃ J ∖ X$
7	6	adantl	$⊢ (Z = ⋃ J ∖ X \land Y \in Clsd (J)) \to ⋃ Clsd (J) ∖ X = ⋃ J ∖ X$
8	2 7	eqtr4d	$⊢ (Z = ⋃ J ∖ X \land Y \in Clsd (J)) \to Z = ⋃ Clsd (J) ∖ X$
9		opndisj	$⊢ Z = ⋃ Clsd (J) ∖ X \to (Y \in (Clsd (J) \cap 𝒫 Z) \leftrightarrow (Y \in Clsd (J) \land X \cap Y = \emptyset))$
10	1 9	bitr3id	$⊢ Z = ⋃ Clsd (J) ∖ X \to ((Y \in Clsd (J) \land Y \in 𝒫 Z) \leftrightarrow (Y \in Clsd (J) \land X \cap Y = \emptyset))$
11	10	pm5.32dra	$⊢ (Z = ⋃ Clsd (J) ∖ X \land Y \in Clsd (J)) \to (Y \in 𝒫 Z \leftrightarrow X \cap Y = \emptyset)$
12	8 11	sylancom	$⊢ (Z = ⋃ J ∖ X \land Y \in Clsd (J)) \to (Y \in 𝒫 Z \leftrightarrow X \cap Y = \emptyset)$
13	12	pm5.32da	$⊢ Z = ⋃ J ∖ X \to ((Y \in Clsd (J) \land Y \in 𝒫 Z) \leftrightarrow (Y \in Clsd (J) \land X \cap Y = \emptyset))$
14	1 13	bitrid	$⊢ Z = ⋃ J ∖ X \to (Y \in (Clsd (J) \cap 𝒫 Z) \leftrightarrow (Y \in Clsd (J) \land X \cap Y = \emptyset))$

Metamath Proof Explorer

Theorem clddisj

Proof