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	bilanri	$⊢ ((J \in Top \land S \subseteq ⋃ J) \land \forall x \in S x \in int (J) (S)) \to S \subseteq int (J) (S)$
30	27 29	sylan2br	$⊢ ((J \in Top \land S \subseteq ⋃ J) \land \forall x \in S \{x\} \subseteq int (J) (S)) \to S \subseteq int (J) (S)$
31	24 30	eqssd	$⊢ ((J \in Top \land S \subseteq ⋃ J) \land \forall x \in S \{x\} \subseteq int (J) (S)) \to int (J) (S) = S$
32	31	ex	$⊢ (J \in Top \land S \subseteq ⋃ J) \to (\forall x \in S \{x\} \subseteq int (J) (S) \to int (J) (S) = S)$
33	25	snss	$⊢ x \in S \leftrightarrow \{x\} \subseteq S$
34		sstr2	$⊢ \{x\} \subseteq S \to (S \subseteq ⋃ J \to \{x\} \subseteq ⋃ J)$
35	34	com12	$⊢ S \subseteq ⋃ J \to (\{x\} \subseteq S \to \{x\} \subseteq ⋃ J)$
36	35	adantl	$⊢ (J \in Top \land S \subseteq ⋃ J) \to (\{x\} \subseteq S \to \{x\} \subseteq ⋃ J)$
37	33 36	biimtrid	$⊢ (J \in Top \land S \subseteq ⋃ J) \to (x \in S \to \{x\} \subseteq ⋃ J)$
38	37	imp	$⊢ ((J \in Top \land S \subseteq ⋃ J) \land x \in S) \to \{x\} \subseteq ⋃ J$
39	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))$
40	39	3com23	$⊢ (J \in Top \land S \subseteq ⋃ J \land \{x\} \subseteq ⋃ J) \to (S \in nei (J) (\{x\}) \leftrightarrow \{x\} \subseteq int (J) (S))$
41	40	3expa	$⊢ ((J \in Top \land S \subseteq ⋃ J) \land \{x\} \subseteq ⋃ J) \to (S \in nei (J) (\{x\}) \leftrightarrow \{x\} \subseteq int (J) (S))$
42	38 41	syldan	$⊢ ((J \in Top \land S \subseteq ⋃ J) \land x \in S) \to (S \in nei (J) (\{x\}) \leftrightarrow \{x\} \subseteq int (J) (S))$
43	42	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))$
44	18	isopn3	$⊢ (J \in Top \land S \subseteq ⋃ J) \to (S \in J \leftrightarrow int (J) (S) = S)$
45	32 43 44	3imtr4d	$⊢ (J \in Top \land S \subseteq ⋃ J) \to (\forall x \in S S \in nei (J) (\{x\}) \to S \in J)$
46	45	ex	$⊢ J \in Top \to (S \subseteq ⋃ J \to (\forall x \in S S \in nei (J) (\{x\}) \to S \in J))$
47	46	com23	$⊢ J \in Top \to (\forall x \in S S \in nei (J) (\{x\}) \to (S \subseteq ⋃ J \to S \in J))$
48	47	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))$
49	22 48	mpdd	$⊢ (J \in Top \land \neg S = \emptyset) \to (\forall x \in S S \in nei (J) (\{x\}) \to S \in J)$
50	13 49	impbid	$⊢ (J \in Top \land \neg S = \emptyset) \to (S \in J \leftrightarrow \forall x \in S S \in nei (J) (\{x\}))$
51	8 50	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