Theorem opncldeqv

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

	Ref	Expression
Hypotheses	opncldeqv.1	|- ( ph -> J e. Top )
	opncldeqv.2	|- ( ( ph /\ x = ( U. J \ y ) ) -> ( ps <-> ch ) )
Assertion	opncldeqv	|- ( ph -> ( A. x e. J ps <-> A. y e. ( Clsd ` J ) ch ) )

Proof

Step	Hyp	Ref	Expression
1		opncldeqv.1	|- ( ph -> J e. Top )
2		opncldeqv.2	|- ( ( ph /\ x = ( U. J \ y ) ) -> ( ps <-> ch ) )
3		eqid	|- U. J = U. J
4	3	cldopn	|- ( y e. ( Clsd ` J ) -> ( U. J \ y ) e. J )
5	4	adantl	|- ( ( ph /\ y e. ( Clsd ` J ) ) -> ( U. J \ y ) e. J )
6	3	opncld	|- ( ( J e. Top /\ x e. J ) -> ( U. J \ x ) e. ( Clsd ` J ) )
7		elssuni	|- ( x e. J -> x C_ U. J )
8		dfss4	|- ( x C_ U. J <-> ( U. J \ ( U. J \ x ) ) = x )
9	7 8	sylib	|- ( x e. J -> ( U. J \ ( U. J \ x ) ) = x )
10	9	eqcomd	|- ( x e. J -> x = ( U. J \ ( U. J \ x ) ) )
11	10	adantl	|- ( ( J e. Top /\ x e. J ) -> x = ( U. J \ ( U. J \ x ) ) )
12	6 11	jca	|- ( ( J e. Top /\ x e. J ) -> ( ( U. J \ x ) e. ( Clsd ` J ) /\ x = ( U. J \ ( U. J \ x ) ) ) )
13		eleq1	|- ( y = ( U. J \ x ) -> ( y e. ( Clsd ` J ) <-> ( U. J \ x ) e. ( Clsd ` J ) ) )
14		difeq2	|- ( y = ( U. J \ x ) -> ( U. J \ y ) = ( U. J \ ( U. J \ x ) ) )
15	14	eqeq2d	|- ( y = ( U. J \ x ) -> ( x = ( U. J \ y ) <-> x = ( U. J \ ( U. J \ x ) ) ) )
16	13 15	anbi12d	|- ( y = ( U. J \ x ) -> ( ( y e. ( Clsd ` J ) /\ x = ( U. J \ y ) ) <-> ( ( U. J \ x ) e. ( Clsd ` J ) /\ x = ( U. J \ ( U. J \ x ) ) ) ) )
17	6 12 16	spcedv	|- ( ( J e. Top /\ x e. J ) -> E. y ( y e. ( Clsd ` J ) /\ x = ( U. J \ y ) ) )
18		df-rex	|- ( E. y e. ( Clsd ` J ) x = ( U. J \ y ) <-> E. y ( y e. ( Clsd ` J ) /\ x = ( U. J \ y ) ) )
19	17 18	sylibr	|- ( ( J e. Top /\ x e. J ) -> E. y e. ( Clsd ` J ) x = ( U. J \ y ) )
20	1 19	sylan	|- ( ( ph /\ x e. J ) -> E. y e. ( Clsd ` J ) x = ( U. J \ y ) )
21	5 20 2	ralxfrd	|- ( ph -> ( A. x e. J ps <-> A. y e. ( Clsd ` J ) ch ) )