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