Theorem ntrclsfv

Description: The value of the interior (closure) expressed in terms of the closure (interior). (Contributed by RP, 25-Jun-2021)

	Ref	Expression
Hypotheses	ntrcls.o	$$⊢O=\left(i\in \mathrm{V}⟼\left(k\in \left({𝒫i}^{𝒫i}\right)⟼\left(j\in 𝒫i⟼i\setminus k\left(i\setminus j\right)\right)\right)\right)$$
	ntrcls.d	$$⊢D=O\left(B\right)$$
	ntrcls.r	$$⊢\phi \to IDK$$
	ntrclsfv.s	$$⊢\phi \to S\in 𝒫B$$
Assertion	ntrclsfv	$$⊢\phi \to I\left(S\right)=B\setminus K\left(B\setminus S\right)$$

Proof

Step	Hyp	Ref	Expression
1		ntrcls.o	$$⊢O=\left(i\in \mathrm{V}⟼\left(k\in \left({𝒫i}^{𝒫i}\right)⟼\left(j\in 𝒫i⟼i\setminus k\left(i\setminus j\right)\right)\right)\right)$$
2		ntrcls.d	$$⊢D=O\left(B\right)$$
3		ntrcls.r	$$⊢\phi \to IDK$$
4		ntrclsfv.s	$$⊢\phi \to S\in 𝒫B$$
5	1 2 3	ntrclsfv2	$$⊢\phi \to D\left(K\right)=I$$
6	5	fveq1d	$$⊢\phi \to D\left(K\right)\left(S\right)=I\left(S\right)$$
7	2 3	ntrclsbex	$$⊢\phi \to B\in \mathrm{V}$$
8	1 2 3	ntrclskex	$$⊢\phi \to K\in \left({𝒫B}^{𝒫B}\right)$$
9		eqid	$$⊢D\left(K\right)=D\left(K\right)$$
10		eqid	$$⊢D\left(K\right)\left(S\right)=D\left(K\right)\left(S\right)$$
11	1 2 7 8 9 4 10	dssmapfv3d	$$⊢\phi \to D\left(K\right)\left(S\right)=B\setminus K\left(B\setminus S\right)$$
12	6 11	eqtr3d	$$⊢\phi \to I\left(S\right)=B\setminus K\left(B\setminus S\right)$$