Theorem ntrf2

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	ntrf2	$$⊢J\in \mathrm{Top}\to I:𝒫X⟶𝒫X$$

Proof

Step	Hyp	Ref	Expression
1		ntrrn.x	$$⊢X=\bigcup J$$
2		ntrrn.i	$$⊢I=\mathrm{int}\left(J\right)$$
3	1 2	ntrf	$$⊢J\in \mathrm{Top}\to I:𝒫X⟶J$$
4	1	toptopon	$$⊢J\in \mathrm{Top}\leftrightarrow J\in \mathrm{TopOn}\left(X\right)$$
5		topgele	$$⊢J\in \mathrm{TopOn}\left(X\right)\to \left(\left\{\varnothing ,X\right\}\subseteq J\wedge J\subseteq 𝒫X\right)$$
6	4 5	sylbi	$$⊢J\in \mathrm{Top}\to \left(\left\{\varnothing ,X\right\}\subseteq J\wedge J\subseteq 𝒫X\right)$$
7	6	simprd	$$⊢J\in \mathrm{Top}\to J\subseteq 𝒫X$$
8	3 7	fssd	$$⊢J\in \mathrm{Top}\to I:𝒫X⟶𝒫X$$