Theorem ntrclsiex

Description: If (pseudo-)interior and (pseudo-)closure functions are related by the duality operator then those functions are maps of subsets to subsets. (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	ntrclsiex	$$⊢\phi \to I\in \left({𝒫B}^{𝒫B}\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	1 2 3	ntrclsf1o	$$⊢\phi \to D:{𝒫B}^{𝒫B}\underset{1-1\; onto}{⟶}{𝒫B}^{𝒫B}$$
5		f1orel	$$⊢D:{𝒫B}^{𝒫B}\underset{1-1\; onto}{⟶}{𝒫B}^{𝒫B}\to \mathrm{Rel}D$$
6	4 5	syl	$$⊢\phi \to \mathrm{Rel}D$$
7		releldm	$$⊢\left(\mathrm{Rel}D\wedge IDK\right)\to I\in \mathrm{dom}D$$
8	6 3 7	syl2anc	$$⊢\phi \to I\in \mathrm{dom}D$$
9		f1odm	$$⊢D:{𝒫B}^{𝒫B}\underset{1-1\; onto}{⟶}{𝒫B}^{𝒫B}\to \mathrm{dom}D={𝒫B}^{𝒫B}$$
10	4 9	syl	$$⊢\phi \to \mathrm{dom}D={𝒫B}^{𝒫B}$$
11	8 10	eleqtrd	$$⊢\phi \to I\in \left({𝒫B}^{𝒫B}\right)$$