Theorem ntrneicnv

Description: If (pseudo-)interior and (pseudo-)neighborhood functions are related by the operator, F , then converse of F is known. (Contributed by RP, 29-May-2021)

	Ref	Expression
Hypotheses	ntrnei.o	$$⊢O=\left(i\in \mathrm{V},j\in \mathrm{V}⟼\left(k\in \left({𝒫j}^i\right)⟼\left(l\in j⟼\left\{m\in i|l\in k\left(m\right)\right\}\right)\right)\right)$$
	ntrnei.f	$$⊢F=𝒫BOB$$
	ntrnei.r	$$⊢\phi \to IFN$$
Assertion	ntrneicnv	$$⊢\phi \to F^{-1}=BO𝒫B$$

Proof

Step	Hyp	Ref	Expression
1		ntrnei.o	$$⊢O=\left(i\in \mathrm{V},j\in \mathrm{V}⟼\left(k\in \left({𝒫j}^i\right)⟼\left(l\in j⟼\left\{m\in i|l\in k\left(m\right)\right\}\right)\right)\right)$$
2		ntrnei.f	$$⊢F=𝒫BOB$$
3		ntrnei.r	$$⊢\phi \to IFN$$
4	1 2 3	ntrneibex	$$⊢\phi \to B\in \mathrm{V}$$
5	4	pwexd	$$⊢\phi \to 𝒫B\in \mathrm{V}$$
6		eqid	$$⊢BO𝒫B=BO𝒫B$$
7	1 5 4 2 6	fsovcnvd	$$⊢\phi \to F^{-1}=BO𝒫B$$