Description: If (pseudo-)interior and (pseudo-)closure functions are related by the duality operator then the base set exists. (Contributed by RP, 21-May-2021)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | ntrclsbex.d | |- D = ( O ` B ) |
|
| ntrclsbex.r | |- ( ph -> I D K ) |
||
| Assertion | ntrclsbex | |- ( ph -> B e. _V ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | ntrclsbex.d | |- D = ( O ` B ) |
|
| 2 | ntrclsbex.r | |- ( ph -> I D K ) |
|
| 3 | 1 | a1i | |- ( ph -> D = ( O ` B ) ) |
| 4 | 2 3 | brfvimex | |- ( ph -> B e. _V ) |