Definition df-cnrm

Description: Define completely normal spaces. A space is completely normal if all its subspaces are normal. (Contributed by Mario Carneiro, 26-Aug-2015)

	Ref	Expression
Assertion	df-cnrm	$$⊢\mathrm{CNrm}=\left\{j\in \mathrm{Top}|\forall x\in 𝒫\bigcup jj{\upharpoonright }_{𝑡}x\in \mathrm{Nrm}\right\}$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		ccnrm	$$class\mathrm{CNrm}$$
1		vj	$$setvarj$$
2		ctop	$$class\mathrm{Top}$$
3		vx	$$setvarx$$
4	1	cv	$$setvarj$$
5	4	cuni	$$class\bigcup j$$
6	5	cpw	$$class𝒫\bigcup j$$
7		crest	$$class{\upharpoonright }_{𝑡}$$
8	3	cv	$$setvarx$$
9	4 8 7	co	$$class\left(j{\upharpoonright }_{𝑡}x\right)$$
10		cnrm	$$class\mathrm{Nrm}$$
11	9 10	wcel	$$wffj{\upharpoonright }_{𝑡}x\in \mathrm{Nrm}$$
12	11 3 6	wral	$$wff\forall x\in 𝒫\bigcup jj{\upharpoonright }_{𝑡}x\in \mathrm{Nrm}$$
13	12 1 2	crab	$$class\left\{j\in \mathrm{Top}|\forall x\in 𝒫\bigcup jj{\upharpoonright }_{𝑡}x\in \mathrm{Nrm}\right\}$$
14	0 13	wceq	$$wff\mathrm{CNrm}=\left\{j\in \mathrm{Top}|\forall x\in 𝒫\bigcup jj{\upharpoonright }_{𝑡}x\in \mathrm{Nrm}\right\}$$