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 = U. J
	ntrrn.i	|- I = ( int ` J )
Assertion	ntrf	|- ( J e. Top -> I : ~P X --> J )

Proof

Step	Hyp	Ref	Expression
1		ntrrn.x	|- X = U. J
2		ntrrn.i	|- I = ( int ` J )
3		vpwex	|- ~P s e. _V
4	3	inex2	|- ( J i^i ~P s ) e. _V
5	4	uniex	|- U. ( J i^i ~P s ) e. _V
6		eqid	|- ( s e. ~P X |-> U. ( J i^i ~P s ) ) = ( s e. ~P X |-> U. ( J i^i ~P s ) )
7	5 6	fnmpti	|- ( s e. ~P X |-> U. ( J i^i ~P s ) ) Fn ~P X
8	1	ntrfval	|- ( J e. Top -> ( int ` J ) = ( s e. ~P X |-> U. ( J i^i ~P s ) ) )
9	2 8	syl5eq	|- ( J e. Top -> I = ( s e. ~P X |-> U. ( J i^i ~P s ) ) )
10	9	fneq1d	|- ( J e. Top -> ( I Fn ~P X <-> ( s e. ~P X |-> U. ( J i^i ~P s ) ) Fn ~P X ) )
11	7 10	mpbiri	|- ( J e. Top -> I Fn ~P X )
12	1 2	ntrrn	|- ( J e. Top -> ran I C_ J )
13		df-f	|- ( I : ~P X --> J <-> ( I Fn ~P X /\ ran I C_ J ) )
14	11 12 13	sylanbrc	|- ( J e. Top -> I : ~P X --> J )