Metamath Proof Explorer

Theorem ntrin

Description: A pairwise intersection of interiors is the interior of the intersection. This does not always hold for arbitrary intersections. (Contributed by Jeff Hankins, 31-Aug-2009)

Ref Expression
Hypothesis clscld.1 
|- X = U. J
Assertion ntrin 
|- ( ( J e. Top /\ A C_ X /\ B C_ X ) -> ( ( int ` J ) ` ( A i^i B ) ) = ( ( ( int ` J ) ` A ) i^i ( ( int ` J ) ` B ) ) )

Proof

Step Hyp Ref Expression
1 clscld.1 
 |-  X = U. J
2 inss1 
 |-  ( A i^i B ) C_ A
3 1 ntrss 
 |-  ( ( J e. Top /\ A C_ X /\ ( A i^i B ) C_ A ) -> ( ( int ` J ) ` ( A i^i B ) ) C_ ( ( int ` J ) ` A ) )
4 2 3 mp3an3 
 |-  ( ( J e. Top /\ A C_ X ) -> ( ( int ` J ) ` ( A i^i B ) ) C_ ( ( int ` J ) ` A ) )
5 4 3adant3 
 |-  ( ( J e. Top /\ A C_ X /\ B C_ X ) -> ( ( int ` J ) ` ( A i^i B ) ) C_ ( ( int ` J ) ` A ) )
6 inss2 
 |-  ( A i^i B ) C_ B
7 1 ntrss 
 |-  ( ( J e. Top /\ B C_ X /\ ( A i^i B ) C_ B ) -> ( ( int ` J ) ` ( A i^i B ) ) C_ ( ( int ` J ) ` B ) )
8 6 7 mp3an3 
 |-  ( ( J e. Top /\ B C_ X ) -> ( ( int ` J ) ` ( A i^i B ) ) C_ ( ( int ` J ) ` B ) )
9 8 3adant2 
 |-  ( ( J e. Top /\ A C_ X /\ B C_ X ) -> ( ( int ` J ) ` ( A i^i B ) ) C_ ( ( int ` J ) ` B ) )
10 5 9 ssind 
 |-  ( ( J e. Top /\ A C_ X /\ B C_ X ) -> ( ( int ` J ) ` ( A i^i B ) ) C_ ( ( ( int ` J ) ` A ) i^i ( ( int ` J ) ` B ) ) )
11 simp1 
 |-  ( ( J e. Top /\ A C_ X /\ B C_ X ) -> J e. Top )
12 ssinss1 
 |-  ( A C_ X -> ( A i^i B ) C_ X )
13 12 3ad2ant2 
 |-  ( ( J e. Top /\ A C_ X /\ B C_ X ) -> ( A i^i B ) C_ X )
14 1 ntropn 
 |-  ( ( J e. Top /\ A C_ X ) -> ( ( int ` J ) ` A ) e. J )
15 14 3adant3 
 |-  ( ( J e. Top /\ A C_ X /\ B C_ X ) -> ( ( int ` J ) ` A ) e. J )
16 1 ntropn 
 |-  ( ( J e. Top /\ B C_ X ) -> ( ( int ` J ) ` B ) e. J )
17 16 3adant2 
 |-  ( ( J e. Top /\ A C_ X /\ B C_ X ) -> ( ( int ` J ) ` B ) e. J )
18 inopn 
 |-  ( ( J e. Top /\ ( ( int ` J ) ` A ) e. J /\ ( ( int ` J ) ` B ) e. J ) -> ( ( ( int ` J ) ` A ) i^i ( ( int ` J ) ` B ) ) e. J )
19 11 15 17 18 syl3anc 
 |-  ( ( J e. Top /\ A C_ X /\ B C_ X ) -> ( ( ( int ` J ) ` A ) i^i ( ( int ` J ) ` B ) ) e. J )
20 inss1 
 |-  ( ( ( int ` J ) ` A ) i^i ( ( int ` J ) ` B ) ) C_ ( ( int ` J ) ` A )
21 1 ntrss2 
 |-  ( ( J e. Top /\ A C_ X ) -> ( ( int ` J ) ` A ) C_ A )
22 21 3adant3 
 |-  ( ( J e. Top /\ A C_ X /\ B C_ X ) -> ( ( int ` J ) ` A ) C_ A )
23 20 22 sstrid 
 |-  ( ( J e. Top /\ A C_ X /\ B C_ X ) -> ( ( ( int ` J ) ` A ) i^i ( ( int ` J ) ` B ) ) C_ A )
24 inss2 
 |-  ( ( ( int ` J ) ` A ) i^i ( ( int ` J ) ` B ) ) C_ ( ( int ` J ) ` B )
25 1 ntrss2 
 |-  ( ( J e. Top /\ B C_ X ) -> ( ( int ` J ) ` B ) C_ B )
26 25 3adant2 
 |-  ( ( J e. Top /\ A C_ X /\ B C_ X ) -> ( ( int ` J ) ` B ) C_ B )
27 24 26 sstrid 
 |-  ( ( J e. Top /\ A C_ X /\ B C_ X ) -> ( ( ( int ` J ) ` A ) i^i ( ( int ` J ) ` B ) ) C_ B )
28 23 27 ssind 
 |-  ( ( J e. Top /\ A C_ X /\ B C_ X ) -> ( ( ( int ` J ) ` A ) i^i ( ( int ` J ) ` B ) ) C_ ( A i^i B ) )
29 1 ssntr 
 |-  ( ( ( J e. Top /\ ( A i^i B ) C_ X ) /\ ( ( ( ( int ` J ) ` A ) i^i ( ( int ` J ) ` B ) ) e. J /\ ( ( ( int ` J ) ` A ) i^i ( ( int ` J ) ` B ) ) C_ ( A i^i B ) ) ) -> ( ( ( int ` J ) ` A ) i^i ( ( int ` J ) ` B ) ) C_ ( ( int ` J ) ` ( A i^i B ) ) )
30 11 13 19 28 29 syl22anc 
 |-  ( ( J e. Top /\ A C_ X /\ B C_ X ) -> ( ( ( int ` J ) ` A ) i^i ( ( int ` J ) ` B ) ) C_ ( ( int ` J ) ` ( A i^i B ) ) )
31 10 30 eqssd 
 |-  ( ( J e. Top /\ A C_ X /\ B C_ X ) -> ( ( int ` J ) ` ( A i^i B ) ) = ( ( ( int ` J ) ` A ) i^i ( ( int ` J ) ` B ) ) )