# Metamath Proof Explorer

## Theorem ntrk2imkb

Description: If an interior function is contracting, the interiors of disjoint sets are disjoint. Kuratowski's K2 axiom implies KB. Interior version. (Contributed by RP, 9-Jun-2021)

Ref Expression
Assertion ntrk2imkb ${⊢}\forall {s}\in 𝒫{B}\phantom{\rule{.4em}{0ex}}{I}\left({s}\right)\subseteq {s}\to \forall {s}\in 𝒫{B}\phantom{\rule{.4em}{0ex}}\forall {t}\in 𝒫{B}\phantom{\rule{.4em}{0ex}}\left({s}\cap {t}=\varnothing \to {I}\left({s}\right)\cap {I}\left({t}\right)=\varnothing \right)$

### Proof

Step Hyp Ref Expression
1 id ${⊢}\forall {s}\in 𝒫{B}\phantom{\rule{.4em}{0ex}}{I}\left({s}\right)\subseteq {s}\to \forall {s}\in 𝒫{B}\phantom{\rule{.4em}{0ex}}{I}\left({s}\right)\subseteq {s}$
2 fveq2 ${⊢}{s}={t}\to {I}\left({s}\right)={I}\left({t}\right)$
3 id ${⊢}{s}={t}\to {s}={t}$
4 2 3 sseq12d ${⊢}{s}={t}\to \left({I}\left({s}\right)\subseteq {s}↔{I}\left({t}\right)\subseteq {t}\right)$
5 4 cbvralvw ${⊢}\forall {s}\in 𝒫{B}\phantom{\rule{.4em}{0ex}}{I}\left({s}\right)\subseteq {s}↔\forall {t}\in 𝒫{B}\phantom{\rule{.4em}{0ex}}{I}\left({t}\right)\subseteq {t}$
6 5 biimpi ${⊢}\forall {s}\in 𝒫{B}\phantom{\rule{.4em}{0ex}}{I}\left({s}\right)\subseteq {s}\to \forall {t}\in 𝒫{B}\phantom{\rule{.4em}{0ex}}{I}\left({t}\right)\subseteq {t}$
7 raaanv ${⊢}\forall {s}\in 𝒫{B}\phantom{\rule{.4em}{0ex}}\forall {t}\in 𝒫{B}\phantom{\rule{.4em}{0ex}}\left({I}\left({s}\right)\subseteq {s}\wedge {I}\left({t}\right)\subseteq {t}\right)↔\left(\forall {s}\in 𝒫{B}\phantom{\rule{.4em}{0ex}}{I}\left({s}\right)\subseteq {s}\wedge \forall {t}\in 𝒫{B}\phantom{\rule{.4em}{0ex}}{I}\left({t}\right)\subseteq {t}\right)$
8 1 6 7 sylanbrc ${⊢}\forall {s}\in 𝒫{B}\phantom{\rule{.4em}{0ex}}{I}\left({s}\right)\subseteq {s}\to \forall {s}\in 𝒫{B}\phantom{\rule{.4em}{0ex}}\forall {t}\in 𝒫{B}\phantom{\rule{.4em}{0ex}}\left({I}\left({s}\right)\subseteq {s}\wedge {I}\left({t}\right)\subseteq {t}\right)$
9 ss2in ${⊢}\left({I}\left({s}\right)\subseteq {s}\wedge {I}\left({t}\right)\subseteq {t}\right)\to {I}\left({s}\right)\cap {I}\left({t}\right)\subseteq {s}\cap {t}$
10 9 adantr ${⊢}\left(\left({I}\left({s}\right)\subseteq {s}\wedge {I}\left({t}\right)\subseteq {t}\right)\wedge {s}\cap {t}=\varnothing \right)\to {I}\left({s}\right)\cap {I}\left({t}\right)\subseteq {s}\cap {t}$
11 simpr ${⊢}\left(\left({I}\left({s}\right)\subseteq {s}\wedge {I}\left({t}\right)\subseteq {t}\right)\wedge {s}\cap {t}=\varnothing \right)\to {s}\cap {t}=\varnothing$
12 10 11 sseqtrd ${⊢}\left(\left({I}\left({s}\right)\subseteq {s}\wedge {I}\left({t}\right)\subseteq {t}\right)\wedge {s}\cap {t}=\varnothing \right)\to {I}\left({s}\right)\cap {I}\left({t}\right)\subseteq \varnothing$
13 ss0 ${⊢}{I}\left({s}\right)\cap {I}\left({t}\right)\subseteq \varnothing \to {I}\left({s}\right)\cap {I}\left({t}\right)=\varnothing$
14 12 13 syl ${⊢}\left(\left({I}\left({s}\right)\subseteq {s}\wedge {I}\left({t}\right)\subseteq {t}\right)\wedge {s}\cap {t}=\varnothing \right)\to {I}\left({s}\right)\cap {I}\left({t}\right)=\varnothing$
15 14 ex ${⊢}\left({I}\left({s}\right)\subseteq {s}\wedge {I}\left({t}\right)\subseteq {t}\right)\to \left({s}\cap {t}=\varnothing \to {I}\left({s}\right)\cap {I}\left({t}\right)=\varnothing \right)$
16 15 2ralimi ${⊢}\forall {s}\in 𝒫{B}\phantom{\rule{.4em}{0ex}}\forall {t}\in 𝒫{B}\phantom{\rule{.4em}{0ex}}\left({I}\left({s}\right)\subseteq {s}\wedge {I}\left({t}\right)\subseteq {t}\right)\to \forall {s}\in 𝒫{B}\phantom{\rule{.4em}{0ex}}\forall {t}\in 𝒫{B}\phantom{\rule{.4em}{0ex}}\left({s}\cap {t}=\varnothing \to {I}\left({s}\right)\cap {I}\left({t}\right)=\varnothing \right)$
17 8 16 syl ${⊢}\forall {s}\in 𝒫{B}\phantom{\rule{.4em}{0ex}}{I}\left({s}\right)\subseteq {s}\to \forall {s}\in 𝒫{B}\phantom{\rule{.4em}{0ex}}\forall {t}\in 𝒫{B}\phantom{\rule{.4em}{0ex}}\left({s}\cap {t}=\varnothing \to {I}\left({s}\right)\cap {I}\left({t}\right)=\varnothing \right)$