neindisj2

Description: A point P belongs to the closure of a set S iff every neighborhood of P meets S . (Contributed by FL, 15-Sep-2013)

		Ref	Expression
	Hypothesis	tpnei.1	$⊢ X = ⋃ J$
	Assertion	neindisj2	$⊢ (J \in Top \land S \subseteq X \land P \in X) \to (P \in cls (J) (S) \leftrightarrow \forall n \in nei (J) (\{P\}) n \cap S \neq \emptyset)$

Proof

Step	Hyp	Ref	Expression
1		tpnei.1	$⊢ X = ⋃ J$
2	1	elcls	$⊢ (J \in Top \land S \subseteq X \land P \in X) \to (P \in cls (J) (S) \leftrightarrow \forall x \in J (P \in x \to x \cap S \neq \emptyset))$
3	1	isneip	$⊢ (J \in Top \land P \in X) \to (n \in nei (J) (\{P\}) \leftrightarrow (n \subseteq X \land \exists x \in J (P \in x \land x \subseteq n)))$
4		r19.29r	$⊢ (\exists x \in J (P \in x \land x \subseteq n) \land \forall x \in J (P \in x \to x \cap S \neq \emptyset)) \to \exists x \in J ((P \in x \land x \subseteq n) \land (P \in x \to x \cap S \neq \emptyset))$
5		pm3.35	$⊢ (P \in x \land (P \in x \to x \cap S \neq \emptyset)) \to x \cap S \neq \emptyset$
6		ssrin	$⊢ x \subseteq n \to x \cap S \subseteq n \cap S$
7		sseq2	$⊢ n \cap S = \emptyset \to (x \cap S \subseteq n \cap S \leftrightarrow x \cap S \subseteq \emptyset)$
8		ss0	$⊢ x \cap S \subseteq \emptyset \to x \cap S = \emptyset$
9	7 8	syl6bi	$⊢ n \cap S = \emptyset \to (x \cap S \subseteq n \cap S \to x \cap S = \emptyset)$
10	6 9	syl5com	$⊢ x \subseteq n \to (n \cap S = \emptyset \to x \cap S = \emptyset)$
11	10	necon3d	$⊢ x \subseteq n \to (x \cap S \neq \emptyset \to n \cap S \neq \emptyset)$
12	5 11	syl5com	$⊢ (P \in x \land (P \in x \to x \cap S \neq \emptyset)) \to (x \subseteq n \to n \cap S \neq \emptyset)$
13	12	ex	$⊢ P \in x \to ((P \in x \to x \cap S \neq \emptyset) \to (x \subseteq n \to n \cap S \neq \emptyset))$
14	13	com23	$⊢ P \in x \to (x \subseteq n \to ((P \in x \to x \cap S \neq \emptyset) \to n \cap S \neq \emptyset))$
15	14	imp31	$⊢ ((P \in x \land x \subseteq n) \land (P \in x \to x \cap S \neq \emptyset)) \to n \cap S \neq \emptyset$
16	15	rexlimivw	$⊢ \exists x \in J ((P \in x \land x \subseteq n) \land (P \in x \to x \cap S \neq \emptyset)) \to n \cap S \neq \emptyset$
17	4 16	syl	$⊢ (\exists x \in J (P \in x \land x \subseteq n) \land \forall x \in J (P \in x \to x \cap S \neq \emptyset)) \to n \cap S \neq \emptyset$
18	17	ex	$⊢ \exists x \in J (P \in x \land x \subseteq n) \to (\forall x \in J (P \in x \to x \cap S \neq \emptyset) \to n \cap S \neq \emptyset)$
19	18	adantl	$⊢ (n \subseteq X \land \exists x \in J (P \in x \land x \subseteq n)) \to (\forall x \in J (P \in x \to x \cap S \neq \emptyset) \to n \cap S \neq \emptyset)$
20	3 19	syl6bi	$⊢ (J \in Top \land P \in X) \to (n \in nei (J) (\{P\}) \to (\forall x \in J (P \in x \to x \cap S \neq \emptyset) \to n \cap S \neq \emptyset))$
21	20	3adant2	$⊢ (J \in Top \land S \subseteq X \land P \in X) \to (n \in nei (J) (\{P\}) \to (\forall x \in J (P \in x \to x \cap S \neq \emptyset) \to n \cap S \neq \emptyset))$
22	21	com23	$⊢ (J \in Top \land S \subseteq X \land P \in X) \to (\forall x \in J (P \in x \to x \cap S \neq \emptyset) \to (n \in nei (J) (\{P\}) \to n \cap S \neq \emptyset))$
23	22	imp	$⊢ ((J \in Top \land S \subseteq X \land P \in X) \land \forall x \in J (P \in x \to x \cap S \neq \emptyset)) \to (n \in nei (J) (\{P\}) \to n \cap S \neq \emptyset)$
24	23	ralrimiv	$⊢ ((J \in Top \land S \subseteq X \land P \in X) \land \forall x \in J (P \in x \to x \cap S \neq \emptyset)) \to \forall n \in nei (J) (\{P\}) n \cap S \neq \emptyset$
25		opnneip	$⊢ (J \in Top \land x \in J \land P \in x) \to x \in nei (J) (\{P\})$
26		ineq1	$⊢ n = x \to n \cap S = x \cap S$
27	26	neeq1d	$⊢ n = x \to (n \cap S \neq \emptyset \leftrightarrow x \cap S \neq \emptyset)$
28	27	rspccva	$⊢ (\forall n \in nei (J) (\{P\}) n \cap S \neq \emptyset \land x \in nei (J) (\{P\})) \to x \cap S \neq \emptyset$
29		idd	$⊢ (P \in X \land (J \in Top \land x \in J \land P \in x) \land S \subseteq X) \to (x \cap S \neq \emptyset \to x \cap S \neq \emptyset)$
30	29	3exp	$⊢ P \in X \to ((J \in Top \land x \in J \land P \in x) \to (S \subseteq X \to (x \cap S \neq \emptyset \to x \cap S \neq \emptyset)))$
31	30	com14	$⊢ x \cap S \neq \emptyset \to ((J \in Top \land x \in J \land P \in x) \to (S \subseteq X \to (P \in X \to x \cap S \neq \emptyset)))$
32	28 31	syl	$⊢ (\forall n \in nei (J) (\{P\}) n \cap S \neq \emptyset \land x \in nei (J) (\{P\})) \to ((J \in Top \land x \in J \land P \in x) \to (S \subseteq X \to (P \in X \to x \cap S \neq \emptyset)))$
33	32	ex	$⊢ \forall n \in nei (J) (\{P\}) n \cap S \neq \emptyset \to (x \in nei (J) (\{P\}) \to ((J \in Top \land x \in J \land P \in x) \to (S \subseteq X \to (P \in X \to x \cap S \neq \emptyset))))$
34	33	com3l	$⊢ x \in nei (J) (\{P\}) \to ((J \in Top \land x \in J \land P \in x) \to (\forall n \in nei (J) (\{P\}) n \cap S \neq \emptyset \to (S \subseteq X \to (P \in X \to x \cap S \neq \emptyset))))$
35	25 34	mpcom	$⊢ (J \in Top \land x \in J \land P \in x) \to (\forall n \in nei (J) (\{P\}) n \cap S \neq \emptyset \to (S \subseteq X \to (P \in X \to x \cap S \neq \emptyset)))$
36	35	3expia	$⊢ (J \in Top \land x \in J) \to (P \in x \to (\forall n \in nei (J) (\{P\}) n \cap S \neq \emptyset \to (S \subseteq X \to (P \in X \to x \cap S \neq \emptyset))))$
37	36	com25	$⊢ (J \in Top \land x \in J) \to (P \in X \to (\forall n \in nei (J) (\{P\}) n \cap S \neq \emptyset \to (S \subseteq X \to (P \in x \to x \cap S \neq \emptyset))))$
38	37	ex	$⊢ J \in Top \to (x \in J \to (P \in X \to (\forall n \in nei (J) (\{P\}) n \cap S \neq \emptyset \to (S \subseteq X \to (P \in x \to x \cap S \neq \emptyset)))))$
39	38	com25	$⊢ J \in Top \to (S \subseteq X \to (P \in X \to (\forall n \in nei (J) (\{P\}) n \cap S \neq \emptyset \to (x \in J \to (P \in x \to x \cap S \neq \emptyset)))))$
40	39	3imp1	$⊢ ((J \in Top \land S \subseteq X \land P \in X) \land \forall n \in nei (J) (\{P\}) n \cap S \neq \emptyset) \to (x \in J \to (P \in x \to x \cap S \neq \emptyset))$
41	40	ralrimiv	$⊢ ((J \in Top \land S \subseteq X \land P \in X) \land \forall n \in nei (J) (\{P\}) n \cap S \neq \emptyset) \to \forall x \in J (P \in x \to x \cap S \neq \emptyset)$
42	24 41	impbida	$⊢ (J \in Top \land S \subseteq X \land P \in X) \to (\forall x \in J (P \in x \to x \cap S \neq \emptyset) \leftrightarrow \forall n \in nei (J) (\{P\}) n \cap S \neq \emptyset)$
43	2 42	bitrd	$⊢ (J \in Top \land S \subseteq X \land P \in X) \to (P \in cls (J) (S) \leftrightarrow \forall n \in nei (J) (\{P\}) n \cap S \neq \emptyset)$

Metamath Proof Explorer

Theorem neindisj2

Proof