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

Proof

Step	Hyp	Ref	Expression
1		ntrrn.x	|- X = U. J
2		ntrrn.i	|- I = ( int ` J )
3	1 2	ntrf	|- ( J e. Top -> I : ~P X --> J )
4	1	toptopon	|- ( J e. Top <-> J e. ( TopOn ` X ) )
5		topgele	|- ( J e. ( TopOn ` X ) -> ( { (/) , X } C_ J /\ J C_ ~P X ) )
6	4 5	sylbi	|- ( J e. Top -> ( { (/) , X } C_ J /\ J C_ ~P X ) )
7	6	simprd	|- ( J e. Top -> J C_ ~P X )
8	3 7	fssd	|- ( J e. Top -> I : ~P X --> ~P X )