This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ 𝑋 = ∪ 𝐽
Assertion ntrin ( ( 𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑋 ) → ( ( int ‘ 𝐽 ) ‘ ( 𝐴 ∩ 𝐵 ) ) = ( ( ( int ‘ 𝐽 ) ‘ 𝐴 ) ∩ ( ( int ‘ 𝐽 ) ‘ 𝐵 ) ) )

Proof

Step Hyp Ref Expression
1 clscld.1 ⊢ 𝑋 = ∪ 𝐽
2 inss1 ⊢ ( 𝐴 ∩ 𝐵 ) ⊆ 𝐴
3 1 ntrss ⊢ ( ( 𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ ( 𝐴 ∩ 𝐵 ) ⊆ 𝐴 ) → ( ( int ‘ 𝐽 ) ‘ ( 𝐴 ∩ 𝐵 ) ) ⊆ ( ( int ‘ 𝐽 ) ‘ 𝐴 ) )
4 2 3 mp3an3 ⊢ ( ( 𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ) → ( ( int ‘ 𝐽 ) ‘ ( 𝐴 ∩ 𝐵 ) ) ⊆ ( ( int ‘ 𝐽 ) ‘ 𝐴 ) )
5 4 3adant3 ⊢ ( ( 𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑋 ) → ( ( int ‘ 𝐽 ) ‘ ( 𝐴 ∩ 𝐵 ) ) ⊆ ( ( int ‘ 𝐽 ) ‘ 𝐴 ) )
6 inss2 ⊢ ( 𝐴 ∩ 𝐵 ) ⊆ 𝐵
7 1 ntrss ⊢ ( ( 𝐽 ∈ Top ∧ 𝐵 ⊆ 𝑋 ∧ ( 𝐴 ∩ 𝐵 ) ⊆ 𝐵 ) → ( ( int ‘ 𝐽 ) ‘ ( 𝐴 ∩ 𝐵 ) ) ⊆ ( ( int ‘ 𝐽 ) ‘ 𝐵 ) )
8 6 7 mp3an3 ⊢ ( ( 𝐽 ∈ Top ∧ 𝐵 ⊆ 𝑋 ) → ( ( int ‘ 𝐽 ) ‘ ( 𝐴 ∩ 𝐵 ) ) ⊆ ( ( int ‘ 𝐽 ) ‘ 𝐵 ) )
9 8 3adant2 ⊢ ( ( 𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑋 ) → ( ( int ‘ 𝐽 ) ‘ ( 𝐴 ∩ 𝐵 ) ) ⊆ ( ( int ‘ 𝐽 ) ‘ 𝐵 ) )
10 5 9 ssind ⊢ ( ( 𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑋 ) → ( ( int ‘ 𝐽 ) ‘ ( 𝐴 ∩ 𝐵 ) ) ⊆ ( ( ( int ‘ 𝐽 ) ‘ 𝐴 ) ∩ ( ( int ‘ 𝐽 ) ‘ 𝐵 ) ) )
11 simp1 ⊢ ( ( 𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑋 ) → 𝐽 ∈ Top )
12 ssinss1 ⊢ ( 𝐴 ⊆ 𝑋 → ( 𝐴 ∩ 𝐵 ) ⊆ 𝑋 )
13 12 3ad2ant2 ⊢ ( ( 𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑋 ) → ( 𝐴 ∩ 𝐵 ) ⊆ 𝑋 )
14 1 ntropn ⊢ ( ( 𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ) → ( ( int ‘ 𝐽 ) ‘ 𝐴 ) ∈ 𝐽 )
15 14 3adant3 ⊢ ( ( 𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑋 ) → ( ( int ‘ 𝐽 ) ‘ 𝐴 ) ∈ 𝐽 )
16 1 ntropn ⊢ ( ( 𝐽 ∈ Top ∧ 𝐵 ⊆ 𝑋 ) → ( ( int ‘ 𝐽 ) ‘ 𝐵 ) ∈ 𝐽 )
17 16 3adant2 ⊢ ( ( 𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑋 ) → ( ( int ‘ 𝐽 ) ‘ 𝐵 ) ∈ 𝐽 )
18 inopn ⊢ ( ( 𝐽 ∈ Top ∧ ( ( int ‘ 𝐽 ) ‘ 𝐴 ) ∈ 𝐽 ∧ ( ( int ‘ 𝐽 ) ‘ 𝐵 ) ∈ 𝐽 ) → ( ( ( int ‘ 𝐽 ) ‘ 𝐴 ) ∩ ( ( int ‘ 𝐽 ) ‘ 𝐵 ) ) ∈ 𝐽 )
19 11 15 17 18 syl3anc ⊢ ( ( 𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑋 ) → ( ( ( int ‘ 𝐽 ) ‘ 𝐴 ) ∩ ( ( int ‘ 𝐽 ) ‘ 𝐵 ) ) ∈ 𝐽 )
20 inss1 ⊢ ( ( ( int ‘ 𝐽 ) ‘ 𝐴 ) ∩ ( ( int ‘ 𝐽 ) ‘ 𝐵 ) ) ⊆ ( ( int ‘ 𝐽 ) ‘ 𝐴 )
21 1 ntrss2 ⊢ ( ( 𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ) → ( ( int ‘ 𝐽 ) ‘ 𝐴 ) ⊆ 𝐴 )
22 21 3adant3 ⊢ ( ( 𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑋 ) → ( ( int ‘ 𝐽 ) ‘ 𝐴 ) ⊆ 𝐴 )
23 20 22 sstrid ⊢ ( ( 𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑋 ) → ( ( ( int ‘ 𝐽 ) ‘ 𝐴 ) ∩ ( ( int ‘ 𝐽 ) ‘ 𝐵 ) ) ⊆ 𝐴 )
24 inss2 ⊢ ( ( ( int ‘ 𝐽 ) ‘ 𝐴 ) ∩ ( ( int ‘ 𝐽 ) ‘ 𝐵 ) ) ⊆ ( ( int ‘ 𝐽 ) ‘ 𝐵 )
25 1 ntrss2 ⊢ ( ( 𝐽 ∈ Top ∧ 𝐵 ⊆ 𝑋 ) → ( ( int ‘ 𝐽 ) ‘ 𝐵 ) ⊆ 𝐵 )
26 25 3adant2 ⊢ ( ( 𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑋 ) → ( ( int ‘ 𝐽 ) ‘ 𝐵 ) ⊆ 𝐵 )
27 24 26 sstrid ⊢ ( ( 𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑋 ) → ( ( ( int ‘ 𝐽 ) ‘ 𝐴 ) ∩ ( ( int ‘ 𝐽 ) ‘ 𝐵 ) ) ⊆ 𝐵 )
28 23 27 ssind ⊢ ( ( 𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑋 ) → ( ( ( int ‘ 𝐽 ) ‘ 𝐴 ) ∩ ( ( int ‘ 𝐽 ) ‘ 𝐵 ) ) ⊆ ( 𝐴 ∩ 𝐵 ) )
29 1 ssntr ⊢ ( ( ( 𝐽 ∈ Top ∧ ( 𝐴 ∩ 𝐵 ) ⊆ 𝑋 ) ∧ ( ( ( ( int ‘ 𝐽 ) ‘ 𝐴 ) ∩ ( ( int ‘ 𝐽 ) ‘ 𝐵 ) ) ∈ 𝐽 ∧ ( ( ( int ‘ 𝐽 ) ‘ 𝐴 ) ∩ ( ( int ‘ 𝐽 ) ‘ 𝐵 ) ) ⊆ ( 𝐴 ∩ 𝐵 ) ) ) → ( ( ( int ‘ 𝐽 ) ‘ 𝐴 ) ∩ ( ( int ‘ 𝐽 ) ‘ 𝐵 ) ) ⊆ ( ( int ‘ 𝐽 ) ‘ ( 𝐴 ∩ 𝐵 ) ) )
30 11 13 19 28 29 syl22anc ⊢ ( ( 𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑋 ) → ( ( ( int ‘ 𝐽 ) ‘ 𝐴 ) ∩ ( ( int ‘ 𝐽 ) ‘ 𝐵 ) ) ⊆ ( ( int ‘ 𝐽 ) ‘ ( 𝐴 ∩ 𝐵 ) ) )
31 10 30 eqssd ⊢ ( ( 𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑋 ) → ( ( int ‘ 𝐽 ) ‘ ( 𝐴 ∩ 𝐵 ) ) = ( ( ( int ‘ 𝐽 ) ‘ 𝐴 ) ∩ ( ( int ‘ 𝐽 ) ‘ 𝐵 ) ) )