Theorem ntrclselnel1

Description: If (pseudo-)interior and (pseudo-)closure functions are related by the duality operator then there is an equivalence between membership in the interior of a set and non-membership in the closure of the complement of the set. (Contributed by RP, 28-May-2021)

	Ref	Expression
Hypotheses	ntrcls.o	⊢ 𝑂 = ( 𝑖 ∈ V ↦ ( 𝑘 ∈ ( 𝒫 𝑖 ↑m 𝒫 𝑖 ) ↦ ( 𝑗 ∈ 𝒫 𝑖 ↦ ( 𝑖 ∖ ( 𝑘 ‘ ( 𝑖 ∖ 𝑗 ) ) ) ) ) )
	ntrcls.d	⊢ 𝐷 = ( 𝑂 ‘ 𝐵 )
	ntrcls.r	⊢ ( 𝜑 → 𝐼 𝐷 𝐾 )
	ntrcls.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
	ntrcls.s	⊢ ( 𝜑 → 𝑆 ∈ 𝒫 𝐵 )
Assertion	ntrclselnel1	⊢ ( 𝜑 → ( 𝑋 ∈ ( 𝐼 ‘ 𝑆 ) ↔ ¬ 𝑋 ∈ ( 𝐾 ‘ ( 𝐵 ∖ 𝑆 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		ntrcls.o	⊢ 𝑂 = ( 𝑖 ∈ V ↦ ( 𝑘 ∈ ( 𝒫 𝑖 ↑m 𝒫 𝑖 ) ↦ ( 𝑗 ∈ 𝒫 𝑖 ↦ ( 𝑖 ∖ ( 𝑘 ‘ ( 𝑖 ∖ 𝑗 ) ) ) ) ) )
2		ntrcls.d	⊢ 𝐷 = ( 𝑂 ‘ 𝐵 )
3		ntrcls.r	⊢ ( 𝜑 → 𝐼 𝐷 𝐾 )
4		ntrcls.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
5		ntrcls.s	⊢ ( 𝜑 → 𝑆 ∈ 𝒫 𝐵 )
6	1 2 3	ntrclsfv2	⊢ ( 𝜑 → ( 𝐷 ‘ 𝐾 ) = 𝐼 )
7	6	eqcomd	⊢ ( 𝜑 → 𝐼 = ( 𝐷 ‘ 𝐾 ) )
8	7	fveq1d	⊢ ( 𝜑 → ( 𝐼 ‘ 𝑆 ) = ( ( 𝐷 ‘ 𝐾 ) ‘ 𝑆 ) )
9	2 3	ntrclsbex	⊢ ( 𝜑 → 𝐵 ∈ V )
10	1 2 3	ntrclskex	⊢ ( 𝜑 → 𝐾 ∈ ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) )
11		eqid	⊢ ( 𝐷 ‘ 𝐾 ) = ( 𝐷 ‘ 𝐾 )
12		eqid	⊢ ( ( 𝐷 ‘ 𝐾 ) ‘ 𝑆 ) = ( ( 𝐷 ‘ 𝐾 ) ‘ 𝑆 )
13	1 2 9 10 11 5 12	dssmapfv3d	⊢ ( 𝜑 → ( ( 𝐷 ‘ 𝐾 ) ‘ 𝑆 ) = ( 𝐵 ∖ ( 𝐾 ‘ ( 𝐵 ∖ 𝑆 ) ) ) )
14	8 13	eqtrd	⊢ ( 𝜑 → ( 𝐼 ‘ 𝑆 ) = ( 𝐵 ∖ ( 𝐾 ‘ ( 𝐵 ∖ 𝑆 ) ) ) )
15	14	eleq2d	⊢ ( 𝜑 → ( 𝑋 ∈ ( 𝐼 ‘ 𝑆 ) ↔ 𝑋 ∈ ( 𝐵 ∖ ( 𝐾 ‘ ( 𝐵 ∖ 𝑆 ) ) ) ) )
16		eldif	⊢ ( 𝑋 ∈ ( 𝐵 ∖ ( 𝐾 ‘ ( 𝐵 ∖ 𝑆 ) ) ) ↔ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ∈ ( 𝐾 ‘ ( 𝐵 ∖ 𝑆 ) ) ) )
17	16	a1i	⊢ ( 𝜑 → ( 𝑋 ∈ ( 𝐵 ∖ ( 𝐾 ‘ ( 𝐵 ∖ 𝑆 ) ) ) ↔ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ∈ ( 𝐾 ‘ ( 𝐵 ∖ 𝑆 ) ) ) ) )
18	4 17	mpbirand	⊢ ( 𝜑 → ( 𝑋 ∈ ( 𝐵 ∖ ( 𝐾 ‘ ( 𝐵 ∖ 𝑆 ) ) ) ↔ ¬ 𝑋 ∈ ( 𝐾 ‘ ( 𝐵 ∖ 𝑆 ) ) ) )
19	15 18	bitrd	⊢ ( 𝜑 → ( 𝑋 ∈ ( 𝐼 ‘ 𝑆 ) ↔ ¬ 𝑋 ∈ ( 𝐾 ‘ ( 𝐵 ∖ 𝑆 ) ) ) )