# Metamath Proof Explorer

## Theorem ntrclsfveq1

Description: If interior and closure functions are related then specific function values are complementary. (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.c ${⊢}{\phi }\to {C}\in 𝒫{B}$
Assertion ntrclsfveq1 ${⊢}{\phi }\to \left({I}\left({S}\right)={C}↔{K}\left({B}\setminus {S}\right)={B}\setminus {C}\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.c ${⊢}{\phi }\to {C}\in 𝒫{B}$
6 5 elpwid ${⊢}{\phi }\to {C}\subseteq {B}$
7 dfss4 ${⊢}{C}\subseteq {B}↔{B}\setminus \left({B}\setminus {C}\right)={C}$
8 6 7 sylib ${⊢}{\phi }\to {B}\setminus \left({B}\setminus {C}\right)={C}$
9 8 eqcomd ${⊢}{\phi }\to {C}={B}\setminus \left({B}\setminus {C}\right)$
10 9 eqeq2d ${⊢}{\phi }\to \left({B}\setminus {K}\left({B}\setminus {S}\right)={C}↔{B}\setminus {K}\left({B}\setminus {S}\right)={B}\setminus \left({B}\setminus {C}\right)\right)$
11 1 2 3 4 ntrclsfv ${⊢}{\phi }\to {I}\left({S}\right)={B}\setminus {K}\left({B}\setminus {S}\right)$
12 11 eqeq1d ${⊢}{\phi }\to \left({I}\left({S}\right)={C}↔{B}\setminus {K}\left({B}\setminus {S}\right)={C}\right)$
13 1 2 3 ntrclskex ${⊢}{\phi }\to {K}\in \left({𝒫{B}}^{𝒫{B}}\right)$
14 elmapi ${⊢}{K}\in \left({𝒫{B}}^{𝒫{B}}\right)\to {K}:𝒫{B}⟶𝒫{B}$
15 13 14 syl ${⊢}{\phi }\to {K}:𝒫{B}⟶𝒫{B}$
16 2 3 ntrclsrcomplex ${⊢}{\phi }\to {B}\setminus {S}\in 𝒫{B}$
17 15 16 ffvelrnd ${⊢}{\phi }\to {K}\left({B}\setminus {S}\right)\in 𝒫{B}$
18 17 elpwid ${⊢}{\phi }\to {K}\left({B}\setminus {S}\right)\subseteq {B}$
19 difssd ${⊢}{\phi }\to {B}\setminus {C}\subseteq {B}$
20 rcompleq ${⊢}\left({K}\left({B}\setminus {S}\right)\subseteq {B}\wedge {B}\setminus {C}\subseteq {B}\right)\to \left({K}\left({B}\setminus {S}\right)={B}\setminus {C}↔{B}\setminus {K}\left({B}\setminus {S}\right)={B}\setminus \left({B}\setminus {C}\right)\right)$
21 18 19 20 syl2anc ${⊢}{\phi }\to \left({K}\left({B}\setminus {S}\right)={B}\setminus {C}↔{B}\setminus {K}\left({B}\setminus {S}\right)={B}\setminus \left({B}\setminus {C}\right)\right)$
22 10 12 21 3bitr4d ${⊢}{\phi }\to \left({I}\left({S}\right)={C}↔{K}\left({B}\setminus {S}\right)={B}\setminus {C}\right)$