Metamath Proof Explorer

Theorem ntrclsbex

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 φ I D K
Assertion ntrclsbex φ B V


Step Hyp Ref Expression
1 ntrclsbex.d D = O B
2 ntrclsbex.r φ I D K
3 1 a1i φ D = O B
4 2 3 brfvimex φ B V