neips

Description: A neighborhood of a set is a neighborhood of every point in the set. Proposition 1 of BourbakiTop1 p. I.2. (Contributed by FL, 16-Nov-2006)

		Ref	Expression
	Hypothesis	neips.1	$⊢ X = ⋃ J$
	Assertion	neips	$⊢ (J \in Top \land S \subseteq X \land S \neq \emptyset) \to (N \in nei (J) (S) \leftrightarrow \forall p \in S N \in nei (J) (\{p\}))$

Proof

Step	Hyp	Ref	Expression
1		neips.1	$⊢ X = ⋃ J$
2		snssi	$⊢ p \in S \to \{p\} \subseteq S$
3		neiss	$⊢ (J \in Top \land N \in nei (J) (S) \land \{p\} \subseteq S) \to N \in nei (J) (\{p\})$
4	2 3	syl3an3	$⊢ (J \in Top \land N \in nei (J) (S) \land p \in S) \to N \in nei (J) (\{p\})$
5	4	3exp	$⊢ J \in Top \to (N \in nei (J) (S) \to (p \in S \to N \in nei (J) (\{p\})))$
6	5	ralrimdv	$⊢ J \in Top \to (N \in nei (J) (S) \to \forall p \in S N \in nei (J) (\{p\}))$
7	6	3ad2ant1	$⊢ (J \in Top \land S \subseteq X \land S \neq \emptyset) \to (N \in nei (J) (S) \to \forall p \in S N \in nei (J) (\{p\}))$
8		r19.28zv	$⊢ S \neq \emptyset \to (\forall p \in S (N \subseteq X \land \exists g \in J (p \in g \land g \subseteq N)) \leftrightarrow (N \subseteq X \land \forall p \in S \exists g \in J (p \in g \land g \subseteq N)))$
9	8	3ad2ant3	$⊢ (J \in Top \land S \subseteq X \land S \neq \emptyset) \to (\forall p \in S (N \subseteq X \land \exists g \in J (p \in g \land g \subseteq N)) \leftrightarrow (N \subseteq X \land \forall p \in S \exists g \in J (p \in g \land g \subseteq N)))$
10		ssrab2	$⊢ \{v \in J \| v \subseteq N\} \subseteq J$
11		uniopn	$⊢ (J \in Top \land \{v \in J \| v \subseteq N\} \subseteq J) \to ⋃ \{v \in J \| v \subseteq N\} \in J$
12	10 11	mpan2	$⊢ J \in Top \to ⋃ \{v \in J \| v \subseteq N\} \in J$
13	12	ad2antrr	$⊢ ((J \in Top \land S \subseteq X) \land \forall p \in S \exists g \in J (p \in g \land g \subseteq N)) \to ⋃ \{v \in J \| v \subseteq N\} \in J$
14		sseq1	$⊢ v = g \to (v \subseteq N \leftrightarrow g \subseteq N)$
15	14	elrab	$⊢ g \in \{v \in J \| v \subseteq N\} \leftrightarrow (g \in J \land g \subseteq N)$
16		elunii	$⊢ (p \in g \land g \in \{v \in J \| v \subseteq N\}) \to p \in ⋃ \{v \in J \| v \subseteq N\}$
17	15 16	sylan2br	$⊢ (p \in g \land (g \in J \land g \subseteq N)) \to p \in ⋃ \{v \in J \| v \subseteq N\}$
18	17	an12s	$⊢ (g \in J \land (p \in g \land g \subseteq N)) \to p \in ⋃ \{v \in J \| v \subseteq N\}$
19	18	rexlimiva	$⊢ \exists g \in J (p \in g \land g \subseteq N) \to p \in ⋃ \{v \in J \| v \subseteq N\}$
20	19	ralimi	$⊢ \forall p \in S \exists g \in J (p \in g \land g \subseteq N) \to \forall p \in S p \in ⋃ \{v \in J \| v \subseteq N\}$
21		dfss3	$⊢ S \subseteq ⋃ \{v \in J \| v \subseteq N\} \leftrightarrow \forall p \in S p \in ⋃ \{v \in J \| v \subseteq N\}$
22	20 21	sylibr	$⊢ \forall p \in S \exists g \in J (p \in g \land g \subseteq N) \to S \subseteq ⋃ \{v \in J \| v \subseteq N\}$
23	22	adantl	$⊢ ((J \in Top \land S \subseteq X) \land \forall p \in S \exists g \in J (p \in g \land g \subseteq N)) \to S \subseteq ⋃ \{v \in J \| v \subseteq N\}$
24		unissb	$⊢ ⋃ \{v \in J \| v \subseteq N\} \subseteq N \leftrightarrow \forall h \in \{v \in J \| v \subseteq N\} h \subseteq N$
25		sseq1	$⊢ v = h \to (v \subseteq N \leftrightarrow h \subseteq N)$
26	25	elrab	$⊢ h \in \{v \in J \| v \subseteq N\} \leftrightarrow (h \in J \land h \subseteq N)$
27	26	simprbi	$⊢ h \in \{v \in J \| v \subseteq N\} \to h \subseteq N$
28	24 27	mprgbir	$⊢ ⋃ \{v \in J \| v \subseteq N\} \subseteq N$
29	23 28	jctir	$⊢ ((J \in Top \land S \subseteq X) \land \forall p \in S \exists g \in J (p \in g \land g \subseteq N)) \to (S \subseteq ⋃ \{v \in J \| v \subseteq N\} \land ⋃ \{v \in J \| v \subseteq N\} \subseteq N)$
30		sseq2	$⊢ h = ⋃ \{v \in J \| v \subseteq N\} \to (S \subseteq h \leftrightarrow S \subseteq ⋃ \{v \in J \| v \subseteq N\})$
31		sseq1	$⊢ h = ⋃ \{v \in J \| v \subseteq N\} \to (h \subseteq N \leftrightarrow ⋃ \{v \in J \| v \subseteq N\} \subseteq N)$
32	30 31	anbi12d	$⊢ h = ⋃ \{v \in J \| v \subseteq N\} \to ((S \subseteq h \land h \subseteq N) \leftrightarrow (S \subseteq ⋃ \{v \in J \| v \subseteq N\} \land ⋃ \{v \in J \| v \subseteq N\} \subseteq N))$
33	32	rspcev	$⊢ (⋃ \{v \in J \| v \subseteq N\} \in J \land (S \subseteq ⋃ \{v \in J \| v \subseteq N\} \land ⋃ \{v \in J \| v \subseteq N\} \subseteq N)) \to \exists h \in J (S \subseteq h \land h \subseteq N)$
34	13 29 33	syl2anc	$⊢ ((J \in Top \land S \subseteq X) \land \forall p \in S \exists g \in J (p \in g \land g \subseteq N)) \to \exists h \in J (S \subseteq h \land h \subseteq N)$
35	34	ex	$⊢ (J \in Top \land S \subseteq X) \to (\forall p \in S \exists g \in J (p \in g \land g \subseteq N) \to \exists h \in J (S \subseteq h \land h \subseteq N))$
36	35	anim2d	$⊢ (J \in Top \land S \subseteq X) \to ((N \subseteq X \land \forall p \in S \exists g \in J (p \in g \land g \subseteq N)) \to (N \subseteq X \land \exists h \in J (S \subseteq h \land h \subseteq N)))$
37	36	3adant3	$⊢ (J \in Top \land S \subseteq X \land S \neq \emptyset) \to ((N \subseteq X \land \forall p \in S \exists g \in J (p \in g \land g \subseteq N)) \to (N \subseteq X \land \exists h \in J (S \subseteq h \land h \subseteq N)))$
38	9 37	sylbid	$⊢ (J \in Top \land S \subseteq X \land S \neq \emptyset) \to (\forall p \in S (N \subseteq X \land \exists g \in J (p \in g \land g \subseteq N)) \to (N \subseteq X \land \exists h \in J (S \subseteq h \land h \subseteq N)))$
39		ssel2	$⊢ (S \subseteq X \land p \in S) \to p \in X$
40	1	isneip	$⊢ (J \in Top \land p \in X) \to (N \in nei (J) (\{p\}) \leftrightarrow (N \subseteq X \land \exists g \in J (p \in g \land g \subseteq N)))$
41	39 40	sylan2	$⊢ (J \in Top \land (S \subseteq X \land p \in S)) \to (N \in nei (J) (\{p\}) \leftrightarrow (N \subseteq X \land \exists g \in J (p \in g \land g \subseteq N)))$
42	41	anassrs	$⊢ ((J \in Top \land S \subseteq X) \land p \in S) \to (N \in nei (J) (\{p\}) \leftrightarrow (N \subseteq X \land \exists g \in J (p \in g \land g \subseteq N)))$
43	42	ralbidva	$⊢ (J \in Top \land S \subseteq X) \to (\forall p \in S N \in nei (J) (\{p\}) \leftrightarrow \forall p \in S (N \subseteq X \land \exists g \in J (p \in g \land g \subseteq N)))$
44	43	3adant3	$⊢ (J \in Top \land S \subseteq X \land S \neq \emptyset) \to (\forall p \in S N \in nei (J) (\{p\}) \leftrightarrow \forall p \in S (N \subseteq X \land \exists g \in J (p \in g \land g \subseteq N)))$
45	1	isnei	$⊢ (J \in Top \land S \subseteq X) \to (N \in nei (J) (S) \leftrightarrow (N \subseteq X \land \exists h \in J (S \subseteq h \land h \subseteq N)))$
46	45	3adant3	$⊢ (J \in Top \land S \subseteq X \land S \neq \emptyset) \to (N \in nei (J) (S) \leftrightarrow (N \subseteq X \land \exists h \in J (S \subseteq h \land h \subseteq N)))$
47	38 44 46	3imtr4d	$⊢ (J \in Top \land S \subseteq X \land S \neq \emptyset) \to (\forall p \in S N \in nei (J) (\{p\}) \to N \in nei (J) (S))$
48	7 47	impbid	$⊢ (J \in Top \land S \subseteq X \land S \neq \emptyset) \to (N \in nei (J) (S) \leftrightarrow \forall p \in S N \in nei (J) (\{p\}))$

Metamath Proof Explorer

Theorem neips

Proof