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 
|- ( A. s e. ~P B A. t e. ~P B ( ( s i^i t ) = (/) -> ( ( I ` s ) i^i ( I ` t ) ) = (/) ) -> ( I ` (/) ) = (/) )

Proof

Step Hyp Ref Expression
1 inidm 
 |-  ( ( I ` (/) ) i^i ( I ` (/) ) ) = ( I ` (/) )
2 0elpw 
 |-  (/) e. ~P B
3 ineq1 
 |-  ( s = (/) -> ( s i^i t ) = ( (/) i^i t ) )
4 3 eqeq1d 
 |-  ( s = (/) -> ( ( s i^i t ) = (/) <-> ( (/) i^i t ) = (/) ) )
5 fveq2 
 |-  ( s = (/) -> ( I ` s ) = ( I ` (/) ) )
6 5 ineq1d 
 |-  ( s = (/) -> ( ( I ` s ) i^i ( I ` t ) ) = ( ( I ` (/) ) i^i ( I ` t ) ) )
7 6 eqeq1d 
 |-  ( s = (/) -> ( ( ( I ` s ) i^i ( I ` t ) ) = (/) <-> ( ( I ` (/) ) i^i ( I ` t ) ) = (/) ) )
8 4 7 imbi12d 
 |-  ( s = (/) -> ( ( ( s i^i t ) = (/) -> ( ( I ` s ) i^i ( I ` t ) ) = (/) ) <-> ( ( (/) i^i t ) = (/) -> ( ( I ` (/) ) i^i ( I ` t ) ) = (/) ) ) )
9 0in 
 |-  ( (/) i^i t ) = (/)
10 pm5.5 
 |-  ( ( (/) i^i t ) = (/) -> ( ( ( (/) i^i t ) = (/) -> ( ( I ` (/) ) i^i ( I ` t ) ) = (/) ) <-> ( ( I ` (/) ) i^i ( I ` t ) ) = (/) ) )
11 9 10 ax-mp 
 |-  ( ( ( (/) i^i t ) = (/) -> ( ( I ` (/) ) i^i ( I ` t ) ) = (/) ) <-> ( ( I ` (/) ) i^i ( I ` t ) ) = (/) )
12 8 11 bitrdi 
 |-  ( s = (/) -> ( ( ( s i^i t ) = (/) -> ( ( I ` s ) i^i ( I ` t ) ) = (/) ) <-> ( ( I ` (/) ) i^i ( I ` t ) ) = (/) ) )
13 fveq2 
 |-  ( t = (/) -> ( I ` t ) = ( I ` (/) ) )
14 13 ineq2d 
 |-  ( t = (/) -> ( ( I ` (/) ) i^i ( I ` t ) ) = ( ( I ` (/) ) i^i ( I ` (/) ) ) )
15 14 eqeq1d 
 |-  ( t = (/) -> ( ( ( I ` (/) ) i^i ( I ` t ) ) = (/) <-> ( ( I ` (/) ) i^i ( I ` (/) ) ) = (/) ) )
16 12 15 rspc2v 
 |-  ( ( (/) e. ~P B /\ (/) e. ~P B ) -> ( A. s e. ~P B A. t e. ~P B ( ( s i^i t ) = (/) -> ( ( I ` s ) i^i ( I ` t ) ) = (/) ) -> ( ( I ` (/) ) i^i ( I ` (/) ) ) = (/) ) )
17 2 2 16 mp2an 
 |-  ( A. s e. ~P B A. t e. ~P B ( ( s i^i t ) = (/) -> ( ( I ` s ) i^i ( I ` t ) ) = (/) ) -> ( ( I ` (/) ) i^i ( I ` (/) ) ) = (/) )
18 1 17 eqtr3id 
 |-  ( A. s e. ~P B A. t e. ~P B ( ( s i^i t ) = (/) -> ( ( I ` s ) i^i ( I ` t ) ) = (/) ) -> ( I ` (/) ) = (/) )