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 s 𝒫 B t 𝒫 B s t = I s I t = I =

Proof

Step Hyp Ref Expression
1 inidm I I = I
2 0elpw 𝒫 B
3 ineq1 s = s t = t
4 3 eqeq1d s = s t = t =
5 fveq2 s = I s = I
6 5 ineq1d s = I s I t = I I t
7 6 eqeq1d s = I s I t = I I t =
8 4 7 imbi12d s = s t = I s I t = t = I I t =
9 0in t =
10 pm5.5 t = t = I I t = I I t =
11 9 10 ax-mp t = I I t = I I t =
12 8 11 bitrdi s = s t = I s I t = I I t =
13 fveq2 t = I t = I
14 13 ineq2d t = I I t = I I
15 14 eqeq1d t = I I t = I I =
16 12 15 rspc2v 𝒫 B 𝒫 B s 𝒫 B t 𝒫 B s t = I s I t = I I =
17 2 2 16 mp2an s 𝒫 B t 𝒫 B s t = I s I t = I I =
18 1 17 eqtr3id s 𝒫 B t 𝒫 B s t = I s I t = I =