neifil

Description: The neighborhoods of a nonempty set is a filter. Example 2 of BourbakiTop1 p. I.36. (Contributed by FL, 18-Sep-2007) (Revised by Mario Carneiro, 23-Aug-2015)

		Ref	Expression
	Assertion	neifil	$⊢ (J \in TopOn (X) \land S \subseteq X \land S \neq \emptyset) \to nei (J) (S) \in Fil (X)$

Proof

Step	Hyp	Ref	Expression
1		toponuni	$⊢ J \in TopOn (X) \to X = ⋃ J$
2	1	adantr	$⊢ (J \in TopOn (X) \land S \subseteq X) \to X = ⋃ J$
3		topontop	$⊢ J \in TopOn (X) \to J \in Top$
4	3	adantr	$⊢ (J \in TopOn (X) \land S \subseteq X) \to J \in Top$
5		simpr	$⊢ (J \in TopOn (X) \land S \subseteq X) \to S \subseteq X$
6	5 2	sseqtrd	$⊢ (J \in TopOn (X) \land S \subseteq X) \to S \subseteq ⋃ J$
7		eqid	$⊢ ⋃ J = ⋃ J$
8	7	neiuni	$⊢ (J \in Top \land S \subseteq ⋃ J) \to ⋃ J = ⋃ nei (J) (S)$
9	4 6 8	syl2anc	$⊢ (J \in TopOn (X) \land S \subseteq X) \to ⋃ J = ⋃ nei (J) (S)$
10	2 9	eqtrd	$⊢ (J \in TopOn (X) \land S \subseteq X) \to X = ⋃ nei (J) (S)$
11		eqimss2	$⊢ X = ⋃ nei (J) (S) \to ⋃ nei (J) (S) \subseteq X$
12	10 11	syl	$⊢ (J \in TopOn (X) \land S \subseteq X) \to ⋃ nei (J) (S) \subseteq X$
13		sspwuni	$⊢ nei (J) (S) \subseteq 𝒫 X \leftrightarrow ⋃ nei (J) (S) \subseteq X$
14	12 13	sylibr	$⊢ (J \in TopOn (X) \land S \subseteq X) \to nei (J) (S) \subseteq 𝒫 X$
15	14	3adant3	$⊢ (J \in TopOn (X) \land S \subseteq X \land S \neq \emptyset) \to nei (J) (S) \subseteq 𝒫 X$
16		0nnei	$⊢ (J \in Top \land S \neq \emptyset) \to \neg \emptyset \in nei (J) (S)$
17	3 16	sylan	$⊢ (J \in TopOn (X) \land S \neq \emptyset) \to \neg \emptyset \in nei (J) (S)$
18	17	3adant2	$⊢ (J \in TopOn (X) \land S \subseteq X \land S \neq \emptyset) \to \neg \emptyset \in nei (J) (S)$
19	7	tpnei	$⊢ J \in Top \to (S \subseteq ⋃ J \leftrightarrow ⋃ J \in nei (J) (S))$
20	19	biimpa	$⊢ (J \in Top \land S \subseteq ⋃ J) \to ⋃ J \in nei (J) (S)$
21	4 6 20	syl2anc	$⊢ (J \in TopOn (X) \land S \subseteq X) \to ⋃ J \in nei (J) (S)$
22	2 21	eqeltrd	$⊢ (J \in TopOn (X) \land S \subseteq X) \to X \in nei (J) (S)$
23	22	3adant3	$⊢ (J \in TopOn (X) \land S \subseteq X \land S \neq \emptyset) \to X \in nei (J) (S)$
24	15 18 23	3jca	$⊢ (J \in TopOn (X) \land S \subseteq X \land S \neq \emptyset) \to (nei (J) (S) \subseteq 𝒫 X \land \neg \emptyset \in nei (J) (S) \land X \in nei (J) (S))$
25		elpwi	$⊢ x \in 𝒫 X \to x \subseteq X$
26	4	ad2antrr	$⊢ (((J \in TopOn (X) \land S \subseteq X) \land x \subseteq X) \land (y \in nei (J) (S) \land y \subseteq x)) \to J \in Top$
27		simprl	$⊢ (((J \in TopOn (X) \land S \subseteq X) \land x \subseteq X) \land (y \in nei (J) (S) \land y \subseteq x)) \to y \in nei (J) (S)$
28		simprr	$⊢ (((J \in TopOn (X) \land S \subseteq X) \land x \subseteq X) \land (y \in nei (J) (S) \land y \subseteq x)) \to y \subseteq x$
29		simplr	$⊢ (((J \in TopOn (X) \land S \subseteq X) \land x \subseteq X) \land (y \in nei (J) (S) \land y \subseteq x)) \to x \subseteq X$
30	2	ad2antrr	$⊢ (((J \in TopOn (X) \land S \subseteq X) \land x \subseteq X) \land (y \in nei (J) (S) \land y \subseteq x)) \to X = ⋃ J$
31	29 30	sseqtrd	$⊢ (((J \in TopOn (X) \land S \subseteq X) \land x \subseteq X) \land (y \in nei (J) (S) \land y \subseteq x)) \to x \subseteq ⋃ J$
32	7	ssnei2	$⊢ ((J \in Top \land y \in nei (J) (S)) \land (y \subseteq x \land x \subseteq ⋃ J)) \to x \in nei (J) (S)$
33	26 27 28 31 32	syl22anc	$⊢ (((J \in TopOn (X) \land S \subseteq X) \land x \subseteq X) \land (y \in nei (J) (S) \land y \subseteq x)) \to x \in nei (J) (S)$
34	33	rexlimdvaa	$⊢ ((J \in TopOn (X) \land S \subseteq X) \land x \subseteq X) \to (\exists y \in nei (J) (S) y \subseteq x \to x \in nei (J) (S))$
35	25 34	sylan2	$⊢ ((J \in TopOn (X) \land S \subseteq X) \land x \in 𝒫 X) \to (\exists y \in nei (J) (S) y \subseteq x \to x \in nei (J) (S))$
36	35	ralrimiva	$⊢ (J \in TopOn (X) \land S \subseteq X) \to \forall x \in 𝒫 X (\exists y \in nei (J) (S) y \subseteq x \to x \in nei (J) (S))$
37	36	3adant3	$⊢ (J \in TopOn (X) \land S \subseteq X \land S \neq \emptyset) \to \forall x \in 𝒫 X (\exists y \in nei (J) (S) y \subseteq x \to x \in nei (J) (S))$
38		innei	$⊢ (J \in Top \land x \in nei (J) (S) \land y \in nei (J) (S)) \to x \cap y \in nei (J) (S)$
39	38	3expib	$⊢ J \in Top \to ((x \in nei (J) (S) \land y \in nei (J) (S)) \to x \cap y \in nei (J) (S))$
40	3 39	syl	$⊢ J \in TopOn (X) \to ((x \in nei (J) (S) \land y \in nei (J) (S)) \to x \cap y \in nei (J) (S))$
41	40	3ad2ant1	$⊢ (J \in TopOn (X) \land S \subseteq X \land S \neq \emptyset) \to ((x \in nei (J) (S) \land y \in nei (J) (S)) \to x \cap y \in nei (J) (S))$
42	41	ralrimivv	$⊢ (J \in TopOn (X) \land S \subseteq X \land S \neq \emptyset) \to \forall x \in nei (J) (S) \forall y \in nei (J) (S) x \cap y \in nei (J) (S)$
43		isfil2	$⊢ nei (J) (S) \in Fil (X) \leftrightarrow ((nei (J) (S) \subseteq 𝒫 X \land \neg \emptyset \in nei (J) (S) \land X \in nei (J) (S)) \land \forall x \in 𝒫 X (\exists y \in nei (J) (S) y \subseteq x \to x \in nei (J) (S)) \land \forall x \in nei (J) (S) \forall y \in nei (J) (S) x \cap y \in nei (J) (S))$
44	24 37 42 43	syl3anbrc	$⊢ (J \in TopOn (X) \land S \subseteq X \land S \neq \emptyset) \to nei (J) (S) \in Fil (X)$

Metamath Proof Explorer

Theorem neifil

Proof