Definition df-xms

Description: Define the (proper) class of extended metric spaces. (Contributed by Mario Carneiro, 2-Sep-2015)

	Ref	Expression
Assertion	df-xms	$$⊢\mathrm{\infty MetSp}=\left\{f\in \mathrm{TopSp}|\mathrm{TopOpen}\left(f\right)=\mathrm{MetOpen}\left({\mathrm{dist}\left(f\right)\upharpoonright }_{\left({\mathrm{Base}}_f\times {\mathrm{Base}}_f\right)}\right)\right\}$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cxms	$$class\mathrm{\infty MetSp}$$
1		vf	$$setvarf$$
2		ctps	$$class\mathrm{TopSp}$$
3		ctopn	$$class\mathrm{TopOpen}$$
4	1	cv	$$setvarf$$
5	4 3	cfv	$$class\mathrm{TopOpen}\left(f\right)$$
6		cmopn	$$class\mathrm{MetOpen}$$
7		cds	$$class\mathrm{dist}$$
8	4 7	cfv	$$class\mathrm{dist}\left(f\right)$$
9		cbs	$$class\mathrm{Base}$$
10	4 9	cfv	$$class{\mathrm{Base}}_f$$
11	10 10	cxp	$$class\left({\mathrm{Base}}_f\times {\mathrm{Base}}_f\right)$$
12	8 11	cres	$$class\left({\mathrm{dist}\left(f\right)\upharpoonright }_{\left({\mathrm{Base}}_f\times {\mathrm{Base}}_f\right)}\right)$$
13	12 6	cfv	$$class\mathrm{MetOpen}\left({\mathrm{dist}\left(f\right)\upharpoonright }_{\left({\mathrm{Base}}_f\times {\mathrm{Base}}_f\right)}\right)$$
14	5 13	wceq	$$wff\mathrm{TopOpen}\left(f\right)=\mathrm{MetOpen}\left({\mathrm{dist}\left(f\right)\upharpoonright }_{\left({\mathrm{Base}}_f\times {\mathrm{Base}}_f\right)}\right)$$
15	14 1 2	crab	$$class\left\{f\in \mathrm{TopSp}|\mathrm{TopOpen}\left(f\right)=\mathrm{MetOpen}\left({\mathrm{dist}\left(f\right)\upharpoonright }_{\left({\mathrm{Base}}_f\times {\mathrm{Base}}_f\right)}\right)\right\}$$
16	0 15	wceq	$$wff\mathrm{\infty MetSp}=\left\{f\in \mathrm{TopSp}|\mathrm{TopOpen}\left(f\right)=\mathrm{MetOpen}\left({\mathrm{dist}\left(f\right)\upharpoonright }_{\left({\mathrm{Base}}_f\times {\mathrm{Base}}_f\right)}\right)\right\}$$