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 ‘ 𝐽 ) ‘ 𝐵 ) ) )