Description: If (pseudo-)interior and (pseudo-)neighborhood functions are related by the operator, F , we may characterize the relation as part of a 1-to-1 onto function. (Contributed by RP, 29-May-2021)
Ref | Expression | ||
---|---|---|---|
Hypotheses | ntrnei.o | |- O = ( i e. _V , j e. _V |-> ( k e. ( ~P j ^m i ) |-> ( l e. j |-> { m e. i | l e. ( k ` m ) } ) ) ) |
|
ntrnei.f | |- F = ( ~P B O B ) |
||
ntrnei.r | |- ( ph -> I F N ) |
||
Assertion | ntrneif1o | |- ( ph -> F : ( ~P B ^m ~P B ) -1-1-onto-> ( ~P ~P B ^m B ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ntrnei.o | |- O = ( i e. _V , j e. _V |-> ( k e. ( ~P j ^m i ) |-> ( l e. j |-> { m e. i | l e. ( k ` m ) } ) ) ) |
|
2 | ntrnei.f | |- F = ( ~P B O B ) |
|
3 | ntrnei.r | |- ( ph -> I F N ) |
|
4 | 1 2 3 | ntrneibex | |- ( ph -> B e. _V ) |
5 | 4 | pwexd | |- ( ph -> ~P B e. _V ) |
6 | 1 5 4 2 | fsovf1od | |- ( ph -> F : ( ~P B ^m ~P B ) -1-1-onto-> ( ~P ~P B ^m B ) ) |