neificl

Description: Neighborhoods are closed under finite intersection. (Contributed by Jeff Madsen, 2-Sep-2009) (Revised by Mario Carneiro, 25-Nov-2013)

		Ref	Expression
	Assertion	neificl	$⊢ ((J \in Top \land N \subseteq nei (J) (S)) \land (N \in Fin \land N \neq \emptyset)) \to ⋂ N \in nei (J) (S)$

Proof

Step	Hyp	Ref	Expression
1		simprl	$⊢ (N \subseteq nei (J) (S) \land (N \in Fin \land N \neq \emptyset)) \to N \in Fin$
2		innei	$⊢ (J \in Top \land x \in nei (J) (S) \land y \in nei (J) (S)) \to x \cap y \in nei (J) (S)$
3	2	3expib	$⊢ J \in Top \to ((x \in nei (J) (S) \land y \in nei (J) (S)) \to x \cap y \in nei (J) (S))$
4	3	ralrimivv	$⊢ J \in Top \to \forall x \in nei (J) (S) \forall y \in nei (J) (S) x \cap y \in nei (J) (S)$
5		fiint	$⊢ \forall x \in nei (J) (S) \forall y \in nei (J) (S) x \cap y \in nei (J) (S) \leftrightarrow \forall x ((x \subseteq nei (J) (S) \land x \neq \emptyset \land x \in Fin) \to ⋂ x \in nei (J) (S))$
6	4 5	sylib	$⊢ J \in Top \to \forall x ((x \subseteq nei (J) (S) \land x \neq \emptyset \land x \in Fin) \to ⋂ x \in nei (J) (S))$
7		sseq1	$⊢ x = N \to (x \subseteq nei (J) (S) \leftrightarrow N \subseteq nei (J) (S))$
8		neeq1	$⊢ x = N \to (x \neq \emptyset \leftrightarrow N \neq \emptyset)$
9		eleq1	$⊢ x = N \to (x \in Fin \leftrightarrow N \in Fin)$
10	7 8 9	3anbi123d	$⊢ x = N \to ((x \subseteq nei (J) (S) \land x \neq \emptyset \land x \in Fin) \leftrightarrow (N \subseteq nei (J) (S) \land N \neq \emptyset \land N \in Fin))$
11		3ancomb	$⊢ (N \subseteq nei (J) (S) \land N \neq \emptyset \land N \in Fin) \leftrightarrow (N \subseteq nei (J) (S) \land N \in Fin \land N \neq \emptyset)$
12		3anass	$⊢ (N \subseteq nei (J) (S) \land N \in Fin \land N \neq \emptyset) \leftrightarrow (N \subseteq nei (J) (S) \land (N \in Fin \land N \neq \emptyset))$
13	11 12	bitri	$⊢ (N \subseteq nei (J) (S) \land N \neq \emptyset \land N \in Fin) \leftrightarrow (N \subseteq nei (J) (S) \land (N \in Fin \land N \neq \emptyset))$
14	10 13	bitrdi	$⊢ x = N \to ((x \subseteq nei (J) (S) \land x \neq \emptyset \land x \in Fin) \leftrightarrow (N \subseteq nei (J) (S) \land (N \in Fin \land N \neq \emptyset)))$
15		inteq	$⊢ x = N \to ⋂ x = ⋂ N$
16	15	eleq1d	$⊢ x = N \to (⋂ x \in nei (J) (S) \leftrightarrow ⋂ N \in nei (J) (S))$
17	14 16	imbi12d	$⊢ x = N \to (((x \subseteq nei (J) (S) \land x \neq \emptyset \land x \in Fin) \to ⋂ x \in nei (J) (S)) \leftrightarrow ((N \subseteq nei (J) (S) \land (N \in Fin \land N \neq \emptyset)) \to ⋂ N \in nei (J) (S)))$
18	17	spcgv	$⊢ N \in Fin \to (\forall x ((x \subseteq nei (J) (S) \land x \neq \emptyset \land x \in Fin) \to ⋂ x \in nei (J) (S)) \to ((N \subseteq nei (J) (S) \land (N \in Fin \land N \neq \emptyset)) \to ⋂ N \in nei (J) (S)))$
19	6 18	syl5	$⊢ N \in Fin \to (J \in Top \to ((N \subseteq nei (J) (S) \land (N \in Fin \land N \neq \emptyset)) \to ⋂ N \in nei (J) (S)))$
20	19	com3l	$⊢ J \in Top \to ((N \subseteq nei (J) (S) \land (N \in Fin \land N \neq \emptyset)) \to (N \in Fin \to ⋂ N \in nei (J) (S)))$
21	1 20	mpdi	$⊢ J \in Top \to ((N \subseteq nei (J) (S) \land (N \in Fin \land N \neq \emptyset)) \to ⋂ N \in nei (J) (S))$
22	21	impl	$⊢ ((J \in Top \land N \subseteq nei (J) (S)) \land (N \in Fin \land N \neq \emptyset)) \to ⋂ N \in nei (J) (S)$

Metamath Proof Explorer

Theorem neificl

Proof