Theorem ntrclsnvobr

Description: If (pseudo-)interior and (pseudo-)closure functions are related by the duality operator then they are related the opposite way. (Contributed by RP, 21-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$$
Assertion	ntrclsnvobr	$$⊢\phi \to KDI$$

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	2 3	ntrclsbex	$$⊢\phi \to B\in \mathrm{V}$$
5	1 2 4	dssmapnvod	$$⊢\phi \to D^{-1}=D$$
6	1 2 3	ntrclsf1o	$$⊢\phi \to D:{𝒫B}^{𝒫B}\underset{1-1\; onto}{⟶}{𝒫B}^{𝒫B}$$
7		f1orel	$$⊢D:{𝒫B}^{𝒫B}\underset{1-1\; onto}{⟶}{𝒫B}^{𝒫B}\to \mathrm{Rel}D$$
8		relbrcnvg	$$⊢\mathrm{Rel}D\to \left(K{D}^{-1}I\leftrightarrow IDK\right)$$
9	6 7 8	3syl	$$⊢\phi \to \left(K{D}^{-1}I\leftrightarrow IDK\right)$$
10	3 9	mpbird	$$⊢\phi \to K{D}^{-1}I$$
11	5 10	breqdi	$$⊢\phi \to KDI$$