regsep2

Description: In a regular space, a closed set is separated by open sets from a point not in it. (Contributed by Jeff Hankins, 1-Feb-2010) (Revised by Mario Carneiro, 25-Aug-2015)

		Ref	Expression
	Hypothesis	t1sep.1	$⊢ X = ⋃ J$
	Assertion	regsep2	$⊢ (J \in Reg \land (C \in Clsd (J) \land A \in X \land \neg A \in C)) \to \exists x \in J \exists y \in J (C \subseteq x \land A \in y \land x \cap y = \emptyset)$

Proof

Step	Hyp	Ref	Expression
1		t1sep.1	$⊢ X = ⋃ J$
2		regtop	$⊢ J \in Reg \to J \in Top$
3	2	ad2antrr	$⊢ ((J \in Reg \land (C \in Clsd (J) \land A \in X \land \neg A \in C)) \land (y \in J \land (A \in y \land cls (J) (y) \subseteq X ∖ C))) \to J \in Top$
4		elssuni	$⊢ y \in J \to y \subseteq ⋃ J$
5	4 1	sseqtrrdi	$⊢ y \in J \to y \subseteq X$
6	5	ad2antrl	$⊢ ((J \in Reg \land (C \in Clsd (J) \land A \in X \land \neg A \in C)) \land (y \in J \land (A \in y \land cls (J) (y) \subseteq X ∖ C))) \to y \subseteq X$
7	1	clscld	$⊢ (J \in Top \land y \subseteq X) \to cls (J) (y) \in Clsd (J)$
8	3 6 7	syl2anc	$⊢ ((J \in Reg \land (C \in Clsd (J) \land A \in X \land \neg A \in C)) \land (y \in J \land (A \in y \land cls (J) (y) \subseteq X ∖ C))) \to cls (J) (y) \in Clsd (J)$
9	1	cldopn	$⊢ cls (J) (y) \in Clsd (J) \to X ∖ cls (J) (y) \in J$
10	8 9	syl	$⊢ ((J \in Reg \land (C \in Clsd (J) \land A \in X \land \neg A \in C)) \land (y \in J \land (A \in y \land cls (J) (y) \subseteq X ∖ C))) \to X ∖ cls (J) (y) \in J$
11		simprrr	$⊢ ((J \in Reg \land (C \in Clsd (J) \land A \in X \land \neg A \in C)) \land (y \in J \land (A \in y \land cls (J) (y) \subseteq X ∖ C))) \to cls (J) (y) \subseteq X ∖ C$
12	1	clsss3	$⊢ (J \in Top \land y \subseteq X) \to cls (J) (y) \subseteq X$
13	3 6 12	syl2anc	$⊢ ((J \in Reg \land (C \in Clsd (J) \land A \in X \land \neg A \in C)) \land (y \in J \land (A \in y \land cls (J) (y) \subseteq X ∖ C))) \to cls (J) (y) \subseteq X$
14		simplr1	$⊢ ((J \in Reg \land (C \in Clsd (J) \land A \in X \land \neg A \in C)) \land (y \in J \land (A \in y \land cls (J) (y) \subseteq X ∖ C))) \to C \in Clsd (J)$
15	1	cldss	$⊢ C \in Clsd (J) \to C \subseteq X$
16	14 15	syl	$⊢ ((J \in Reg \land (C \in Clsd (J) \land A \in X \land \neg A \in C)) \land (y \in J \land (A \in y \land cls (J) (y) \subseteq X ∖ C))) \to C \subseteq X$
17		ssconb	$⊢ (cls (J) (y) \subseteq X \land C \subseteq X) \to (cls (J) (y) \subseteq X ∖ C \leftrightarrow C \subseteq X ∖ cls (J) (y))$
18	13 16 17	syl2anc	$⊢ ((J \in Reg \land (C \in Clsd (J) \land A \in X \land \neg A \in C)) \land (y \in J \land (A \in y \land cls (J) (y) \subseteq X ∖ C))) \to (cls (J) (y) \subseteq X ∖ C \leftrightarrow C \subseteq X ∖ cls (J) (y))$
19	11 18	mpbid	$⊢ ((J \in Reg \land (C \in Clsd (J) \land A \in X \land \neg A \in C)) \land (y \in J \land (A \in y \land cls (J) (y) \subseteq X ∖ C))) \to C \subseteq X ∖ cls (J) (y)$
20		simprrl	$⊢ ((J \in Reg \land (C \in Clsd (J) \land A \in X \land \neg A \in C)) \land (y \in J \land (A \in y \land cls (J) (y) \subseteq X ∖ C))) \to A \in y$
21	1	sscls	$⊢ (J \in Top \land y \subseteq X) \to y \subseteq cls (J) (y)$
22	3 6 21	syl2anc	$⊢ ((J \in Reg \land (C \in Clsd (J) \land A \in X \land \neg A \in C)) \land (y \in J \land (A \in y \land cls (J) (y) \subseteq X ∖ C))) \to y \subseteq cls (J) (y)$
23		sslin	$⊢ y \subseteq cls (J) (y) \to (X ∖ cls (J) (y)) \cap y \subseteq (X ∖ cls (J) (y)) \cap cls (J) (y)$
24	22 23	syl	$⊢ ((J \in Reg \land (C \in Clsd (J) \land A \in X \land \neg A \in C)) \land (y \in J \land (A \in y \land cls (J) (y) \subseteq X ∖ C))) \to (X ∖ cls (J) (y)) \cap y \subseteq (X ∖ cls (J) (y)) \cap cls (J) (y)$
25		incom	$⊢ (X ∖ cls (J) (y)) \cap cls (J) (y) = cls (J) (y) \cap (X ∖ cls (J) (y))$
26		disjdif	$⊢ cls (J) (y) \cap (X ∖ cls (J) (y)) = \emptyset$
27	25 26	eqtri	$⊢ (X ∖ cls (J) (y)) \cap cls (J) (y) = \emptyset$
28		sseq0	$⊢ ((X ∖ cls (J) (y)) \cap y \subseteq (X ∖ cls (J) (y)) \cap cls (J) (y) \land (X ∖ cls (J) (y)) \cap cls (J) (y) = \emptyset) \to (X ∖ cls (J) (y)) \cap y = \emptyset$
29	24 27 28	sylancl	$⊢ ((J \in Reg \land (C \in Clsd (J) \land A \in X \land \neg A \in C)) \land (y \in J \land (A \in y \land cls (J) (y) \subseteq X ∖ C))) \to (X ∖ cls (J) (y)) \cap y = \emptyset$
30		sseq2	$⊢ x = X ∖ cls (J) (y) \to (C \subseteq x \leftrightarrow C \subseteq X ∖ cls (J) (y))$
31		ineq1	$⊢ x = X ∖ cls (J) (y) \to x \cap y = (X ∖ cls (J) (y)) \cap y$
32	31	eqeq1d	$⊢ x = X ∖ cls (J) (y) \to (x \cap y = \emptyset \leftrightarrow (X ∖ cls (J) (y)) \cap y = \emptyset)$
33	30 32	3anbi13d	$⊢ x = X ∖ cls (J) (y) \to ((C \subseteq x \land A \in y \land x \cap y = \emptyset) \leftrightarrow (C \subseteq X ∖ cls (J) (y) \land A \in y \land (X ∖ cls (J) (y)) \cap y = \emptyset))$
34	33	rspcev	$⊢ (X ∖ cls (J) (y) \in J \land (C \subseteq X ∖ cls (J) (y) \land A \in y \land (X ∖ cls (J) (y)) \cap y = \emptyset)) \to \exists x \in J (C \subseteq x \land A \in y \land x \cap y = \emptyset)$
35	10 19 20 29 34	syl13anc	$⊢ ((J \in Reg \land (C \in Clsd (J) \land A \in X \land \neg A \in C)) \land (y \in J \land (A \in y \land cls (J) (y) \subseteq X ∖ C))) \to \exists x \in J (C \subseteq x \land A \in y \land x \cap y = \emptyset)$
36		simpl	$⊢ (J \in Reg \land (C \in Clsd (J) \land A \in X \land \neg A \in C)) \to J \in Reg$
37		simpr1	$⊢ (J \in Reg \land (C \in Clsd (J) \land A \in X \land \neg A \in C)) \to C \in Clsd (J)$
38	1	cldopn	$⊢ C \in Clsd (J) \to X ∖ C \in J$
39	37 38	syl	$⊢ (J \in Reg \land (C \in Clsd (J) \land A \in X \land \neg A \in C)) \to X ∖ C \in J$
40		simpr2	$⊢ (J \in Reg \land (C \in Clsd (J) \land A \in X \land \neg A \in C)) \to A \in X$
41		simpr3	$⊢ (J \in Reg \land (C \in Clsd (J) \land A \in X \land \neg A \in C)) \to \neg A \in C$
42	40 41	eldifd	$⊢ (J \in Reg \land (C \in Clsd (J) \land A \in X \land \neg A \in C)) \to A \in (X ∖ C)$
43		regsep	$⊢ (J \in Reg \land X ∖ C \in J \land A \in (X ∖ C)) \to \exists y \in J (A \in y \land cls (J) (y) \subseteq X ∖ C)$
44	36 39 42 43	syl3anc	$⊢ (J \in Reg \land (C \in Clsd (J) \land A \in X \land \neg A \in C)) \to \exists y \in J (A \in y \land cls (J) (y) \subseteq X ∖ C)$
45	35 44	reximddv	$⊢ (J \in Reg \land (C \in Clsd (J) \land A \in X \land \neg A \in C)) \to \exists y \in J \exists x \in J (C \subseteq x \land A \in y \land x \cap y = \emptyset)$
46		rexcom	$⊢ \exists y \in J \exists x \in J (C \subseteq x \land A \in y \land x \cap y = \emptyset) \leftrightarrow \exists x \in J \exists y \in J (C \subseteq x \land A \in y \land x \cap y = \emptyset)$
47	45 46	sylib	$⊢ (J \in Reg \land (C \in Clsd (J) \land A \in X \land \neg A \in C)) \to \exists x \in J \exists y \in J (C \subseteq x \land A \in y \land x \cap y = \emptyset)$

Metamath Proof Explorer

Theorem regsep2

Proof