# Metamath Proof Explorer

## Theorem ntrkbimka

Description: If the interiors of disjoint sets are disjoint, then the interior of the empty set is the empty set. (Contributed by RP, 14-Jun-2021)

Ref Expression
Assertion ntrkbimka ${⊢}\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)\to {I}\left(\varnothing \right)=\varnothing$

### Proof

Step Hyp Ref Expression
1 inidm ${⊢}{I}\left(\varnothing \right)\cap {I}\left(\varnothing \right)={I}\left(\varnothing \right)$
2 0elpw ${⊢}\varnothing \in 𝒫{B}$
3 ineq1 ${⊢}{s}=\varnothing \to {s}\cap {t}=\varnothing \cap {t}$
4 3 eqeq1d ${⊢}{s}=\varnothing \to \left({s}\cap {t}=\varnothing ↔\varnothing \cap {t}=\varnothing \right)$
5 fveq2 ${⊢}{s}=\varnothing \to {I}\left({s}\right)={I}\left(\varnothing \right)$
6 5 ineq1d ${⊢}{s}=\varnothing \to {I}\left({s}\right)\cap {I}\left({t}\right)={I}\left(\varnothing \right)\cap {I}\left({t}\right)$
7 6 eqeq1d ${⊢}{s}=\varnothing \to \left({I}\left({s}\right)\cap {I}\left({t}\right)=\varnothing ↔{I}\left(\varnothing \right)\cap {I}\left({t}\right)=\varnothing \right)$
8 4 7 imbi12d ${⊢}{s}=\varnothing \to \left(\left({s}\cap {t}=\varnothing \to {I}\left({s}\right)\cap {I}\left({t}\right)=\varnothing \right)↔\left(\varnothing \cap {t}=\varnothing \to {I}\left(\varnothing \right)\cap {I}\left({t}\right)=\varnothing \right)\right)$
9 0in ${⊢}\varnothing \cap {t}=\varnothing$
10 pm5.5 ${⊢}\varnothing \cap {t}=\varnothing \to \left(\left(\varnothing \cap {t}=\varnothing \to {I}\left(\varnothing \right)\cap {I}\left({t}\right)=\varnothing \right)↔{I}\left(\varnothing \right)\cap {I}\left({t}\right)=\varnothing \right)$
11 9 10 ax-mp ${⊢}\left(\varnothing \cap {t}=\varnothing \to {I}\left(\varnothing \right)\cap {I}\left({t}\right)=\varnothing \right)↔{I}\left(\varnothing \right)\cap {I}\left({t}\right)=\varnothing$
12 8 11 syl6bb ${⊢}{s}=\varnothing \to \left(\left({s}\cap {t}=\varnothing \to {I}\left({s}\right)\cap {I}\left({t}\right)=\varnothing \right)↔{I}\left(\varnothing \right)\cap {I}\left({t}\right)=\varnothing \right)$
13 fveq2 ${⊢}{t}=\varnothing \to {I}\left({t}\right)={I}\left(\varnothing \right)$
14 13 ineq2d ${⊢}{t}=\varnothing \to {I}\left(\varnothing \right)\cap {I}\left({t}\right)={I}\left(\varnothing \right)\cap {I}\left(\varnothing \right)$
15 14 eqeq1d ${⊢}{t}=\varnothing \to \left({I}\left(\varnothing \right)\cap {I}\left({t}\right)=\varnothing ↔{I}\left(\varnothing \right)\cap {I}\left(\varnothing \right)=\varnothing \right)$
16 12 15 rspc2v ${⊢}\left(\varnothing \in 𝒫{B}\wedge \varnothing \in 𝒫{B}\right)\to \left(\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)\to {I}\left(\varnothing \right)\cap {I}\left(\varnothing \right)=\varnothing \right)$
17 2 2 16 mp2an ${⊢}\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)\to {I}\left(\varnothing \right)\cap {I}\left(\varnothing \right)=\varnothing$
18 1 17 syl5eqr ${⊢}\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)\to {I}\left(\varnothing \right)=\varnothing$