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	⊢ 𝐷 = ( 𝑂 ‘ 𝐵 )
	ntrclsbex.r	⊢ ( 𝜑 → 𝐼 𝐷 𝐾 )
Assertion	ntrclsbex	⊢ ( 𝜑 → 𝐵 ∈ V )

Proof

Step	Hyp	Ref	Expression
1		ntrclsbex.d	⊢ 𝐷 = ( 𝑂 ‘ 𝐵 )
2		ntrclsbex.r	⊢ ( 𝜑 → 𝐼 𝐷 𝐾 )
3	1	a1i	⊢ ( 𝜑 → 𝐷 = ( 𝑂 ‘ 𝐵 ) )
4	2 3	brfvimex	⊢ ( 𝜑 → 𝐵 ∈ V )