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\left(B\right)$$
	ntrclsbex.r	$$⊢\phi \to IDK$$
Assertion	ntrclsbex	$$⊢\phi \to B\in \mathrm{V}$$

Proof

Step	Hyp	Ref	Expression
1		ntrclsbex.d	$$⊢D=O\left(B\right)$$
2		ntrclsbex.r	$$⊢\phi \to IDK$$
3	1	a1i	$$⊢\phi \to D=O\left(B\right)$$
4	2 3	brfvimex	$$⊢\phi \to B\in \mathrm{V}$$