Theorem ntrclsf1o

Description: If (pseudo-)interior and (pseudo-)closure functions are related by the duality operator we may characterize the relation as part of a 1-to-1 onto function. (Contributed by RP, 29-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	ntrclsf1o	$$⊢\phi \to D:{𝒫B}^{𝒫B}\underset{1-1\; onto}{⟶}{𝒫B}^{𝒫B}$$

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	dssmapf1od	$$⊢\phi \to D:{𝒫B}^{𝒫B}\underset{1-1\; onto}{⟶}{𝒫B}^{𝒫B}$$