isreg

Description: The predicate "is a regular space". In a regular space, any open neighborhood has a closed subneighborhood. Note that some authors require the space to be Hausdorff (which would make it the same as T_3), but we reserve the phrase "regular Hausdorff" for that as many topologists do. (Contributed by Jeff Hankins, 1-Feb-2010) (Revised by Mario Carneiro, 25-Aug-2015)

		Ref	Expression
	Assertion	isreg	$⊢ J \in Reg \leftrightarrow (J \in Top \land \forall x \in J \forall y \in x \exists z \in J (y \in z \land cls (J) (z) \subseteq x))$

Proof

Step	Hyp	Ref	Expression
1		fveq2	$⊢ j = J \to cls (j) = cls (J)$
2	1	fveq1d	$⊢ j = J \to cls (j) (z) = cls (J) (z)$
3	2	sseq1d	$⊢ j = J \to (cls (j) (z) \subseteq x \leftrightarrow cls (J) (z) \subseteq x)$
4	3	anbi2d	$⊢ j = J \to ((y \in z \land cls (j) (z) \subseteq x) \leftrightarrow (y \in z \land cls (J) (z) \subseteq x))$
5	4	rexeqbi1dv	$⊢ j = J \to (\exists z \in j (y \in z \land cls (j) (z) \subseteq x) \leftrightarrow \exists z \in J (y \in z \land cls (J) (z) \subseteq x))$
6	5	ralbidv	$⊢ j = J \to (\forall y \in x \exists z \in j (y \in z \land cls (j) (z) \subseteq x) \leftrightarrow \forall y \in x \exists z \in J (y \in z \land cls (J) (z) \subseteq x))$
7	6	raleqbi1dv	$⊢ j = J \to (\forall x \in j \forall y \in x \exists z \in j (y \in z \land cls (j) (z) \subseteq x) \leftrightarrow \forall x \in J \forall y \in x \exists z \in J (y \in z \land cls (J) (z) \subseteq x))$
8		df-reg	$⊢ Reg = \{j \in Top \| \forall x \in j \forall y \in x \exists z \in j (y \in z \land cls (j) (z) \subseteq x)\}$
9	7 8	elrab2	$⊢ J \in Reg \leftrightarrow (J \in Top \land \forall x \in J \forall y \in x \exists z \in J (y \in z \land cls (J) (z) \subseteq x))$

Metamath Proof Explorer

Theorem isreg

Proof