nrmsep

Description: In a normal space, disjoint closed sets are separated by open sets. (Contributed by Jeff Hankins, 1-Feb-2010)

		Ref	Expression
	Assertion	nrmsep	$⊢ (J \in Nrm \land (C \in Clsd (J) \land D \in Clsd (J) \land C \cap D = \emptyset)) \to \exists x \in J \exists y \in J (C \subseteq x \land D \subseteq y \land x \cap y = \emptyset)$

Proof

Step	Hyp	Ref	Expression
1		nrmtop	$⊢ J \in Nrm \to J \in Top$
2	1	ad2antrr	$⊢ ((J \in Nrm \land (C \in Clsd (J) \land D \in Clsd (J) \land C \cap D = \emptyset)) \land (x \in J \land (C \subseteq x \land cls (J) (x) \cap D = \emptyset))) \to J \in Top$
3		elssuni	$⊢ x \in J \to x \subseteq ⋃ J$
4	3	ad2antrl	$⊢ ((J \in Nrm \land (C \in Clsd (J) \land D \in Clsd (J) \land C \cap D = \emptyset)) \land (x \in J \land (C \subseteq x \land cls (J) (x) \cap D = \emptyset))) \to x \subseteq ⋃ J$
5		eqid	$⊢ ⋃ J = ⋃ J$
6	5	clscld	$⊢ (J \in Top \land x \subseteq ⋃ J) \to cls (J) (x) \in Clsd (J)$
7	2 4 6	syl2anc	$⊢ ((J \in Nrm \land (C \in Clsd (J) \land D \in Clsd (J) \land C \cap D = \emptyset)) \land (x \in J \land (C \subseteq x \land cls (J) (x) \cap D = \emptyset))) \to cls (J) (x) \in Clsd (J)$
8	5	cldopn	$⊢ cls (J) (x) \in Clsd (J) \to ⋃ J ∖ cls (J) (x) \in J$
9	7 8	syl	$⊢ ((J \in Nrm \land (C \in Clsd (J) \land D \in Clsd (J) \land C \cap D = \emptyset)) \land (x \in J \land (C \subseteq x \land cls (J) (x) \cap D = \emptyset))) \to ⋃ J ∖ cls (J) (x) \in J$
10		simprrl	$⊢ ((J \in Nrm \land (C \in Clsd (J) \land D \in Clsd (J) \land C \cap D = \emptyset)) \land (x \in J \land (C \subseteq x \land cls (J) (x) \cap D = \emptyset))) \to C \subseteq x$
11		incom	$⊢ D \cap cls (J) (x) = cls (J) (x) \cap D$
12		simprrr	$⊢ ((J \in Nrm \land (C \in Clsd (J) \land D \in Clsd (J) \land C \cap D = \emptyset)) \land (x \in J \land (C \subseteq x \land cls (J) (x) \cap D = \emptyset))) \to cls (J) (x) \cap D = \emptyset$
13	11 12	syl5eq	$⊢ ((J \in Nrm \land (C \in Clsd (J) \land D \in Clsd (J) \land C \cap D = \emptyset)) \land (x \in J \land (C \subseteq x \land cls (J) (x) \cap D = \emptyset))) \to D \cap cls (J) (x) = \emptyset$
14		simplr2	$⊢ ((J \in Nrm \land (C \in Clsd (J) \land D \in Clsd (J) \land C \cap D = \emptyset)) \land (x \in J \land (C \subseteq x \land cls (J) (x) \cap D = \emptyset))) \to D \in Clsd (J)$
15	5	cldss	$⊢ D \in Clsd (J) \to D \subseteq ⋃ J$
16		reldisj	$⊢ D \subseteq ⋃ J \to (D \cap cls (J) (x) = \emptyset \leftrightarrow D \subseteq ⋃ J ∖ cls (J) (x))$
17	14 15 16	3syl	$⊢ ((J \in Nrm \land (C \in Clsd (J) \land D \in Clsd (J) \land C \cap D = \emptyset)) \land (x \in J \land (C \subseteq x \land cls (J) (x) \cap D = \emptyset))) \to (D \cap cls (J) (x) = \emptyset \leftrightarrow D \subseteq ⋃ J ∖ cls (J) (x))$
18	13 17	mpbid	$⊢ ((J \in Nrm \land (C \in Clsd (J) \land D \in Clsd (J) \land C \cap D = \emptyset)) \land (x \in J \land (C \subseteq x \land cls (J) (x) \cap D = \emptyset))) \to D \subseteq ⋃ J ∖ cls (J) (x)$
19	5	sscls	$⊢ (J \in Top \land x \subseteq ⋃ J) \to x \subseteq cls (J) (x)$
20	2 4 19	syl2anc	$⊢ ((J \in Nrm \land (C \in Clsd (J) \land D \in Clsd (J) \land C \cap D = \emptyset)) \land (x \in J \land (C \subseteq x \land cls (J) (x) \cap D = \emptyset))) \to x \subseteq cls (J) (x)$
21	20	ssrind	$⊢ ((J \in Nrm \land (C \in Clsd (J) \land D \in Clsd (J) \land C \cap D = \emptyset)) \land (x \in J \land (C \subseteq x \land cls (J) (x) \cap D = \emptyset))) \to x \cap (⋃ J ∖ cls (J) (x)) \subseteq cls (J) (x) \cap (⋃ J ∖ cls (J) (x))$
22		disjdif	$⊢ cls (J) (x) \cap (⋃ J ∖ cls (J) (x)) = \emptyset$
23		sseq0	$⊢ (x \cap (⋃ J ∖ cls (J) (x)) \subseteq cls (J) (x) \cap (⋃ J ∖ cls (J) (x)) \land cls (J) (x) \cap (⋃ J ∖ cls (J) (x)) = \emptyset) \to x \cap (⋃ J ∖ cls (J) (x)) = \emptyset$
24	21 22 23	sylancl	$⊢ ((J \in Nrm \land (C \in Clsd (J) \land D \in Clsd (J) \land C \cap D = \emptyset)) \land (x \in J \land (C \subseteq x \land cls (J) (x) \cap D = \emptyset))) \to x \cap (⋃ J ∖ cls (J) (x)) = \emptyset$
25		sseq2	$⊢ y = ⋃ J ∖ cls (J) (x) \to (D \subseteq y \leftrightarrow D \subseteq ⋃ J ∖ cls (J) (x))$
26		ineq2	$⊢ y = ⋃ J ∖ cls (J) (x) \to x \cap y = x \cap (⋃ J ∖ cls (J) (x))$
27	26	eqeq1d	$⊢ y = ⋃ J ∖ cls (J) (x) \to (x \cap y = \emptyset \leftrightarrow x \cap (⋃ J ∖ cls (J) (x)) = \emptyset)$
28	25 27	3anbi23d	$⊢ y = ⋃ J ∖ cls (J) (x) \to ((C \subseteq x \land D \subseteq y \land x \cap y = \emptyset) \leftrightarrow (C \subseteq x \land D \subseteq ⋃ J ∖ cls (J) (x) \land x \cap (⋃ J ∖ cls (J) (x)) = \emptyset))$
29	28	rspcev	$⊢ (⋃ J ∖ cls (J) (x) \in J \land (C \subseteq x \land D \subseteq ⋃ J ∖ cls (J) (x) \land x \cap (⋃ J ∖ cls (J) (x)) = \emptyset)) \to \exists y \in J (C \subseteq x \land D \subseteq y \land x \cap y = \emptyset)$
30	9 10 18 24 29	syl13anc	$⊢ ((J \in Nrm \land (C \in Clsd (J) \land D \in Clsd (J) \land C \cap D = \emptyset)) \land (x \in J \land (C \subseteq x \land cls (J) (x) \cap D = \emptyset))) \to \exists y \in J (C \subseteq x \land D \subseteq y \land x \cap y = \emptyset)$
31		nrmsep2	$⊢ (J \in Nrm \land (C \in Clsd (J) \land D \in Clsd (J) \land C \cap D = \emptyset)) \to \exists x \in J (C \subseteq x \land cls (J) (x) \cap D = \emptyset)$
32	30 31	reximddv	$⊢ (J \in Nrm \land (C \in Clsd (J) \land D \in Clsd (J) \land C \cap D = \emptyset)) \to \exists x \in J \exists y \in J (C \subseteq x \land D \subseteq y \land x \cap y = \emptyset)$

Metamath Proof Explorer

Theorem nrmsep

Proof