# Metamath Proof Explorer

## 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 {I}{D}{K}$
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 {I}{D}{K}$
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)$