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 = ⋃ J$
	Assertion	ntrin	$⊢ (J \in Top \land A \subseteq X \land B \subseteq X) \to int (J) (A \cap B) = int (J) (A) \cap int (J) (B)$

Proof

Step	Hyp	Ref	Expression
1		clscld.1	$⊢ X = ⋃ J$
2		inss1	$⊢ A \cap B \subseteq A$
3	1	ntrss	$⊢ (J \in Top \land A \subseteq X \land A \cap B \subseteq A) \to int (J) (A \cap B) \subseteq int (J) (A)$
4	2 3	mp3an3	$⊢ (J \in Top \land A \subseteq X) \to int (J) (A \cap B) \subseteq int (J) (A)$
5	4	3adant3	$⊢ (J \in Top \land A \subseteq X \land B \subseteq X) \to int (J) (A \cap B) \subseteq int (J) (A)$
6		inss2	$⊢ A \cap B \subseteq B$
7	1	ntrss	$⊢ (J \in Top \land B \subseteq X \land A \cap B \subseteq B) \to int (J) (A \cap B) \subseteq int (J) (B)$
8	6 7	mp3an3	$⊢ (J \in Top \land B \subseteq X) \to int (J) (A \cap B) \subseteq int (J) (B)$
9	8	3adant2	$⊢ (J \in Top \land A \subseteq X \land B \subseteq X) \to int (J) (A \cap B) \subseteq int (J) (B)$
10	5 9	ssind	$⊢ (J \in Top \land A \subseteq X \land B \subseteq X) \to int (J) (A \cap B) \subseteq int (J) (A) \cap int (J) (B)$
11		simp1	$⊢ (J \in Top \land A \subseteq X \land B \subseteq X) \to J \in Top$
12		ssinss1	$⊢ A \subseteq X \to A \cap B \subseteq X$
13	12	3ad2ant2	$⊢ (J \in Top \land A \subseteq X \land B \subseteq X) \to A \cap B \subseteq X$
14	1	ntropn	$⊢ (J \in Top \land A \subseteq X) \to int (J) (A) \in J$
15	14	3adant3	$⊢ (J \in Top \land A \subseteq X \land B \subseteq X) \to int (J) (A) \in J$
16	1	ntropn	$⊢ (J \in Top \land B \subseteq X) \to int (J) (B) \in J$
17	16	3adant2	$⊢ (J \in Top \land A \subseteq X \land B \subseteq X) \to int (J) (B) \in J$
18		inopn	$⊢ (J \in Top \land int (J) (A) \in J \land int (J) (B) \in J) \to int (J) (A) \cap int (J) (B) \in J$
19	11 15 17 18	syl3anc	$⊢ (J \in Top \land A \subseteq X \land B \subseteq X) \to int (J) (A) \cap int (J) (B) \in J$
20		inss1	$⊢ int (J) (A) \cap int (J) (B) \subseteq int (J) (A)$
21	1	ntrss2	$⊢ (J \in Top \land A \subseteq X) \to int (J) (A) \subseteq A$
22	21	3adant3	$⊢ (J \in Top \land A \subseteq X \land B \subseteq X) \to int (J) (A) \subseteq A$
23	20 22	sstrid	$⊢ (J \in Top \land A \subseteq X \land B \subseteq X) \to int (J) (A) \cap int (J) (B) \subseteq A$
24		inss2	$⊢ int (J) (A) \cap int (J) (B) \subseteq int (J) (B)$
25	1	ntrss2	$⊢ (J \in Top \land B \subseteq X) \to int (J) (B) \subseteq B$
26	25	3adant2	$⊢ (J \in Top \land A \subseteq X \land B \subseteq X) \to int (J) (B) \subseteq B$
27	24 26	sstrid	$⊢ (J \in Top \land A \subseteq X \land B \subseteq X) \to int (J) (A) \cap int (J) (B) \subseteq B$
28	23 27	ssind	$⊢ (J \in Top \land A \subseteq X \land B \subseteq X) \to int (J) (A) \cap int (J) (B) \subseteq A \cap B$
29	1	ssntr	$⊢ ((J \in Top \land A \cap B \subseteq X) \land (int (J) (A) \cap int (J) (B) \in J \land int (J) (A) \cap int (J) (B) \subseteq A \cap B)) \to int (J) (A) \cap int (J) (B) \subseteq int (J) (A \cap B)$
30	11 13 19 28 29	syl22anc	$⊢ (J \in Top \land A \subseteq X \land B \subseteq X) \to int (J) (A) \cap int (J) (B) \subseteq int (J) (A \cap B)$
31	10 30	eqssd	$⊢ (J \in Top \land A \subseteq X \land B \subseteq X) \to int (J) (A \cap B) = int (J) (A) \cap int (J) (B)$

Metamath Proof Explorer

Theorem ntrin

Proof