Description: If (pseudo-)interior and (pseudo-)closure functions are related by the duality operator we may characterize the relation as part of a 1-to-1 onto function. (Contributed by RP, 29-May-2021)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | ntrcls.o | |- O = ( i e. _V |-> ( k e. ( ~P i ^m ~P i ) |-> ( j e. ~P i |-> ( i \ ( k ` ( i \ j ) ) ) ) ) ) |
|
| ntrcls.d | |- D = ( O ` B ) |
||
| ntrcls.r | |- ( ph -> I D K ) |
||
| Assertion | ntrclsf1o | |- ( ph -> D : ( ~P B ^m ~P B ) -1-1-onto-> ( ~P B ^m ~P B ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | ntrcls.o | |- O = ( i e. _V |-> ( k e. ( ~P i ^m ~P i ) |-> ( j e. ~P i |-> ( i \ ( k ` ( i \ j ) ) ) ) ) ) |
|
| 2 | ntrcls.d | |- D = ( O ` B ) |
|
| 3 | ntrcls.r | |- ( ph -> I D K ) |
|
| 4 | 2 3 | ntrclsbex | |- ( ph -> B e. _V ) |
| 5 | 1 2 4 | dssmapf1od | |- ( ph -> D : ( ~P B ^m ~P B ) -1-1-onto-> ( ~P B ^m ~P B ) ) |