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\forall t\in 𝒫B\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 \leftrightarrow \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 \leftrightarrow 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)\leftrightarrow \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)\leftrightarrow 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)\leftrightarrow 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)\leftrightarrow 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 \leftrightarrow 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\forall t\in 𝒫B\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\forall t\in 𝒫B\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\forall t\in 𝒫B\left(s\cap t=\varnothing \to I\left(s\right)\cap I\left(t\right)=\varnothing \right)\to I\left(\varnothing \right)=\varnothing$$