Metamath Proof Explorer

Theorem ntrclsss

Description: If interior and closure functions are related then a subset relation of a pair of function values is equivalent to subset relation 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 ntrclsss ${⊢}{\phi }\to \left({I}\left({S}\right)\subseteq {I}\left({T}\right)↔{K}\left({B}\setminus {T}\right)\subseteq {K}\left({B}\setminus {S}\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 4 ntrclsfv ${⊢}{\phi }\to {I}\left({S}\right)={B}\setminus {K}\left({B}\setminus {S}\right)$
7 1 2 3 5 ntrclsfv ${⊢}{\phi }\to {I}\left({T}\right)={B}\setminus {K}\left({B}\setminus {T}\right)$
8 6 7 sseq12d ${⊢}{\phi }\to \left({I}\left({S}\right)\subseteq {I}\left({T}\right)↔{B}\setminus {K}\left({B}\setminus {S}\right)\subseteq {B}\setminus {K}\left({B}\setminus {T}\right)\right)$
9 1 2 3 ntrclskex ${⊢}{\phi }\to {K}\in \left({𝒫{B}}^{𝒫{B}}\right)$
10 9 ancli ${⊢}{\phi }\to \left({\phi }\wedge {K}\in \left({𝒫{B}}^{𝒫{B}}\right)\right)$
11 elmapi ${⊢}{K}\in \left({𝒫{B}}^{𝒫{B}}\right)\to {K}:𝒫{B}⟶𝒫{B}$
12 11 adantl ${⊢}\left({\phi }\wedge {K}\in \left({𝒫{B}}^{𝒫{B}}\right)\right)\to {K}:𝒫{B}⟶𝒫{B}$
13 2 3 ntrclsrcomplex ${⊢}{\phi }\to {B}\setminus {T}\in 𝒫{B}$
14 13 adantr ${⊢}\left({\phi }\wedge {K}\in \left({𝒫{B}}^{𝒫{B}}\right)\right)\to {B}\setminus {T}\in 𝒫{B}$
15 12 14 ffvelrnd ${⊢}\left({\phi }\wedge {K}\in \left({𝒫{B}}^{𝒫{B}}\right)\right)\to {K}\left({B}\setminus {T}\right)\in 𝒫{B}$
16 15 elpwid ${⊢}\left({\phi }\wedge {K}\in \left({𝒫{B}}^{𝒫{B}}\right)\right)\to {K}\left({B}\setminus {T}\right)\subseteq {B}$
17 2 3 ntrclsrcomplex ${⊢}{\phi }\to {B}\setminus {S}\in 𝒫{B}$
18 17 adantr ${⊢}\left({\phi }\wedge {K}\in \left({𝒫{B}}^{𝒫{B}}\right)\right)\to {B}\setminus {S}\in 𝒫{B}$
19 12 18 ffvelrnd ${⊢}\left({\phi }\wedge {K}\in \left({𝒫{B}}^{𝒫{B}}\right)\right)\to {K}\left({B}\setminus {S}\right)\in 𝒫{B}$
20 19 elpwid ${⊢}\left({\phi }\wedge {K}\in \left({𝒫{B}}^{𝒫{B}}\right)\right)\to {K}\left({B}\setminus {S}\right)\subseteq {B}$
21 16 20 jca ${⊢}\left({\phi }\wedge {K}\in \left({𝒫{B}}^{𝒫{B}}\right)\right)\to \left({K}\left({B}\setminus {T}\right)\subseteq {B}\wedge {K}\left({B}\setminus {S}\right)\subseteq {B}\right)$
22 sscon34b ${⊢}\left({K}\left({B}\setminus {T}\right)\subseteq {B}\wedge {K}\left({B}\setminus {S}\right)\subseteq {B}\right)\to \left({K}\left({B}\setminus {T}\right)\subseteq {K}\left({B}\setminus {S}\right)↔{B}\setminus {K}\left({B}\setminus {S}\right)\subseteq {B}\setminus {K}\left({B}\setminus {T}\right)\right)$
23 10 21 22 3syl ${⊢}{\phi }\to \left({K}\left({B}\setminus {T}\right)\subseteq {K}\left({B}\setminus {S}\right)↔{B}\setminus {K}\left({B}\setminus {S}\right)\subseteq {B}\setminus {K}\left({B}\setminus {T}\right)\right)$
24 8 23 bitr4d ${⊢}{\phi }\to \left({I}\left({S}\right)\subseteq {I}\left({T}\right)↔{K}\left({B}\setminus {T}\right)\subseteq {K}\left({B}\setminus {S}\right)\right)$