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 ) ) |
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 ) ) |