This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem isnrm

Description: The predicate "is a normal space." Much like the case for regular spaces, normal does not imply Hausdorff or even regular. (Contributed by Jeff Hankins, 1-Feb-2010) (Revised by Mario Carneiro, 24-Aug-2015)

		Ref	Expression
	Assertion	isnrm	$⊢ J \in Nrm \leftrightarrow (J \in Top \land \forall x \in J \forall y \in (Clsd (J) \cap 𝒫 x) \exists z \in J (y \subseteq z \land cls (J) (z) \subseteq x))$

Proof

Step	Hyp	Ref	Expression
1		fveq2	$⊢ j = J \to Clsd (j) = Clsd (J)$
2	1	ineq1d	$⊢ j = J \to Clsd (j) \cap 𝒫 x = Clsd (J) \cap 𝒫 x$
3		fveq2	$⊢ j = J \to cls (j) = cls (J)$
4	3	fveq1d	$⊢ j = J \to cls (j) (z) = cls (J) (z)$
5	4	sseq1d	$⊢ j = J \to (cls (j) (z) \subseteq x \leftrightarrow cls (J) (z) \subseteq x)$
6	5	anbi2d	$⊢ j = J \to ((y \subseteq z \land cls (j) (z) \subseteq x) \leftrightarrow (y \subseteq z \land cls (J) (z) \subseteq x))$
7	6	rexeqbi1dv	$⊢ j = J \to (\exists z \in j (y \subseteq z \land cls (j) (z) \subseteq x) \leftrightarrow \exists z \in J (y \subseteq z \land cls (J) (z) \subseteq x))$
8	2 7	raleqbidv	$⊢ j = J \to (\forall y \in (Clsd (j) \cap 𝒫 x) \exists z \in j (y \subseteq z \land cls (j) (z) \subseteq x) \leftrightarrow \forall y \in (Clsd (J) \cap 𝒫 x) \exists z \in J (y \subseteq z \land cls (J) (z) \subseteq x))$
9	8	raleqbi1dv	$⊢ j = J \to (\forall x \in j \forall y \in (Clsd (j) \cap 𝒫 x) \exists z \in j (y \subseteq z \land cls (j) (z) \subseteq x) \leftrightarrow \forall x \in J \forall y \in (Clsd (J) \cap 𝒫 x) \exists z \in J (y \subseteq z \land cls (J) (z) \subseteq x))$
10		df-nrm	$⊢ Nrm = \{j \in Top \| \forall x \in j \forall y \in (Clsd (j) \cap 𝒫 x) \exists z \in j (y \subseteq z \land cls (j) (z) \subseteq x)\}$
11	9 10	elrab2	$⊢ J \in Nrm \leftrightarrow (J \in Top \land \forall x \in J \forall y \in (Clsd (J) \cap 𝒫 x) \exists z \in J (y \subseteq z \land cls (J) (z) \subseteq x))$