opnnei

Description: A set is open iff it is a neighborhood of all of its points. (Contributed by Jeff Hankins, 15-Sep-2009)

		Ref	Expression
	Assertion	opnnei	$⊢ J \in Top \to (S \in J \leftrightarrow \forall x \in S S \in nei (J) (\{x\}))$

Proof

Step	Hyp	Ref	Expression
1		0opn	$⊢ J \in Top \to \emptyset \in J$
2	1	adantr	$⊢ (J \in Top \land S = \emptyset) \to \emptyset \in J$
3		eleq1	$⊢ S = \emptyset \to (S \in J \leftrightarrow \emptyset \in J)$
4	3	adantl	$⊢ (J \in Top \land S = \emptyset) \to (S \in J \leftrightarrow \emptyset \in J)$
5	2 4	mpbird	$⊢ (J \in Top \land S = \emptyset) \to S \in J$
6		rzal	$⊢ S = \emptyset \to \forall x \in S S \in nei (J) (\{x\})$
7	6	adantl	$⊢ (J \in Top \land S = \emptyset) \to \forall x \in S S \in nei (J) (\{x\})$
8	5 7	2thd	$⊢ (J \in Top \land S = \emptyset) \to (S \in J \leftrightarrow \forall x \in S S \in nei (J) (\{x\}))$
9		opnneip	$⊢ (J \in Top \land S \in J \land x \in S) \to S \in nei (J) (\{x\})$
10	9	3expia	$⊢ (J \in Top \land S \in J) \to (x \in S \to S \in nei (J) (\{x\}))$
11	10	ralrimiv	$⊢ (J \in Top \land S \in J) \to \forall x \in S S \in nei (J) (\{x\})$
12	11	ex	$⊢ J \in Top \to (S \in J \to \forall x \in S S \in nei (J) (\{x\}))$
13	12	adantr	$⊢ (J \in Top \land \neg S = \emptyset) \to (S \in J \to \forall x \in S S \in nei (J) (\{x\}))$
14		df-ne	$⊢ S \neq \emptyset \leftrightarrow \neg S = \emptyset$
15		r19.2z	$⊢ (S \neq \emptyset \land \forall x \in S S \in nei (J) (\{x\})) \to \exists x \in S S \in nei (J) (\{x\})$
16	15	ex	$⊢ S \neq \emptyset \to (\forall x \in S S \in nei (J) (\{x\}) \to \exists x \in S S \in nei (J) (\{x\}))$
17	14 16	sylbir	$⊢ \neg S = \emptyset \to (\forall x \in S S \in nei (J) (\{x\}) \to \exists x \in S S \in nei (J) (\{x\}))$
18		eqid	$⊢ ⋃ J = ⋃ J$
19	18	neii1	$⊢ (J \in Top \land S \in nei (J) (\{x\})) \to S \subseteq ⋃ J$
20	19	ex	$⊢ J \in Top \to (S \in nei (J) (\{x\}) \to S \subseteq ⋃ J)$
21	20	rexlimdvw	$⊢ J \in Top \to (\exists x \in S S \in nei (J) (\{x\}) \to S \subseteq ⋃ J)$
22	17 21	sylan9r	$⊢ (J \in Top \land \neg S = \emptyset) \to (\forall x \in S S \in nei (J) (\{x\}) \to S \subseteq ⋃ J)$
23	18	ntrss2	$⊢ (J \in Top \land S \subseteq ⋃ J) \to int (J) (S) \subseteq S$
24	23	adantr	$⊢ ((J \in Top \land S \subseteq ⋃ J) \land \forall x \in S \{x\} \subseteq int (J) (S)) \to int (J) (S) \subseteq S$
25		vex	$⊢ x \in V$
26	25	snss	$⊢ x \in int (J) (S) \leftrightarrow \{x\} \subseteq int (J) (S)$
27	26	ralbii	$⊢ \forall x \in S x \in int (J) (S) \leftrightarrow \forall x \in S \{x\} \subseteq int (J) (S)$
28		dfss3	$⊢ S \subseteq int (J) (S) \leftrightarrow \forall x \in S x \in int (J) (S)$
29	28	biimpri	$⊢ \forall x \in S x \in int (J) (S) \to S \subseteq int (J) (S)$
30	29	adantl	$⊢ ((J \in Top \land S \subseteq ⋃ J) \land \forall x \in S x \in int (J) (S)) \to S \subseteq int (J) (S)$
31	27 30	sylan2br	$⊢ ((J \in Top \land S \subseteq ⋃ J) \land \forall x \in S \{x\} \subseteq int (J) (S)) \to S \subseteq int (J) (S)$
32	24 31	eqssd	$⊢ ((J \in Top \land S \subseteq ⋃ J) \land \forall x \in S \{x\} \subseteq int (J) (S)) \to int (J) (S) = S$
33	32	ex	$⊢ (J \in Top \land S \subseteq ⋃ J) \to (\forall x \in S \{x\} \subseteq int (J) (S) \to int (J) (S) = S)$
34	25	snss	$⊢ x \in S \leftrightarrow \{x\} \subseteq S$
35		sstr2	$⊢ \{x\} \subseteq S \to (S \subseteq ⋃ J \to \{x\} \subseteq ⋃ J)$
36	35	com12	$⊢ S \subseteq ⋃ J \to (\{x\} \subseteq S \to \{x\} \subseteq ⋃ J)$
37	36	adantl	$⊢ (J \in Top \land S \subseteq ⋃ J) \to (\{x\} \subseteq S \to \{x\} \subseteq ⋃ J)$
38	34 37	syl5bi	$⊢ (J \in Top \land S \subseteq ⋃ J) \to (x \in S \to \{x\} \subseteq ⋃ J)$
39	38	imp	$⊢ ((J \in Top \land S \subseteq ⋃ J) \land x \in S) \to \{x\} \subseteq ⋃ J$
40	18	neiint	$⊢ (J \in Top \land \{x\} \subseteq ⋃ J \land S \subseteq ⋃ J) \to (S \in nei (J) (\{x\}) \leftrightarrow \{x\} \subseteq int (J) (S))$
41	40	3com23	$⊢ (J \in Top \land S \subseteq ⋃ J \land \{x\} \subseteq ⋃ J) \to (S \in nei (J) (\{x\}) \leftrightarrow \{x\} \subseteq int (J) (S))$
42	41	3expa	$⊢ ((J \in Top \land S \subseteq ⋃ J) \land \{x\} \subseteq ⋃ J) \to (S \in nei (J) (\{x\}) \leftrightarrow \{x\} \subseteq int (J) (S))$
43	39 42	syldan	$⊢ ((J \in Top \land S \subseteq ⋃ J) \land x \in S) \to (S \in nei (J) (\{x\}) \leftrightarrow \{x\} \subseteq int (J) (S))$
44	43	ralbidva	$⊢ (J \in Top \land S \subseteq ⋃ J) \to (\forall x \in S S \in nei (J) (\{x\}) \leftrightarrow \forall x \in S \{x\} \subseteq int (J) (S))$
45	18	isopn3	$⊢ (J \in Top \land S \subseteq ⋃ J) \to (S \in J \leftrightarrow int (J) (S) = S)$
46	33 44 45	3imtr4d	$⊢ (J \in Top \land S \subseteq ⋃ J) \to (\forall x \in S S \in nei (J) (\{x\}) \to S \in J)$
47	46	ex	$⊢ J \in Top \to (S \subseteq ⋃ J \to (\forall x \in S S \in nei (J) (\{x\}) \to S \in J))$
48	47	com23	$⊢ J \in Top \to (\forall x \in S S \in nei (J) (\{x\}) \to (S \subseteq ⋃ J \to S \in J))$
49	48	adantr	$⊢ (J \in Top \land \neg S = \emptyset) \to (\forall x \in S S \in nei (J) (\{x\}) \to (S \subseteq ⋃ J \to S \in J))$
50	22 49	mpdd	$⊢ (J \in Top \land \neg S = \emptyset) \to (\forall x \in S S \in nei (J) (\{x\}) \to S \in J)$
51	13 50	impbid	$⊢ (J \in Top \land \neg S = \emptyset) \to (S \in J \leftrightarrow \forall x \in S S \in nei (J) (\{x\}))$
52	8 51	pm2.61dan	$⊢ J \in Top \to (S \in J \leftrightarrow \forall x \in S S \in nei (J) (\{x\}))$

Metamath Proof Explorer

Theorem opnnei

Proof