Theorem ntrelmap

Description: The interior function is a map from the powerset of the base set to itself. (Contributed by RP, 22-Apr-2021)

	Ref	Expression
Hypotheses	ntrrn.x	$$⊢X=\bigcup J$$
	ntrrn.i	$$⊢I=\mathrm{int}\left(J\right)$$
Assertion	ntrelmap	$$⊢J\in \mathrm{Top}\to I\in \left({𝒫X}^{𝒫X}\right)$$

Proof

Step	Hyp	Ref	Expression
1		ntrrn.x	$$⊢X=\bigcup J$$
2		ntrrn.i	$$⊢I=\mathrm{int}\left(J\right)$$
3	1 2	ntrf2	$$⊢J\in \mathrm{Top}\to I:𝒫X⟶𝒫X$$
4	1	topopn	$$⊢J\in \mathrm{Top}\to X\in J$$
5	4	pwexd	$$⊢J\in \mathrm{Top}\to 𝒫X\in \mathrm{V}$$
6	5 5	elmapd	$$⊢J\in \mathrm{Top}\to \left(I\in \left({𝒫X}^{𝒫X}\right)\leftrightarrow I:𝒫X⟶𝒫X\right)$$
7	3 6	mpbird	$$⊢J\in \mathrm{Top}\to I\in \left({𝒫X}^{𝒫X}\right)$$