isreg2

Description: A topological space is regular if any closed set is separated from any point not in it by neighborhoods. (Contributed by Jeff Hankins, 1-Feb-2010) (Revised by Mario Carneiro, 25-Aug-2015)

		Ref	Expression
	Assertion	isreg2	$⊢ J \in TopOn (X) \to (J \in Reg \leftrightarrow \forall c \in Clsd (J) \forall x \in X (\neg x \in c \to \exists o \in J \exists p \in J (c \subseteq o \land x \in p \land o \cap p = \emptyset)))$

Proof

Step	Hyp	Ref	Expression
1		simp1r	$⊢ ((J \in TopOn (X) \land J \in Reg) \land (c \in Clsd (J) \land x \in X) \land \neg x \in c) \to J \in Reg$
2		simp2l	$⊢ ((J \in TopOn (X) \land J \in Reg) \land (c \in Clsd (J) \land x \in X) \land \neg x \in c) \to c \in Clsd (J)$
3		simp2r	$⊢ ((J \in TopOn (X) \land J \in Reg) \land (c \in Clsd (J) \land x \in X) \land \neg x \in c) \to x \in X$
4		simp1l	$⊢ ((J \in TopOn (X) \land J \in Reg) \land (c \in Clsd (J) \land x \in X) \land \neg x \in c) \to J \in TopOn (X)$
5		toponuni	$⊢ J \in TopOn (X) \to X = ⋃ J$
6	4 5	syl	$⊢ ((J \in TopOn (X) \land J \in Reg) \land (c \in Clsd (J) \land x \in X) \land \neg x \in c) \to X = ⋃ J$
7	3 6	eleqtrd	$⊢ ((J \in TopOn (X) \land J \in Reg) \land (c \in Clsd (J) \land x \in X) \land \neg x \in c) \to x \in ⋃ J$
8		simp3	$⊢ ((J \in TopOn (X) \land J \in Reg) \land (c \in Clsd (J) \land x \in X) \land \neg x \in c) \to \neg x \in c$
9		eqid	$⊢ ⋃ J = ⋃ J$
10	9	regsep2	$⊢ (J \in Reg \land (c \in Clsd (J) \land x \in ⋃ J \land \neg x \in c)) \to \exists o \in J \exists p \in J (c \subseteq o \land x \in p \land o \cap p = \emptyset)$
11	1 2 7 8 10	syl13anc	$⊢ ((J \in TopOn (X) \land J \in Reg) \land (c \in Clsd (J) \land x \in X) \land \neg x \in c) \to \exists o \in J \exists p \in J (c \subseteq o \land x \in p \land o \cap p = \emptyset)$
12	11	3expia	$⊢ ((J \in TopOn (X) \land J \in Reg) \land (c \in Clsd (J) \land x \in X)) \to (\neg x \in c \to \exists o \in J \exists p \in J (c \subseteq o \land x \in p \land o \cap p = \emptyset))$
13	12	ralrimivva	$⊢ (J \in TopOn (X) \land J \in Reg) \to \forall c \in Clsd (J) \forall x \in X (\neg x \in c \to \exists o \in J \exists p \in J (c \subseteq o \land x \in p \land o \cap p = \emptyset))$
14		topontop	$⊢ J \in TopOn (X) \to J \in Top$
15	14	adantr	$⊢ (J \in TopOn (X) \land \forall c \in Clsd (J) \forall x \in X (\neg x \in c \to \exists o \in J \exists p \in J (c \subseteq o \land x \in p \land o \cap p = \emptyset))) \to J \in Top$
16	5	adantr	$⊢ (J \in TopOn (X) \land y \in J) \to X = ⋃ J$
17	16	difeq1d	$⊢ (J \in TopOn (X) \land y \in J) \to X ∖ y = ⋃ J ∖ y$
18	9	opncld	$⊢ (J \in Top \land y \in J) \to ⋃ J ∖ y \in Clsd (J)$
19	14 18	sylan	$⊢ (J \in TopOn (X) \land y \in J) \to ⋃ J ∖ y \in Clsd (J)$
20	17 19	eqeltrd	$⊢ (J \in TopOn (X) \land y \in J) \to X ∖ y \in Clsd (J)$
21		eleq2	$⊢ c = X ∖ y \to (x \in c \leftrightarrow x \in (X ∖ y))$
22	21	notbid	$⊢ c = X ∖ y \to (\neg x \in c \leftrightarrow \neg x \in (X ∖ y))$
23		eldif	$⊢ x \in (X ∖ y) \leftrightarrow (x \in X \land \neg x \in y)$
24	23	baibr	$⊢ x \in X \to (\neg x \in y \leftrightarrow x \in (X ∖ y))$
25	24	con1bid	$⊢ x \in X \to (\neg x \in (X ∖ y) \leftrightarrow x \in y)$
26	22 25	sylan9bb	$⊢ (c = X ∖ y \land x \in X) \to (\neg x \in c \leftrightarrow x \in y)$
27		simpl	$⊢ (c = X ∖ y \land x \in X) \to c = X ∖ y$
28	27	sseq1d	$⊢ (c = X ∖ y \land x \in X) \to (c \subseteq o \leftrightarrow X ∖ y \subseteq o)$
29	28	3anbi1d	$⊢ (c = X ∖ y \land x \in X) \to ((c \subseteq o \land x \in p \land o \cap p = \emptyset) \leftrightarrow (X ∖ y \subseteq o \land x \in p \land o \cap p = \emptyset))$
30	29	2rexbidv	$⊢ (c = X ∖ y \land x \in X) \to (\exists o \in J \exists p \in J (c \subseteq o \land x \in p \land o \cap p = \emptyset) \leftrightarrow \exists o \in J \exists p \in J (X ∖ y \subseteq o \land x \in p \land o \cap p = \emptyset))$
31	26 30	imbi12d	$⊢ (c = X ∖ y \land x \in X) \to ((\neg x \in c \to \exists o \in J \exists p \in J (c \subseteq o \land x \in p \land o \cap p = \emptyset)) \leftrightarrow (x \in y \to \exists o \in J \exists p \in J (X ∖ y \subseteq o \land x \in p \land o \cap p = \emptyset)))$
32	31	ralbidva	$⊢ c = X ∖ y \to (\forall x \in X (\neg x \in c \to \exists o \in J \exists p \in J (c \subseteq o \land x \in p \land o \cap p = \emptyset)) \leftrightarrow \forall x \in X (x \in y \to \exists o \in J \exists p \in J (X ∖ y \subseteq o \land x \in p \land o \cap p = \emptyset)))$
33	32	rspcv	$⊢ X ∖ y \in Clsd (J) \to (\forall c \in Clsd (J) \forall x \in X (\neg x \in c \to \exists o \in J \exists p \in J (c \subseteq o \land x \in p \land o \cap p = \emptyset)) \to \forall x \in X (x \in y \to \exists o \in J \exists p \in J (X ∖ y \subseteq o \land x \in p \land o \cap p = \emptyset)))$
34	20 33	syl	$⊢ (J \in TopOn (X) \land y \in J) \to (\forall c \in Clsd (J) \forall x \in X (\neg x \in c \to \exists o \in J \exists p \in J (c \subseteq o \land x \in p \land o \cap p = \emptyset)) \to \forall x \in X (x \in y \to \exists o \in J \exists p \in J (X ∖ y \subseteq o \land x \in p \land o \cap p = \emptyset)))$
35		ralcom3	$⊢ \forall x \in X (x \in y \to \exists o \in J \exists p \in J (X ∖ y \subseteq o \land x \in p \land o \cap p = \emptyset)) \leftrightarrow \forall x \in y (x \in X \to \exists o \in J \exists p \in J (X ∖ y \subseteq o \land x \in p \land o \cap p = \emptyset))$
36		toponss	$⊢ (J \in TopOn (X) \land y \in J) \to y \subseteq X$
37	36	sselda	$⊢ ((J \in TopOn (X) \land y \in J) \land x \in y) \to x \in X$
38		simprr2	$⊢ (((J \in TopOn (X) \land y \in J) \land x \in y) \land ((o \in J \land p \in J) \land (X ∖ y \subseteq o \land x \in p \land o \cap p = \emptyset))) \to x \in p$
39	5	ad3antrrr	$⊢ (((J \in TopOn (X) \land y \in J) \land x \in y) \land ((o \in J \land p \in J) \land (X ∖ y \subseteq o \land x \in p \land o \cap p = \emptyset))) \to X = ⋃ J$
40	39	difeq1d	$⊢ (((J \in TopOn (X) \land y \in J) \land x \in y) \land ((o \in J \land p \in J) \land (X ∖ y \subseteq o \land x \in p \land o \cap p = \emptyset))) \to X ∖ o = ⋃ J ∖ o$
41	14	ad3antrrr	$⊢ (((J \in TopOn (X) \land y \in J) \land x \in y) \land ((o \in J \land p \in J) \land (X ∖ y \subseteq o \land x \in p \land o \cap p = \emptyset))) \to J \in Top$
42		simprll	$⊢ (((J \in TopOn (X) \land y \in J) \land x \in y) \land ((o \in J \land p \in J) \land (X ∖ y \subseteq o \land x \in p \land o \cap p = \emptyset))) \to o \in J$
43	9	opncld	$⊢ (J \in Top \land o \in J) \to ⋃ J ∖ o \in Clsd (J)$
44	41 42 43	syl2anc	$⊢ (((J \in TopOn (X) \land y \in J) \land x \in y) \land ((o \in J \land p \in J) \land (X ∖ y \subseteq o \land x \in p \land o \cap p = \emptyset))) \to ⋃ J ∖ o \in Clsd (J)$
45	40 44	eqeltrd	$⊢ (((J \in TopOn (X) \land y \in J) \land x \in y) \land ((o \in J \land p \in J) \land (X ∖ y \subseteq o \land x \in p \land o \cap p = \emptyset))) \to X ∖ o \in Clsd (J)$
46		incom	$⊢ p \cap o = o \cap p$
47		simprr3	$⊢ (((J \in TopOn (X) \land y \in J) \land x \in y) \land ((o \in J \land p \in J) \land (X ∖ y \subseteq o \land x \in p \land o \cap p = \emptyset))) \to o \cap p = \emptyset$
48	46 47	syl5eq	$⊢ (((J \in TopOn (X) \land y \in J) \land x \in y) \land ((o \in J \land p \in J) \land (X ∖ y \subseteq o \land x \in p \land o \cap p = \emptyset))) \to p \cap o = \emptyset$
49		simplll	$⊢ (((J \in TopOn (X) \land y \in J) \land x \in y) \land ((o \in J \land p \in J) \land (X ∖ y \subseteq o \land x \in p \land o \cap p = \emptyset))) \to J \in TopOn (X)$
50		simprlr	$⊢ (((J \in TopOn (X) \land y \in J) \land x \in y) \land ((o \in J \land p \in J) \land (X ∖ y \subseteq o \land x \in p \land o \cap p = \emptyset))) \to p \in J$
51		toponss	$⊢ (J \in TopOn (X) \land p \in J) \to p \subseteq X$
52	49 50 51	syl2anc	$⊢ (((J \in TopOn (X) \land y \in J) \land x \in y) \land ((o \in J \land p \in J) \land (X ∖ y \subseteq o \land x \in p \land o \cap p = \emptyset))) \to p \subseteq X$
53		reldisj	$⊢ p \subseteq X \to (p \cap o = \emptyset \leftrightarrow p \subseteq X ∖ o)$
54	52 53	syl	$⊢ (((J \in TopOn (X) \land y \in J) \land x \in y) \land ((o \in J \land p \in J) \land (X ∖ y \subseteq o \land x \in p \land o \cap p = \emptyset))) \to (p \cap o = \emptyset \leftrightarrow p \subseteq X ∖ o)$
55	48 54	mpbid	$⊢ (((J \in TopOn (X) \land y \in J) \land x \in y) \land ((o \in J \land p \in J) \land (X ∖ y \subseteq o \land x \in p \land o \cap p = \emptyset))) \to p \subseteq X ∖ o$
56	9	clsss2	$⊢ (X ∖ o \in Clsd (J) \land p \subseteq X ∖ o) \to cls (J) (p) \subseteq X ∖ o$
57	45 55 56	syl2anc	$⊢ (((J \in TopOn (X) \land y \in J) \land x \in y) \land ((o \in J \land p \in J) \land (X ∖ y \subseteq o \land x \in p \land o \cap p = \emptyset))) \to cls (J) (p) \subseteq X ∖ o$
58		simprr1	$⊢ (((J \in TopOn (X) \land y \in J) \land x \in y) \land ((o \in J \land p \in J) \land (X ∖ y \subseteq o \land x \in p \land o \cap p = \emptyset))) \to X ∖ y \subseteq o$
59		difcom	$⊢ X ∖ y \subseteq o \leftrightarrow X ∖ o \subseteq y$
60	58 59	sylib	$⊢ (((J \in TopOn (X) \land y \in J) \land x \in y) \land ((o \in J \land p \in J) \land (X ∖ y \subseteq o \land x \in p \land o \cap p = \emptyset))) \to X ∖ o \subseteq y$
61	57 60	sstrd	$⊢ (((J \in TopOn (X) \land y \in J) \land x \in y) \land ((o \in J \land p \in J) \land (X ∖ y \subseteq o \land x \in p \land o \cap p = \emptyset))) \to cls (J) (p) \subseteq y$
62	38 61	jca	$⊢ (((J \in TopOn (X) \land y \in J) \land x \in y) \land ((o \in J \land p \in J) \land (X ∖ y \subseteq o \land x \in p \land o \cap p = \emptyset))) \to (x \in p \land cls (J) (p) \subseteq y)$
63	62	expr	$⊢ (((J \in TopOn (X) \land y \in J) \land x \in y) \land (o \in J \land p \in J)) \to ((X ∖ y \subseteq o \land x \in p \land o \cap p = \emptyset) \to (x \in p \land cls (J) (p) \subseteq y))$
64	63	anassrs	$⊢ ((((J \in TopOn (X) \land y \in J) \land x \in y) \land o \in J) \land p \in J) \to ((X ∖ y \subseteq o \land x \in p \land o \cap p = \emptyset) \to (x \in p \land cls (J) (p) \subseteq y))$
65	64	reximdva	$⊢ (((J \in TopOn (X) \land y \in J) \land x \in y) \land o \in J) \to (\exists p \in J (X ∖ y \subseteq o \land x \in p \land o \cap p = \emptyset) \to \exists p \in J (x \in p \land cls (J) (p) \subseteq y))$
66	65	rexlimdva	$⊢ ((J \in TopOn (X) \land y \in J) \land x \in y) \to (\exists o \in J \exists p \in J (X ∖ y \subseteq o \land x \in p \land o \cap p = \emptyset) \to \exists p \in J (x \in p \land cls (J) (p) \subseteq y))$
67	37 66	embantd	$⊢ ((J \in TopOn (X) \land y \in J) \land x \in y) \to ((x \in X \to \exists o \in J \exists p \in J (X ∖ y \subseteq o \land x \in p \land o \cap p = \emptyset)) \to \exists p \in J (x \in p \land cls (J) (p) \subseteq y))$
68	67	ralimdva	$⊢ (J \in TopOn (X) \land y \in J) \to (\forall x \in y (x \in X \to \exists o \in J \exists p \in J (X ∖ y \subseteq o \land x \in p \land o \cap p = \emptyset)) \to \forall x \in y \exists p \in J (x \in p \land cls (J) (p) \subseteq y))$
69	35 68	syl5bi	$⊢ (J \in TopOn (X) \land y \in J) \to (\forall x \in X (x \in y \to \exists o \in J \exists p \in J (X ∖ y \subseteq o \land x \in p \land o \cap p = \emptyset)) \to \forall x \in y \exists p \in J (x \in p \land cls (J) (p) \subseteq y))$
70	34 69	syld	$⊢ (J \in TopOn (X) \land y \in J) \to (\forall c \in Clsd (J) \forall x \in X (\neg x \in c \to \exists o \in J \exists p \in J (c \subseteq o \land x \in p \land o \cap p = \emptyset)) \to \forall x \in y \exists p \in J (x \in p \land cls (J) (p) \subseteq y))$
71	70	ralrimdva	$⊢ J \in TopOn (X) \to (\forall c \in Clsd (J) \forall x \in X (\neg x \in c \to \exists o \in J \exists p \in J (c \subseteq o \land x \in p \land o \cap p = \emptyset)) \to \forall y \in J \forall x \in y \exists p \in J (x \in p \land cls (J) (p) \subseteq y))$
72	71	imp	$⊢ (J \in TopOn (X) \land \forall c \in Clsd (J) \forall x \in X (\neg x \in c \to \exists o \in J \exists p \in J (c \subseteq o \land x \in p \land o \cap p = \emptyset))) \to \forall y \in J \forall x \in y \exists p \in J (x \in p \land cls (J) (p) \subseteq y)$
73		isreg	$⊢ J \in Reg \leftrightarrow (J \in Top \land \forall y \in J \forall x \in y \exists p \in J (x \in p \land cls (J) (p) \subseteq y))$
74	15 72 73	sylanbrc	$⊢ (J \in TopOn (X) \land \forall c \in Clsd (J) \forall x \in X (\neg x \in c \to \exists o \in J \exists p \in J (c \subseteq o \land x \in p \land o \cap p = \emptyset))) \to J \in Reg$
75	13 74	impbida	$⊢ J \in TopOn (X) \to (J \in Reg \leftrightarrow \forall c \in Clsd (J) \forall x \in X (\neg x \in c \to \exists o \in J \exists p \in J (c \subseteq o \land x \in p \land o \cap p = \emptyset)))$

Metamath Proof Explorer

Theorem isreg2

Proof