Metamath Proof Explorer

Theorem ntrk0kbimka

Description: If the interiors of disjoint sets are disjoint and the interior of the base set is the base set, then the interior of the empty set is the empty set. Obsolete version of ntrkbimka . (Contributed by RP, 12-Jun-2021)

Ref Expression
Assertion ntrk0kbimka 
|- ( ( B e. V /\ I e. ( ~P B ^m ~P B ) ) -> ( ( ( I ` B ) = B /\ 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 pwidg 
 |-  ( B e. V -> B e. ~P B )
2 1 ad2antrr 
 |-  ( ( ( B e. V /\ I e. ( ~P B ^m ~P B ) ) /\ ( ( I ` B ) = B /\ A. s e. ~P B A. t e. ~P B ( ( s i^i t ) = (/) -> ( ( I ` s ) i^i ( I ` t ) ) = (/) ) ) ) -> B e. ~P B )
3 0elpw 
 |-  (/) e. ~P B
4 3 a1i 
 |-  ( ( ( B e. V /\ I e. ( ~P B ^m ~P B ) ) /\ ( ( I ` B ) = B /\ A. s e. ~P B A. t e. ~P B ( ( s i^i t ) = (/) -> ( ( I ` s ) i^i ( I ` t ) ) = (/) ) ) ) -> (/) e. ~P B )
5 simprr 
 |-  ( ( ( B e. V /\ I e. ( ~P B ^m ~P B ) ) /\ ( ( I ` B ) = B /\ A. s e. ~P B A. t e. ~P B ( ( s i^i t ) = (/) -> ( ( I ` s ) i^i ( I ` t ) ) = (/) ) ) ) -> A. s e. ~P B A. t e. ~P B ( ( s i^i t ) = (/) -> ( ( I ` s ) i^i ( I ` t ) ) = (/) ) )
6 ineq1 
 |-  ( s = B -> ( s i^i t ) = ( B i^i t ) )
7 6 eqeq1d 
 |-  ( s = B -> ( ( s i^i t ) = (/) <-> ( B i^i t ) = (/) ) )
8 fveq2 
 |-  ( s = B -> ( I ` s ) = ( I ` B ) )
9 8 ineq1d 
 |-  ( s = B -> ( ( I ` s ) i^i ( I ` t ) ) = ( ( I ` B ) i^i ( I ` t ) ) )
10 9 eqeq1d 
 |-  ( s = B -> ( ( ( I ` s ) i^i ( I ` t ) ) = (/) <-> ( ( I ` B ) i^i ( I ` t ) ) = (/) ) )
11 7 10 imbi12d 
 |-  ( s = B -> ( ( ( s i^i t ) = (/) -> ( ( I ` s ) i^i ( I ` t ) ) = (/) ) <-> ( ( B i^i t ) = (/) -> ( ( I ` B ) i^i ( I ` t ) ) = (/) ) ) )
12 ineq2 
 |-  ( t = (/) -> ( B i^i t ) = ( B i^i (/) ) )
13 12 eqeq1d 
 |-  ( t = (/) -> ( ( B i^i t ) = (/) <-> ( B i^i (/) ) = (/) ) )
14 fveq2 
 |-  ( t = (/) -> ( I ` t ) = ( I ` (/) ) )
15 14 ineq2d 
 |-  ( t = (/) -> ( ( I ` B ) i^i ( I ` t ) ) = ( ( I ` B ) i^i ( I ` (/) ) ) )
16 15 eqeq1d 
 |-  ( t = (/) -> ( ( ( I ` B ) i^i ( I ` t ) ) = (/) <-> ( ( I ` B ) i^i ( I ` (/) ) ) = (/) ) )
17 13 16 imbi12d 
 |-  ( t = (/) -> ( ( ( B i^i t ) = (/) -> ( ( I ` B ) i^i ( I ` t ) ) = (/) ) <-> ( ( B i^i (/) ) = (/) -> ( ( I ` B ) i^i ( I ` (/) ) ) = (/) ) ) )
18 in0 
 |-  ( B i^i (/) ) = (/)
19 pm5.5 
 |-  ( ( B i^i (/) ) = (/) -> ( ( ( B i^i (/) ) = (/) -> ( ( I ` B ) i^i ( I ` (/) ) ) = (/) ) <-> ( ( I ` B ) i^i ( I ` (/) ) ) = (/) ) )
20 18 19 mp1i 
 |-  ( t = (/) -> ( ( ( B i^i (/) ) = (/) -> ( ( I ` B ) i^i ( I ` (/) ) ) = (/) ) <-> ( ( I ` B ) i^i ( I ` (/) ) ) = (/) ) )
21 17 20 bitrd 
 |-  ( t = (/) -> ( ( ( B i^i t ) = (/) -> ( ( I ` B ) i^i ( I ` t ) ) = (/) ) <-> ( ( I ` B ) i^i ( I ` (/) ) ) = (/) ) )
22 11 21 rspc2va 
 |-  ( ( ( B 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 ` B ) i^i ( I ` (/) ) ) = (/) )
23 2 4 5 22 syl21anc 
 |-  ( ( ( B e. V /\ I e. ( ~P B ^m ~P B ) ) /\ ( ( I ` B ) = B /\ A. s e. ~P B A. t e. ~P B ( ( s i^i t ) = (/) -> ( ( I ` s ) i^i ( I ` t ) ) = (/) ) ) ) -> ( ( I ` B ) i^i ( I ` (/) ) ) = (/) )
24 23 ex 
 |-  ( ( B e. V /\ I e. ( ~P B ^m ~P B ) ) -> ( ( ( I ` B ) = B /\ A. s e. ~P B A. t e. ~P B ( ( s i^i t ) = (/) -> ( ( I ` s ) i^i ( I ` t ) ) = (/) ) ) -> ( ( I ` B ) i^i ( I ` (/) ) ) = (/) ) )
25 elmapi 
 |-  ( I e. ( ~P B ^m ~P B ) -> I : ~P B --> ~P B )
26 25 adantl 
 |-  ( ( B e. V /\ I e. ( ~P B ^m ~P B ) ) -> I : ~P B --> ~P B )
27 3 a1i 
 |-  ( ( B e. V /\ I e. ( ~P B ^m ~P B ) ) -> (/) e. ~P B )
28 26 27 ffvelrnd 
 |-  ( ( B e. V /\ I e. ( ~P B ^m ~P B ) ) -> ( I ` (/) ) e. ~P B )
29 28 elpwid 
 |-  ( ( B e. V /\ I e. ( ~P B ^m ~P B ) ) -> ( I ` (/) ) C_ B )
30 simpl 
 |-  ( ( ( I ` B ) = B /\ A. s e. ~P B A. t e. ~P B ( ( s i^i t ) = (/) -> ( ( I ` s ) i^i ( I ` t ) ) = (/) ) ) -> ( I ` B ) = B )
31 ineq1 
 |-  ( ( I ` B ) = B -> ( ( I ` B ) i^i ( I ` (/) ) ) = ( B i^i ( I ` (/) ) ) )
32 incom 
 |-  ( B i^i ( I ` (/) ) ) = ( ( I ` (/) ) i^i B )
33 31 32 eqtrdi 
 |-  ( ( I ` B ) = B -> ( ( I ` B ) i^i ( I ` (/) ) ) = ( ( I ` (/) ) i^i B ) )
34 33 eqeq1d 
 |-  ( ( I ` B ) = B -> ( ( ( I ` B ) i^i ( I ` (/) ) ) = (/) <-> ( ( I ` (/) ) i^i B ) = (/) ) )
35 34 biimpd 
 |-  ( ( I ` B ) = B -> ( ( ( I ` B ) i^i ( I ` (/) ) ) = (/) -> ( ( I ` (/) ) i^i B ) = (/) ) )
36 reldisj 
 |-  ( ( I ` (/) ) C_ B -> ( ( ( I ` (/) ) i^i B ) = (/) <-> ( I ` (/) ) C_ ( B \ B ) ) )
37 36 biimpd 
 |-  ( ( I ` (/) ) C_ B -> ( ( ( I ` (/) ) i^i B ) = (/) -> ( I ` (/) ) C_ ( B \ B ) ) )
38 difid 
 |-  ( B \ B ) = (/)
39 38 sseq2i 
 |-  ( ( I ` (/) ) C_ ( B \ B ) <-> ( I ` (/) ) C_ (/) )
40 ss0 
 |-  ( ( I ` (/) ) C_ (/) -> ( I ` (/) ) = (/) )
41 39 40 sylbi 
 |-  ( ( I ` (/) ) C_ ( B \ B ) -> ( I ` (/) ) = (/) )
42 37 41 syl6com 
 |-  ( ( ( I ` (/) ) i^i B ) = (/) -> ( ( I ` (/) ) C_ B -> ( I ` (/) ) = (/) ) )
43 35 42 syl6com 
 |-  ( ( ( I ` B ) i^i ( I ` (/) ) ) = (/) -> ( ( I ` B ) = B -> ( ( I ` (/) ) C_ B -> ( I ` (/) ) = (/) ) ) )
44 43 com13 
 |-  ( ( I ` (/) ) C_ B -> ( ( I ` B ) = B -> ( ( ( I ` B ) i^i ( I ` (/) ) ) = (/) -> ( I ` (/) ) = (/) ) ) )
45 29 30 44 syl2im 
 |-  ( ( B e. V /\ I e. ( ~P B ^m ~P B ) ) -> ( ( ( I ` B ) = B /\ A. s e. ~P B A. t e. ~P B ( ( s i^i t ) = (/) -> ( ( I ` s ) i^i ( I ` t ) ) = (/) ) ) -> ( ( ( I ` B ) i^i ( I ` (/) ) ) = (/) -> ( I ` (/) ) = (/) ) ) )
46 24 45 mpdd 
 |-  ( ( B e. V /\ I e. ( ~P B ^m ~P B ) ) -> ( ( ( I ` B ) = B /\ A. s e. ~P B A. t e. ~P B ( ( s i^i t ) = (/) -> ( ( I ` s ) i^i ( I ` t ) ) = (/) ) ) -> ( I ` (/) ) = (/) ) )