Theorem opndisj

Description: Two ways of saying that two open sets are disjoint, if J is a topology and X is an open set. (Contributed by Zhi Wang, 6-Sep-2024)

	Ref	Expression
Assertion	opndisj	$$⊢Z=\bigcup J\setminus X\to \left(Y\in \left(J\cap 𝒫Z\right)\leftrightarrow \left(Y\in J\wedge X\cap Y=\varnothing \right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		elpwg	$$⊢Y\in J\to \left(Y\in 𝒫Z\leftrightarrow Y\subseteq Z\right)$$
2		sseq2	$$⊢Z=\bigcup J\setminus X\to \left(Y\subseteq Z\leftrightarrow Y\subseteq \bigcup J\setminus X\right)$$
3	1 2	sylan9bbr	$$⊢\left(Z=\bigcup J\setminus X\wedge Y\in J\right)\to \left(Y\in 𝒫Z\leftrightarrow Y\subseteq \bigcup J\setminus X\right)$$
4	3	pm5.32da	$$⊢Z=\bigcup J\setminus X\to \left(\left(Y\in J\wedge Y\in 𝒫Z\right)\leftrightarrow \left(Y\in J\wedge Y\subseteq \bigcup J\setminus X\right)\right)$$
5		elin	$$⊢Y\in \left(J\cap 𝒫Z\right)\leftrightarrow \left(Y\in J\wedge Y\in 𝒫Z\right)$$
6		elssuni	$$⊢Y\in J\to Y\subseteq \bigcup J$$
7		incom	$$⊢X\cap Y=Y\cap X$$
8	7	eqeq1i	$$⊢X\cap Y=\varnothing \leftrightarrow Y\cap X=\varnothing$$
9		reldisj	$$⊢Y\subseteq \bigcup J\to \left(Y\cap X=\varnothing \leftrightarrow Y\subseteq \bigcup J\setminus X\right)$$
10	8 9	bitrid	$$⊢Y\subseteq \bigcup J\to \left(X\cap Y=\varnothing \leftrightarrow Y\subseteq \bigcup J\setminus X\right)$$
11	6 10	syl	$$⊢Y\in J\to \left(X\cap Y=\varnothing \leftrightarrow Y\subseteq \bigcup J\setminus X\right)$$
12	11	pm5.32i	$$⊢\left(Y\in J\wedge X\cap Y=\varnothing \right)\leftrightarrow \left(Y\in J\wedge Y\subseteq \bigcup J\setminus X\right)$$
13	4 5 12	3bitr4g	$$⊢Z=\bigcup J\setminus X\to \left(Y\in \left(J\cap 𝒫Z\right)\leftrightarrow \left(Y\in J\wedge X\cap Y=\varnothing \right)\right)$$