Theorem ntrclselnel2

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

	Ref	Expression
Hypotheses	ntrcls.o	$$⊢O=\left(i\in \mathrm{V}⟼\left(k\in \left({𝒫i}^{𝒫i}\right)⟼\left(j\in 𝒫i⟼i\setminus k\left(i\setminus j\right)\right)\right)\right)$$
	ntrcls.d	$$⊢D=O\left(B\right)$$
	ntrcls.r	$$⊢\phi \to IDK$$
	ntrcls.x	$$⊢\phi \to X\in B$$
	ntrcls.s	$$⊢\phi \to S\in 𝒫B$$
Assertion	ntrclselnel2	$$⊢\phi \to \left(X\in I\left(B\setminus S\right)\leftrightarrow \neg X\in K\left(S\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		ntrcls.o	$$⊢O=\left(i\in \mathrm{V}⟼\left(k\in \left({𝒫i}^{𝒫i}\right)⟼\left(j\in 𝒫i⟼i\setminus k\left(i\setminus j\right)\right)\right)\right)$$
2		ntrcls.d	$$⊢D=O\left(B\right)$$
3		ntrcls.r	$$⊢\phi \to IDK$$
4		ntrcls.x	$$⊢\phi \to X\in B$$
5		ntrcls.s	$$⊢\phi \to S\in 𝒫B$$
6	1 2 3	ntrclsnvobr	$$⊢\phi \to KDI$$
7	1 2 6 4 5	ntrclselnel1	$$⊢\phi \to \left(X\in K\left(S\right)\leftrightarrow \neg X\in I\left(B\setminus S\right)\right)$$
8	7	con2bid	$$⊢\phi \to \left(X\in I\left(B\setminus S\right)\leftrightarrow \neg X\in K\left(S\right)\right)$$