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	⊢ ( 𝜑 → 𝐽 ∈ Top )
	opncldeqv.2	⊢ ( ( 𝜑 ∧ 𝑥 = ( ∪ 𝐽 ∖ 𝑦 ) ) → ( 𝜓 ↔ 𝜒 ) )
Assertion	opncldeqv	⊢ ( 𝜑 → ( ∀ 𝑥 ∈ 𝐽 𝜓 ↔ ∀ 𝑦 ∈ ( Clsd ‘ 𝐽 ) 𝜒 ) )

Proof

Step	Hyp	Ref	Expression
1		opncldeqv.1	⊢ ( 𝜑 → 𝐽 ∈ Top )
2		opncldeqv.2	⊢ ( ( 𝜑 ∧ 𝑥 = ( ∪ 𝐽 ∖ 𝑦 ) ) → ( 𝜓 ↔ 𝜒 ) )
3		eqid	⊢ ∪ 𝐽 = ∪ 𝐽
4	3	cldopn	⊢ ( 𝑦 ∈ ( Clsd ‘ 𝐽 ) → ( ∪ 𝐽 ∖ 𝑦 ) ∈ 𝐽 )
5	4	adantl	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( Clsd ‘ 𝐽 ) ) → ( ∪ 𝐽 ∖ 𝑦 ) ∈ 𝐽 )
6	3	opncld	⊢ ( ( 𝐽 ∈ Top ∧ 𝑥 ∈ 𝐽 ) → ( ∪ 𝐽 ∖ 𝑥 ) ∈ ( Clsd ‘ 𝐽 ) )
7		elssuni	⊢ ( 𝑥 ∈ 𝐽 → 𝑥 ⊆ ∪ 𝐽 )
8		dfss4	⊢ ( 𝑥 ⊆ ∪ 𝐽 ↔ ( ∪ 𝐽 ∖ ( ∪ 𝐽 ∖ 𝑥 ) ) = 𝑥 )
9	7 8	sylib	⊢ ( 𝑥 ∈ 𝐽 → ( ∪ 𝐽 ∖ ( ∪ 𝐽 ∖ 𝑥 ) ) = 𝑥 )
10	9	eqcomd	⊢ ( 𝑥 ∈ 𝐽 → 𝑥 = ( ∪ 𝐽 ∖ ( ∪ 𝐽 ∖ 𝑥 ) ) )
11	10	adantl	⊢ ( ( 𝐽 ∈ Top ∧ 𝑥 ∈ 𝐽 ) → 𝑥 = ( ∪ 𝐽 ∖ ( ∪ 𝐽 ∖ 𝑥 ) ) )
12	6 11	jca	⊢ ( ( 𝐽 ∈ Top ∧ 𝑥 ∈ 𝐽 ) → ( ( ∪ 𝐽 ∖ 𝑥 ) ∈ ( Clsd ‘ 𝐽 ) ∧ 𝑥 = ( ∪ 𝐽 ∖ ( ∪ 𝐽 ∖ 𝑥 ) ) ) )
13		eleq1	⊢ ( 𝑦 = ( ∪ 𝐽 ∖ 𝑥 ) → ( 𝑦 ∈ ( Clsd ‘ 𝐽 ) ↔ ( ∪ 𝐽 ∖ 𝑥 ) ∈ ( Clsd ‘ 𝐽 ) ) )
14		difeq2	⊢ ( 𝑦 = ( ∪ 𝐽 ∖ 𝑥 ) → ( ∪ 𝐽 ∖ 𝑦 ) = ( ∪ 𝐽 ∖ ( ∪ 𝐽 ∖ 𝑥 ) ) )
15	14	eqeq2d	⊢ ( 𝑦 = ( ∪ 𝐽 ∖ 𝑥 ) → ( 𝑥 = ( ∪ 𝐽 ∖ 𝑦 ) ↔ 𝑥 = ( ∪ 𝐽 ∖ ( ∪ 𝐽 ∖ 𝑥 ) ) ) )
16	13 15	anbi12d	⊢ ( 𝑦 = ( ∪ 𝐽 ∖ 𝑥 ) → ( ( 𝑦 ∈ ( Clsd ‘ 𝐽 ) ∧ 𝑥 = ( ∪ 𝐽 ∖ 𝑦 ) ) ↔ ( ( ∪ 𝐽 ∖ 𝑥 ) ∈ ( Clsd ‘ 𝐽 ) ∧ 𝑥 = ( ∪ 𝐽 ∖ ( ∪ 𝐽 ∖ 𝑥 ) ) ) ) )
17	6 12 16	spcedv	⊢ ( ( 𝐽 ∈ Top ∧ 𝑥 ∈ 𝐽 ) → ∃ 𝑦 ( 𝑦 ∈ ( Clsd ‘ 𝐽 ) ∧ 𝑥 = ( ∪ 𝐽 ∖ 𝑦 ) ) )
18		df-rex	⊢ ( ∃ 𝑦 ∈ ( Clsd ‘ 𝐽 ) 𝑥 = ( ∪ 𝐽 ∖ 𝑦 ) ↔ ∃ 𝑦 ( 𝑦 ∈ ( Clsd ‘ 𝐽 ) ∧ 𝑥 = ( ∪ 𝐽 ∖ 𝑦 ) ) )
19	17 18	sylibr	⊢ ( ( 𝐽 ∈ Top ∧ 𝑥 ∈ 𝐽 ) → ∃ 𝑦 ∈ ( Clsd ‘ 𝐽 ) 𝑥 = ( ∪ 𝐽 ∖ 𝑦 ) )
20	1 19	sylan	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐽 ) → ∃ 𝑦 ∈ ( Clsd ‘ 𝐽 ) 𝑥 = ( ∪ 𝐽 ∖ 𝑦 ) )
21	5 20 2	ralxfrd	⊢ ( 𝜑 → ( ∀ 𝑥 ∈ 𝐽 𝜓 ↔ ∀ 𝑦 ∈ ( Clsd ‘ 𝐽 ) 𝜒 ) )