neissex

Description: For any neighborhood N of S , there is a neighborhood x of S such that N is a neighborhood of all subsets of x . Generalization to subsets of Property V_iv of BourbakiTop1 p. I.3. (Contributed by FL, 2-Oct-2006)

		Ref	Expression
	Assertion	neissex	$⊢ (J \in Top \land N \in nei (J) (S)) \to \exists x \in nei (J) (S) \forall y (y \subseteq x \to N \in nei (J) (y))$

Proof

Step	Hyp	Ref	Expression
1		neii2	$⊢ (J \in Top \land N \in nei (J) (S)) \to \exists x \in J (S \subseteq x \land x \subseteq N)$
2		opnneiss	$⊢ (J \in Top \land x \in J \land S \subseteq x) \to x \in nei (J) (S)$
3	2	3expb	$⊢ (J \in Top \land (x \in J \land S \subseteq x)) \to x \in nei (J) (S)$
4	3	adantrrr	$⊢ (J \in Top \land (x \in J \land (S \subseteq x \land x \subseteq N))) \to x \in nei (J) (S)$
5	4	adantlr	$⊢ ((J \in Top \land N \in nei (J) (S)) \land (x \in J \land (S \subseteq x \land x \subseteq N))) \to x \in nei (J) (S)$
6		simplll	$⊢ (((J \in Top \land N \in nei (J) (S)) \land (x \in J \land x \subseteq N)) \land y \subseteq x) \to J \in Top$
7		simpll	$⊢ ((J \in Top \land N \in nei (J) (S)) \land x \in J) \to J \in Top$
8		simpr	$⊢ ((J \in Top \land N \in nei (J) (S)) \land x \in J) \to x \in J$
9		eqid	$⊢ ⋃ J = ⋃ J$
10	9	neii1	$⊢ (J \in Top \land N \in nei (J) (S)) \to N \subseteq ⋃ J$
11	10	adantr	$⊢ ((J \in Top \land N \in nei (J) (S)) \land x \in J) \to N \subseteq ⋃ J$
12	9	opnssneib	$⊢ (J \in Top \land x \in J \land N \subseteq ⋃ J) \to (x \subseteq N \leftrightarrow N \in nei (J) (x))$
13	7 8 11 12	syl3anc	$⊢ ((J \in Top \land N \in nei (J) (S)) \land x \in J) \to (x \subseteq N \leftrightarrow N \in nei (J) (x))$
14	13	biimpa	$⊢ (((J \in Top \land N \in nei (J) (S)) \land x \in J) \land x \subseteq N) \to N \in nei (J) (x)$
15	14	anasss	$⊢ ((J \in Top \land N \in nei (J) (S)) \land (x \in J \land x \subseteq N)) \to N \in nei (J) (x)$
16	15	adantr	$⊢ (((J \in Top \land N \in nei (J) (S)) \land (x \in J \land x \subseteq N)) \land y \subseteq x) \to N \in nei (J) (x)$
17		simpr	$⊢ (((J \in Top \land N \in nei (J) (S)) \land (x \in J \land x \subseteq N)) \land y \subseteq x) \to y \subseteq x$
18		neiss	$⊢ (J \in Top \land N \in nei (J) (x) \land y \subseteq x) \to N \in nei (J) (y)$
19	6 16 17 18	syl3anc	$⊢ (((J \in Top \land N \in nei (J) (S)) \land (x \in J \land x \subseteq N)) \land y \subseteq x) \to N \in nei (J) (y)$
20	19	ex	$⊢ ((J \in Top \land N \in nei (J) (S)) \land (x \in J \land x \subseteq N)) \to (y \subseteq x \to N \in nei (J) (y))$
21	20	adantrrl	$⊢ ((J \in Top \land N \in nei (J) (S)) \land (x \in J \land (S \subseteq x \land x \subseteq N))) \to (y \subseteq x \to N \in nei (J) (y))$
22	21	alrimiv	$⊢ ((J \in Top \land N \in nei (J) (S)) \land (x \in J \land (S \subseteq x \land x \subseteq N))) \to \forall y (y \subseteq x \to N \in nei (J) (y))$
23	1 5 22	reximssdv	$⊢ (J \in Top \land N \in nei (J) (S)) \to \exists x \in nei (J) (S) \forall y (y \subseteq x \to N \in nei (J) (y))$

Metamath Proof Explorer

Theorem neissex

Proof