Theorem opncldbid

Description: Conditions on open sets are equivalent to conditions on closed sets. (Contributed by Zhi Wang, 30-Aug-2024)

	Ref	Expression
Hypotheses	opncldbid.1	$$⊢\phi \to J\in \mathrm{Top}$$
	opncldbid.2	$$⊢\left(\phi \wedge x=\bigcup J\setminus y\right)\to \left(\psi \leftrightarrow \chi \right)$$
Assertion	opncldbid	$$⊢\phi \to \left(\forall x\in J\psi \leftrightarrow \forall y\in \mathrm{Clsd}\left(J\right)\chi \right)$$

Proof

Step	Hyp	Ref	Expression
1		opncldbid.1	$$⊢\phi \to J\in \mathrm{Top}$$
2		opncldbid.2	$$⊢\left(\phi \wedge x=\bigcup J\setminus y\right)\to \left(\psi \leftrightarrow \chi \right)$$
3		eqid	$$⊢\bigcup J=\bigcup J$$
4	3	cldopn	$$⊢y\in \mathrm{Clsd}\left(J\right)\to \bigcup J\setminus y\in J$$
5	4	adantl	$$⊢\left(\phi \wedge y\in \mathrm{Clsd}\left(J\right)\right)\to \bigcup J\setminus y\in J$$
6	3	opncld	$$⊢\left(J\in \mathrm{Top}\wedge x\in J\right)\to \bigcup J\setminus x\in \mathrm{Clsd}\left(J\right)$$
7		elssuni	$$⊢x\in J\to x\subseteq \bigcup J$$
8		dfss4	$$⊢x\subseteq \bigcup J\leftrightarrow \bigcup J\setminus \left(\bigcup J\setminus x\right)=x$$
9	7 8	sylib	$$⊢x\in J\to \bigcup J\setminus \left(\bigcup J\setminus x\right)=x$$
10	9	eqcomd	$$⊢x\in J\to x=\bigcup J\setminus \left(\bigcup J\setminus x\right)$$
11	10	adantl	$$⊢\left(J\in \mathrm{Top}\wedge x\in J\right)\to x=\bigcup J\setminus \left(\bigcup J\setminus x\right)$$
12	6 11	jca	$$⊢\left(J\in \mathrm{Top}\wedge x\in J\right)\to \left(\bigcup J\setminus x\in \mathrm{Clsd}\left(J\right)\wedge x=\bigcup J\setminus \left(\bigcup J\setminus x\right)\right)$$
13		eleq1	$$⊢y=\bigcup J\setminus x\to \left(y\in \mathrm{Clsd}\left(J\right)\leftrightarrow \bigcup J\setminus x\in \mathrm{Clsd}\left(J\right)\right)$$
14		difeq2	$$⊢y=\bigcup J\setminus x\to \bigcup J\setminus y=\bigcup J\setminus \left(\bigcup J\setminus x\right)$$
15	14	eqeq2d	$$⊢y=\bigcup J\setminus x\to \left(x=\bigcup J\setminus y\leftrightarrow x=\bigcup J\setminus \left(\bigcup J\setminus x\right)\right)$$
16	13 15	anbi12d	$$⊢y=\bigcup J\setminus x\to \left(\left(y\in \mathrm{Clsd}\left(J\right)\wedge x=\bigcup J\setminus y\right)\leftrightarrow \left(\bigcup J\setminus x\in \mathrm{Clsd}\left(J\right)\wedge x=\bigcup J\setminus \left(\bigcup J\setminus x\right)\right)\right)$$
17	6 12 16	spcedv	$$⊢\left(J\in \mathrm{Top}\wedge x\in J\right)\to \exists y\left(y\in \mathrm{Clsd}\left(J\right)\wedge x=\bigcup J\setminus y\right)$$
18		df-rex	$$⊢\exists y\in \mathrm{Clsd}\left(J\right)x=\bigcup J\setminus y\leftrightarrow \exists y\left(y\in \mathrm{Clsd}\left(J\right)\wedge x=\bigcup J\setminus y\right)$$
19	17 18	sylibr	$$⊢\left(J\in \mathrm{Top}\wedge x\in J\right)\to \exists y\in \mathrm{Clsd}\left(J\right)x=\bigcup J\setminus y$$
20	1 19	sylan	$$⊢\left(\phi \wedge x\in J\right)\to \exists y\in \mathrm{Clsd}\left(J\right)x=\bigcup J\setminus y$$
21	5 20 2	ralxfrd	$$⊢\phi \to \left(\forall x\in J\psi \leftrightarrow \forall y\in \mathrm{Clsd}\left(J\right)\chi \right)$$