isnrm3

Description: A topological space is normal iff any two disjoint closed sets are separated by open sets. (Contributed by Mario Carneiro, 24-Aug-2015)

		Ref	Expression
	Assertion	isnrm3	$⊢ J \in Nrm \leftrightarrow (J \in Top \land \forall c \in Clsd (J) \forall d \in Clsd (J) (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		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)$
3	2	3exp2	$⊢ J \in Nrm \to (c \in Clsd (J) \to (d \in Clsd (J) \to (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))))$
4	3	impd	$⊢ J \in Nrm \to ((c \in Clsd (J) \land d \in Clsd (J)) \to (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)))$
5	4	ralrimivv	$⊢ J \in Nrm \to \forall c \in Clsd (J) \forall d \in Clsd (J) (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))$
6	1 5	jca	$⊢ J \in Nrm \to (J \in Top \land \forall c \in Clsd (J) \forall d \in Clsd (J) (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)))$
7		simpl	$⊢ (J \in Top \land \forall c \in Clsd (J) \forall d \in Clsd (J) (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))) \to J \in Top$
8		simpr1	$⊢ (((J \in Top \land x \in J) \land y \in J) \land (c \subseteq x \land d \subseteq y \land x \cap y = \emptyset)) \to c \subseteq x$
9		simpr2	$⊢ (((J \in Top \land x \in J) \land y \in J) \land (c \subseteq x \land d \subseteq y \land x \cap y = \emptyset)) \to d \subseteq y$
10		sslin	$⊢ d \subseteq y \to cls (J) (x) \cap d \subseteq cls (J) (x) \cap y$
11	9 10	syl	$⊢ (((J \in Top \land x \in J) \land y \in J) \land (c \subseteq x \land d \subseteq y \land x \cap y = \emptyset)) \to cls (J) (x) \cap d \subseteq cls (J) (x) \cap y$
12		eqid	$⊢ ⋃ J = ⋃ J$
13	12	opncld	$⊢ (J \in Top \land y \in J) \to ⋃ J ∖ y \in Clsd (J)$
14	13	ad4ant13	$⊢ (((J \in Top \land x \in J) \land y \in J) \land (c \subseteq x \land d \subseteq y \land x \cap y = \emptyset)) \to ⋃ J ∖ y \in Clsd (J)$
15		simpr3	$⊢ (((J \in Top \land x \in J) \land y \in J) \land (c \subseteq x \land d \subseteq y \land x \cap y = \emptyset)) \to x \cap y = \emptyset$
16		simpllr	$⊢ (((J \in Top \land x \in J) \land y \in J) \land (c \subseteq x \land d \subseteq y \land x \cap y = \emptyset)) \to x \in J$
17		elssuni	$⊢ x \in J \to x \subseteq ⋃ J$
18		reldisj	$⊢ x \subseteq ⋃ J \to (x \cap y = \emptyset \leftrightarrow x \subseteq ⋃ J ∖ y)$
19	16 17 18	3syl	$⊢ (((J \in Top \land x \in J) \land y \in J) \land (c \subseteq x \land d \subseteq y \land x \cap y = \emptyset)) \to (x \cap y = \emptyset \leftrightarrow x \subseteq ⋃ J ∖ y)$
20	15 19	mpbid	$⊢ (((J \in Top \land x \in J) \land y \in J) \land (c \subseteq x \land d \subseteq y \land x \cap y = \emptyset)) \to x \subseteq ⋃ J ∖ y$
21	12	clsss2	$⊢ (⋃ J ∖ y \in Clsd (J) \land x \subseteq ⋃ J ∖ y) \to cls (J) (x) \subseteq ⋃ J ∖ y$
22		ssdifin0	$⊢ cls (J) (x) \subseteq ⋃ J ∖ y \to cls (J) (x) \cap y = \emptyset$
23	21 22	syl	$⊢ (⋃ J ∖ y \in Clsd (J) \land x \subseteq ⋃ J ∖ y) \to cls (J) (x) \cap y = \emptyset$
24	14 20 23	syl2anc	$⊢ (((J \in Top \land x \in J) \land y \in J) \land (c \subseteq x \land d \subseteq y \land x \cap y = \emptyset)) \to cls (J) (x) \cap y = \emptyset$
25		sseq0	$⊢ (cls (J) (x) \cap d \subseteq cls (J) (x) \cap y \land cls (J) (x) \cap y = \emptyset) \to cls (J) (x) \cap d = \emptyset$
26	11 24 25	syl2anc	$⊢ (((J \in Top \land x \in J) \land y \in J) \land (c \subseteq x \land d \subseteq y \land x \cap y = \emptyset)) \to cls (J) (x) \cap d = \emptyset$
27	8 26	jca	$⊢ (((J \in Top \land x \in J) \land y \in J) \land (c \subseteq x \land d \subseteq y \land x \cap y = \emptyset)) \to (c \subseteq x \land cls (J) (x) \cap d = \emptyset)$
28	27	rexlimdva2	$⊢ (J \in Top \land x \in J) \to (\exists y \in J (c \subseteq x \land d \subseteq y \land x \cap y = \emptyset) \to (c \subseteq x \land cls (J) (x) \cap d = \emptyset))$
29	28	reximdva	$⊢ J \in Top \to (\exists x \in J \exists y \in J (c \subseteq x \land d \subseteq y \land x \cap y = \emptyset) \to \exists x \in J (c \subseteq x \land cls (J) (x) \cap d = \emptyset))$
30	29	imim2d	$⊢ J \in Top \to ((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)) \to (c \cap d = \emptyset \to \exists x \in J (c \subseteq x \land cls (J) (x) \cap d = \emptyset)))$
31	30	ralimdv	$⊢ J \in Top \to (\forall d \in Clsd (J) (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)) \to \forall d \in Clsd (J) (c \cap d = \emptyset \to \exists x \in J (c \subseteq x \land cls (J) (x) \cap d = \emptyset)))$
32	31	ralimdv	$⊢ J \in Top \to (\forall c \in Clsd (J) \forall d \in Clsd (J) (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)) \to \forall c \in Clsd (J) \forall d \in Clsd (J) (c \cap d = \emptyset \to \exists x \in J (c \subseteq x \land cls (J) (x) \cap d = \emptyset)))$
33	32	imp	$⊢ (J \in Top \land \forall c \in Clsd (J) \forall d \in Clsd (J) (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))) \to \forall c \in Clsd (J) \forall d \in Clsd (J) (c \cap d = \emptyset \to \exists x \in J (c \subseteq x \land cls (J) (x) \cap d = \emptyset))$
34		isnrm2	$⊢ J \in Nrm \leftrightarrow (J \in Top \land \forall c \in Clsd (J) \forall d \in Clsd (J) (c \cap d = \emptyset \to \exists x \in J (c \subseteq x \land cls (J) (x) \cap d = \emptyset)))$
35	7 33 34	sylanbrc	$⊢ (J \in Top \land \forall c \in Clsd (J) \forall d \in Clsd (J) (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))) \to J \in Nrm$
36	6 35	impbii	$⊢ J \in Nrm \leftrightarrow (J \in Top \land \forall c \in Clsd (J) \forall d \in Clsd (J) (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 isnrm3

Proof