neiin

Description: Two neighborhoods intersect to form a neighborhood of the intersection. (Contributed by Jeff Hankins, 31-Aug-2009)

		Ref	Expression
	Assertion	neiin	$⊢ (J \in Top \land M \in nei (J) (A) \land N \in nei (J) (B)) \to M \cap N \in nei (J) (A \cap B)$

Proof

Step	Hyp	Ref	Expression
1		simpr	$⊢ (J \in Top \land M \in nei (J) (A)) \to M \in nei (J) (A)$
2		simpl	$⊢ (J \in Top \land M \in nei (J) (A)) \to J \in Top$
3		eqid	$⊢ ⋃ J = ⋃ J$
4	3	neiss2	$⊢ (J \in Top \land M \in nei (J) (A)) \to A \subseteq ⋃ J$
5	3	neii1	$⊢ (J \in Top \land M \in nei (J) (A)) \to M \subseteq ⋃ J$
6	3	neiint	$⊢ (J \in Top \land A \subseteq ⋃ J \land M \subseteq ⋃ J) \to (M \in nei (J) (A) \leftrightarrow A \subseteq int (J) (M))$
7	2 4 5 6	syl3anc	$⊢ (J \in Top \land M \in nei (J) (A)) \to (M \in nei (J) (A) \leftrightarrow A \subseteq int (J) (M))$
8	1 7	mpbid	$⊢ (J \in Top \land M \in nei (J) (A)) \to A \subseteq int (J) (M)$
9		ssinss1	$⊢ A \subseteq int (J) (M) \to A \cap B \subseteq int (J) (M)$
10	8 9	syl	$⊢ (J \in Top \land M \in nei (J) (A)) \to A \cap B \subseteq int (J) (M)$
11	10	3adant3	$⊢ (J \in Top \land M \in nei (J) (A) \land N \in nei (J) (B)) \to A \cap B \subseteq int (J) (M)$
12		inss2	$⊢ A \cap B \subseteq B$
13		simpr	$⊢ (J \in Top \land N \in nei (J) (B)) \to N \in nei (J) (B)$
14		simpl	$⊢ (J \in Top \land N \in nei (J) (B)) \to J \in Top$
15	3	neiss2	$⊢ (J \in Top \land N \in nei (J) (B)) \to B \subseteq ⋃ J$
16	3	neii1	$⊢ (J \in Top \land N \in nei (J) (B)) \to N \subseteq ⋃ J$
17	3	neiint	$⊢ (J \in Top \land B \subseteq ⋃ J \land N \subseteq ⋃ J) \to (N \in nei (J) (B) \leftrightarrow B \subseteq int (J) (N))$
18	14 15 16 17	syl3anc	$⊢ (J \in Top \land N \in nei (J) (B)) \to (N \in nei (J) (B) \leftrightarrow B \subseteq int (J) (N))$
19	13 18	mpbid	$⊢ (J \in Top \land N \in nei (J) (B)) \to B \subseteq int (J) (N)$
20	19	3adant2	$⊢ (J \in Top \land M \in nei (J) (A) \land N \in nei (J) (B)) \to B \subseteq int (J) (N)$
21	12 20	sstrid	$⊢ (J \in Top \land M \in nei (J) (A) \land N \in nei (J) (B)) \to A \cap B \subseteq int (J) (N)$
22	11 21	ssind	$⊢ (J \in Top \land M \in nei (J) (A) \land N \in nei (J) (B)) \to A \cap B \subseteq int (J) (M) \cap int (J) (N)$
23		simp1	$⊢ (J \in Top \land M \in nei (J) (A) \land N \in nei (J) (B)) \to J \in Top$
24	5	3adant3	$⊢ (J \in Top \land M \in nei (J) (A) \land N \in nei (J) (B)) \to M \subseteq ⋃ J$
25	16	3adant2	$⊢ (J \in Top \land M \in nei (J) (A) \land N \in nei (J) (B)) \to N \subseteq ⋃ J$
26	3	ntrin	$⊢ (J \in Top \land M \subseteq ⋃ J \land N \subseteq ⋃ J) \to int (J) (M \cap N) = int (J) (M) \cap int (J) (N)$
27	23 24 25 26	syl3anc	$⊢ (J \in Top \land M \in nei (J) (A) \land N \in nei (J) (B)) \to int (J) (M \cap N) = int (J) (M) \cap int (J) (N)$
28	22 27	sseqtrrd	$⊢ (J \in Top \land M \in nei (J) (A) \land N \in nei (J) (B)) \to A \cap B \subseteq int (J) (M \cap N)$
29		ssinss1	$⊢ A \subseteq ⋃ J \to A \cap B \subseteq ⋃ J$
30	4 29	syl	$⊢ (J \in Top \land M \in nei (J) (A)) \to A \cap B \subseteq ⋃ J$
31		ssinss1	$⊢ M \subseteq ⋃ J \to M \cap N \subseteq ⋃ J$
32	5 31	syl	$⊢ (J \in Top \land M \in nei (J) (A)) \to M \cap N \subseteq ⋃ J$
33	3	neiint	$⊢ (J \in Top \land A \cap B \subseteq ⋃ J \land M \cap N \subseteq ⋃ J) \to (M \cap N \in nei (J) (A \cap B) \leftrightarrow A \cap B \subseteq int (J) (M \cap N))$
34	2 30 32 33	syl3anc	$⊢ (J \in Top \land M \in nei (J) (A)) \to (M \cap N \in nei (J) (A \cap B) \leftrightarrow A \cap B \subseteq int (J) (M \cap N))$
35	34	3adant3	$⊢ (J \in Top \land M \in nei (J) (A) \land N \in nei (J) (B)) \to (M \cap N \in nei (J) (A \cap B) \leftrightarrow A \cap B \subseteq int (J) (M \cap N))$
36	28 35	mpbird	$⊢ (J \in Top \land M \in nei (J) (A) \land N \in nei (J) (B)) \to M \cap N \in nei (J) (A \cap B)$

Metamath Proof Explorer

Theorem neiin

Proof