opnregcld

Description: A set is regularly closed iff it is the closure of some open set. (Contributed by Jeff Hankins, 27-Sep-2009)

		Ref	Expression
	Hypothesis	opnregcld.1	$⊢ X = ⋃ J$
	Assertion	opnregcld	$⊢ (J \in Top \land A \subseteq X) \to (cls (J) (int (J) (A)) = A \leftrightarrow \exists o \in J A = cls (J) (o))$

Proof

Step	Hyp	Ref	Expression
1		opnregcld.1	$⊢ X = ⋃ J$
2	1	ntropn	$⊢ (J \in Top \land A \subseteq X) \to int (J) (A) \in J$
3		eqcom	$⊢ cls (J) (int (J) (A)) = A \leftrightarrow A = cls (J) (int (J) (A))$
4	3	biimpi	$⊢ cls (J) (int (J) (A)) = A \to A = cls (J) (int (J) (A))$
5		fveq2	$⊢ o = int (J) (A) \to cls (J) (o) = cls (J) (int (J) (A))$
6	5	rspceeqv	$⊢ (int (J) (A) \in J \land A = cls (J) (int (J) (A))) \to \exists o \in J A = cls (J) (o)$
7	2 4 6	syl2an	$⊢ ((J \in Top \land A \subseteq X) \land cls (J) (int (J) (A)) = A) \to \exists o \in J A = cls (J) (o)$
8	7	ex	$⊢ (J \in Top \land A \subseteq X) \to (cls (J) (int (J) (A)) = A \to \exists o \in J A = cls (J) (o))$
9		simpl	$⊢ (J \in Top \land o \in J) \to J \in Top$
10	1	eltopss	$⊢ (J \in Top \land o \in J) \to o \subseteq X$
11	1	clsss3	$⊢ (J \in Top \land o \subseteq X) \to cls (J) (o) \subseteq X$
12	10 11	syldan	$⊢ (J \in Top \land o \in J) \to cls (J) (o) \subseteq X$
13	1	ntrss2	$⊢ (J \in Top \land cls (J) (o) \subseteq X) \to int (J) (cls (J) (o)) \subseteq cls (J) (o)$
14	12 13	syldan	$⊢ (J \in Top \land o \in J) \to int (J) (cls (J) (o)) \subseteq cls (J) (o)$
15	1	clsss	$⊢ (J \in Top \land cls (J) (o) \subseteq X \land int (J) (cls (J) (o)) \subseteq cls (J) (o)) \to cls (J) (int (J) (cls (J) (o))) \subseteq cls (J) (cls (J) (o))$
16	9 12 14 15	syl3anc	$⊢ (J \in Top \land o \in J) \to cls (J) (int (J) (cls (J) (o))) \subseteq cls (J) (cls (J) (o))$
17	1	clsidm	$⊢ (J \in Top \land o \subseteq X) \to cls (J) (cls (J) (o)) = cls (J) (o)$
18	10 17	syldan	$⊢ (J \in Top \land o \in J) \to cls (J) (cls (J) (o)) = cls (J) (o)$
19	16 18	sseqtrd	$⊢ (J \in Top \land o \in J) \to cls (J) (int (J) (cls (J) (o))) \subseteq cls (J) (o)$
20	1	ntrss3	$⊢ (J \in Top \land cls (J) (o) \subseteq X) \to int (J) (cls (J) (o)) \subseteq X$
21	12 20	syldan	$⊢ (J \in Top \land o \in J) \to int (J) (cls (J) (o)) \subseteq X$
22		simpr	$⊢ (J \in Top \land o \in J) \to o \in J$
23	1	sscls	$⊢ (J \in Top \land o \subseteq X) \to o \subseteq cls (J) (o)$
24	10 23	syldan	$⊢ (J \in Top \land o \in J) \to o \subseteq cls (J) (o)$
25	1	ssntr	$⊢ ((J \in Top \land cls (J) (o) \subseteq X) \land (o \in J \land o \subseteq cls (J) (o))) \to o \subseteq int (J) (cls (J) (o))$
26	9 12 22 24 25	syl22anc	$⊢ (J \in Top \land o \in J) \to o \subseteq int (J) (cls (J) (o))$
27	1	clsss	$⊢ (J \in Top \land int (J) (cls (J) (o)) \subseteq X \land o \subseteq int (J) (cls (J) (o))) \to cls (J) (o) \subseteq cls (J) (int (J) (cls (J) (o)))$
28	9 21 26 27	syl3anc	$⊢ (J \in Top \land o \in J) \to cls (J) (o) \subseteq cls (J) (int (J) (cls (J) (o)))$
29	19 28	eqssd	$⊢ (J \in Top \land o \in J) \to cls (J) (int (J) (cls (J) (o))) = cls (J) (o)$
30	29	adantlr	$⊢ ((J \in Top \land A \subseteq X) \land o \in J) \to cls (J) (int (J) (cls (J) (o))) = cls (J) (o)$
31		2fveq3	$⊢ A = cls (J) (o) \to cls (J) (int (J) (A)) = cls (J) (int (J) (cls (J) (o)))$
32		id	$⊢ A = cls (J) (o) \to A = cls (J) (o)$
33	31 32	eqeq12d	$⊢ A = cls (J) (o) \to (cls (J) (int (J) (A)) = A \leftrightarrow cls (J) (int (J) (cls (J) (o))) = cls (J) (o))$
34	30 33	syl5ibrcom	$⊢ ((J \in Top \land A \subseteq X) \land o \in J) \to (A = cls (J) (o) \to cls (J) (int (J) (A)) = A)$
35	34	rexlimdva	$⊢ (J \in Top \land A \subseteq X) \to (\exists o \in J A = cls (J) (o) \to cls (J) (int (J) (A)) = A)$
36	8 35	impbid	$⊢ (J \in Top \land A \subseteq X) \to (cls (J) (int (J) (A)) = A \leftrightarrow \exists o \in J A = cls (J) (o))$

Metamath Proof Explorer

Theorem opnregcld

Proof