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		disjdifr	$⊢ (X ∖ cls (J) (y)) \cap cls (J) (y) = \emptyset$
26		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$
27	24 25 26	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$
28		sseq2	$⊢ x = X ∖ cls (J) (y) \to (C \subseteq x \leftrightarrow C \subseteq X ∖ cls (J) (y))$
29		ineq1	$⊢ x = X ∖ cls (J) (y) \to x \cap y = (X ∖ cls (J) (y)) \cap y$
30	29	eqeq1d	$⊢ x = X ∖ cls (J) (y) \to (x \cap y = \emptyset \leftrightarrow (X ∖ cls (J) (y)) \cap y = \emptyset)$
31	28 30	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))$
32	31	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)$
33	10 19 20 27 32	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)$
34		simpl	$⊢ (J \in Reg \land (C \in Clsd (J) \land A \in X \land \neg A \in C)) \to J \in Reg$
35		simpr1	$⊢ (J \in Reg \land (C \in Clsd (J) \land A \in X \land \neg A \in C)) \to C \in Clsd (J)$
36	1	cldopn	$⊢ C \in Clsd (J) \to X ∖ C \in J$
37	35 36	syl	$⊢ (J \in Reg \land (C \in Clsd (J) \land A \in X \land \neg A \in C)) \to X ∖ C \in J$
38		simpr2	$⊢ (J \in Reg \land (C \in Clsd (J) \land A \in X \land \neg A \in C)) \to A \in X$
39		simpr3	$⊢ (J \in Reg \land (C \in Clsd (J) \land A \in X \land \neg A \in C)) \to \neg A \in C$
40	38 39	eldifd	$⊢ (J \in Reg \land (C \in Clsd (J) \land A \in X \land \neg A \in C)) \to A \in (X ∖ C)$
41		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)$
42	34 37 40 41	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)$
43	33 42	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)$
44		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)$
45	43 44	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