Theorem ntrf

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

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

Proof

Step	Hyp	Ref	Expression
1		ntrrn.x	$$⊢X=\bigcup J$$
2		ntrrn.i	$$⊢I=\mathrm{int}\left(J\right)$$
3		vpwex	$$⊢𝒫s\in \mathrm{V}$$
4	3	inex2	$$⊢J\cap 𝒫s\in \mathrm{V}$$
5	4	uniex	$$⊢\bigcup \left(J\cap 𝒫s\right)\in \mathrm{V}$$
6		eqid	$$⊢\left(s\in 𝒫X⟼\bigcup \left(J\cap 𝒫s\right)\right)=\left(s\in 𝒫X⟼\bigcup \left(J\cap 𝒫s\right)\right)$$
7	5 6	fnmpti	$$⊢\left(s\in 𝒫X⟼\bigcup \left(J\cap 𝒫s\right)\right)Fn𝒫X$$
8	1	ntrfval	$$⊢J\in \mathrm{Top}\to \mathrm{int}\left(J\right)=\left(s\in 𝒫X⟼\bigcup \left(J\cap 𝒫s\right)\right)$$
9	2 8	syl5eq	$$⊢J\in \mathrm{Top}\to I=\left(s\in 𝒫X⟼\bigcup \left(J\cap 𝒫s\right)\right)$$
10	9	fneq1d	$$⊢J\in \mathrm{Top}\to \left(IFn𝒫X\leftrightarrow \left(s\in 𝒫X⟼\bigcup \left(J\cap 𝒫s\right)\right)Fn𝒫X\right)$$
11	7 10	mpbiri	$$⊢J\in \mathrm{Top}\to IFn𝒫X$$
12	1 2	ntrrn	$$⊢J\in \mathrm{Top}\to \mathrm{ran}I\subseteq J$$
13		df-f	$$⊢I:𝒫X⟶J\leftrightarrow \left(IFn𝒫X\wedge \mathrm{ran}I\subseteq J\right)$$
14	11 12 13	sylanbrc	$$⊢J\in \mathrm{Top}\to I:𝒫X⟶J$$