Metamath Proof Explorer


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

Proof

Step Hyp Ref Expression
1 ntrrn.x
 |-  X = U. J
2 ntrrn.i
 |-  I = ( int ` J )
3 1 2 ntrf2
 |-  ( J e. Top -> I : ~P X --> ~P X )
4 1 topopn
 |-  ( J e. Top -> X e. J )
5 4 pwexd
 |-  ( J e. Top -> ~P X e. _V )
6 5 5 elmapd
 |-  ( J e. Top -> ( I e. ( ~P X ^m ~P X ) <-> I : ~P X --> ~P X ) )
7 3 6 mpbird
 |-  ( J e. Top -> I e. ( ~P X ^m ~P X ) )