# Metamath Proof Explorer

## Theorem ntrclsfveq

Description: If interior and closure functions are related then equality of a pair of function values is equivalent to equality of a pair of the other function's values. (Contributed by RP, 27-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}$
ntrclsfv.t ${⊢}{\phi }\to {T}\in 𝒫{B}$
Assertion ntrclsfveq ${⊢}{\phi }\to \left({I}\left({S}\right)={I}\left({T}\right)↔{K}\left({B}\setminus {S}\right)={K}\left({B}\setminus {T}\right)\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 ntrclsfv.t ${⊢}{\phi }\to {T}\in 𝒫{B}$
6 1 2 3 5 ntrclsfv ${⊢}{\phi }\to {I}\left({T}\right)={B}\setminus {K}\left({B}\setminus {T}\right)$
7 6 eqeq2d ${⊢}{\phi }\to \left({I}\left({S}\right)={I}\left({T}\right)↔{I}\left({S}\right)={B}\setminus {K}\left({B}\setminus {T}\right)\right)$
8 2 3 ntrclsrcomplex ${⊢}{\phi }\to {B}\setminus {K}\left({B}\setminus {T}\right)\in 𝒫{B}$
9 1 2 3 4 8 ntrclsfveq1 ${⊢}{\phi }\to \left({I}\left({S}\right)={B}\setminus {K}\left({B}\setminus {T}\right)↔{K}\left({B}\setminus {S}\right)={B}\setminus \left({B}\setminus {K}\left({B}\setminus {T}\right)\right)\right)$
10 1 2 3 ntrclskex ${⊢}{\phi }\to {K}\in \left({𝒫{B}}^{𝒫{B}}\right)$
11 elmapi ${⊢}{K}\in \left({𝒫{B}}^{𝒫{B}}\right)\to {K}:𝒫{B}⟶𝒫{B}$
12 10 11 syl ${⊢}{\phi }\to {K}:𝒫{B}⟶𝒫{B}$
13 2 3 ntrclsrcomplex ${⊢}{\phi }\to {B}\setminus {T}\in 𝒫{B}$
14 12 13 ffvelrnd ${⊢}{\phi }\to {K}\left({B}\setminus {T}\right)\in 𝒫{B}$
15 14 elpwid ${⊢}{\phi }\to {K}\left({B}\setminus {T}\right)\subseteq {B}$
16 dfss4 ${⊢}{K}\left({B}\setminus {T}\right)\subseteq {B}↔{B}\setminus \left({B}\setminus {K}\left({B}\setminus {T}\right)\right)={K}\left({B}\setminus {T}\right)$
17 15 16 sylib ${⊢}{\phi }\to {B}\setminus \left({B}\setminus {K}\left({B}\setminus {T}\right)\right)={K}\left({B}\setminus {T}\right)$
18 17 eqeq2d ${⊢}{\phi }\to \left({K}\left({B}\setminus {S}\right)={B}\setminus \left({B}\setminus {K}\left({B}\setminus {T}\right)\right)↔{K}\left({B}\setminus {S}\right)={K}\left({B}\setminus {T}\right)\right)$
19 7 9 18 3bitrd ${⊢}{\phi }\to \left({I}\left({S}\right)={I}\left({T}\right)↔{K}\left({B}\setminus {S}\right)={K}\left({B}\setminus {T}\right)\right)$