innei

Description: The intersection of two neighborhoods of a set is also a neighborhood of the set. Generalization to subsets of Property V_ii of BourbakiTop1 p. I.3 for binary intersections. (Contributed by FL, 28-Sep-2006)

		Ref	Expression
	Assertion	innei	$⊢ (J \in Top \land N \in nei (J) (S) \land M \in nei (J) (S)) \to N \cap M \in nei (J) (S)$

Proof

Step	Hyp	Ref	Expression
1		eqid	$⊢ ⋃ J = ⋃ J$
2	1	neii1	$⊢ (J \in Top \land N \in nei (J) (S)) \to N \subseteq ⋃ J$
3		ssinss1	$⊢ N \subseteq ⋃ J \to N \cap M \subseteq ⋃ J$
4	2 3	syl	$⊢ (J \in Top \land N \in nei (J) (S)) \to N \cap M \subseteq ⋃ J$
5	4	3adant3	$⊢ (J \in Top \land N \in nei (J) (S) \land M \in nei (J) (S)) \to N \cap M \subseteq ⋃ J$
6		neii2	$⊢ (J \in Top \land N \in nei (J) (S)) \to \exists h \in J (S \subseteq h \land h \subseteq N)$
7		neii2	$⊢ (J \in Top \land M \in nei (J) (S)) \to \exists v \in J (S \subseteq v \land v \subseteq M)$
8	6 7	anim12dan	$⊢ (J \in Top \land (N \in nei (J) (S) \land M \in nei (J) (S))) \to (\exists h \in J (S \subseteq h \land h \subseteq N) \land \exists v \in J (S \subseteq v \land v \subseteq M))$
9		inopn	$⊢ (J \in Top \land h \in J \land v \in J) \to h \cap v \in J$
10	9	3expa	$⊢ ((J \in Top \land h \in J) \land v \in J) \to h \cap v \in J$
11		ssin	$⊢ (S \subseteq h \land S \subseteq v) \leftrightarrow S \subseteq h \cap v$
12	11	biimpi	$⊢ (S \subseteq h \land S \subseteq v) \to S \subseteq h \cap v$
13		ss2in	$⊢ (h \subseteq N \land v \subseteq M) \to h \cap v \subseteq N \cap M$
14	12 13	anim12i	$⊢ ((S \subseteq h \land S \subseteq v) \land (h \subseteq N \land v \subseteq M)) \to (S \subseteq h \cap v \land h \cap v \subseteq N \cap M)$
15	14	an4s	$⊢ ((S \subseteq h \land h \subseteq N) \land (S \subseteq v \land v \subseteq M)) \to (S \subseteq h \cap v \land h \cap v \subseteq N \cap M)$
16		sseq2	$⊢ g = h \cap v \to (S \subseteq g \leftrightarrow S \subseteq h \cap v)$
17		sseq1	$⊢ g = h \cap v \to (g \subseteq N \cap M \leftrightarrow h \cap v \subseteq N \cap M)$
18	16 17	anbi12d	$⊢ g = h \cap v \to ((S \subseteq g \land g \subseteq N \cap M) \leftrightarrow (S \subseteq h \cap v \land h \cap v \subseteq N \cap M))$
19	18	rspcev	$⊢ (h \cap v \in J \land (S \subseteq h \cap v \land h \cap v \subseteq N \cap M)) \to \exists g \in J (S \subseteq g \land g \subseteq N \cap M)$
20	10 15 19	syl2an	$⊢ (((J \in Top \land h \in J) \land v \in J) \land ((S \subseteq h \land h \subseteq N) \land (S \subseteq v \land v \subseteq M))) \to \exists g \in J (S \subseteq g \land g \subseteq N \cap M)$
21	20	expr	$⊢ (((J \in Top \land h \in J) \land v \in J) \land (S \subseteq h \land h \subseteq N)) \to ((S \subseteq v \land v \subseteq M) \to \exists g \in J (S \subseteq g \land g \subseteq N \cap M))$
22	21	an32s	$⊢ (((J \in Top \land h \in J) \land (S \subseteq h \land h \subseteq N)) \land v \in J) \to ((S \subseteq v \land v \subseteq M) \to \exists g \in J (S \subseteq g \land g \subseteq N \cap M))$
23	22	rexlimdva	$⊢ ((J \in Top \land h \in J) \land (S \subseteq h \land h \subseteq N)) \to (\exists v \in J (S \subseteq v \land v \subseteq M) \to \exists g \in J (S \subseteq g \land g \subseteq N \cap M))$
24	23	rexlimdva2	$⊢ J \in Top \to (\exists h \in J (S \subseteq h \land h \subseteq N) \to (\exists v \in J (S \subseteq v \land v \subseteq M) \to \exists g \in J (S \subseteq g \land g \subseteq N \cap M)))$
25	24	imp32	$⊢ (J \in Top \land (\exists h \in J (S \subseteq h \land h \subseteq N) \land \exists v \in J (S \subseteq v \land v \subseteq M))) \to \exists g \in J (S \subseteq g \land g \subseteq N \cap M)$
26	8 25	syldan	$⊢ (J \in Top \land (N \in nei (J) (S) \land M \in nei (J) (S))) \to \exists g \in J (S \subseteq g \land g \subseteq N \cap M)$
27	26	3impb	$⊢ (J \in Top \land N \in nei (J) (S) \land M \in nei (J) (S)) \to \exists g \in J (S \subseteq g \land g \subseteq N \cap M)$
28	1	neiss2	$⊢ (J \in Top \land N \in nei (J) (S)) \to S \subseteq ⋃ J$
29	1	isnei	$⊢ (J \in Top \land S \subseteq ⋃ J) \to (N \cap M \in nei (J) (S) \leftrightarrow (N \cap M \subseteq ⋃ J \land \exists g \in J (S \subseteq g \land g \subseteq N \cap M)))$
30	28 29	syldan	$⊢ (J \in Top \land N \in nei (J) (S)) \to (N \cap M \in nei (J) (S) \leftrightarrow (N \cap M \subseteq ⋃ J \land \exists g \in J (S \subseteq g \land g \subseteq N \cap M)))$
31	30	3adant3	$⊢ (J \in Top \land N \in nei (J) (S) \land M \in nei (J) (S)) \to (N \cap M \in nei (J) (S) \leftrightarrow (N \cap M \subseteq ⋃ J \land \exists g \in J (S \subseteq g \land g \subseteq N \cap M)))$
32	5 27 31	mpbir2and	$⊢ (J \in Top \land N \in nei (J) (S) \land M \in nei (J) (S)) \to N \cap M \in nei (J) (S)$

Metamath Proof Explorer

Theorem innei

Proof