Definition df-usp

Description: Definition of a uniform space, i.e. a base set with an uniform structure and its induced topology. Derived from definition 3 of BourbakiTop1 p. II.4. (Contributed by Thierry Arnoux, 17-Nov-2017)

	Ref	Expression
Assertion	df-usp	$$⊢\mathrm{UnifSp}=\left\{f|\left(\mathrm{UnifSt}\left(f\right)\in \mathrm{UnifOn}\left({\mathrm{Base}}_f\right)\wedge \mathrm{TopOpen}\left(f\right)=\mathrm{unifTop}\left(\mathrm{UnifSt}\left(f\right)\right)\right)\right\}$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cusp	$$class\mathrm{UnifSp}$$
1		vf	$$setvarf$$
2		cuss	$$class\mathrm{UnifSt}$$
3	1	cv	$$setvarf$$
4	3 2	cfv	$$class\mathrm{UnifSt}\left(f\right)$$
5		cust	$$class\mathrm{UnifOn}$$
6		cbs	$$class\mathrm{Base}$$
7	3 6	cfv	$$class{\mathrm{Base}}_f$$
8	7 5	cfv	$$class\mathrm{UnifOn}\left({\mathrm{Base}}_f\right)$$
9	4 8	wcel	$$wff\mathrm{UnifSt}\left(f\right)\in \mathrm{UnifOn}\left({\mathrm{Base}}_f\right)$$
10		ctopn	$$class\mathrm{TopOpen}$$
11	3 10	cfv	$$class\mathrm{TopOpen}\left(f\right)$$
12		cutop	$$class\mathrm{unifTop}$$
13	4 12	cfv	$$class\mathrm{unifTop}\left(\mathrm{UnifSt}\left(f\right)\right)$$
14	11 13	wceq	$$wff\mathrm{TopOpen}\left(f\right)=\mathrm{unifTop}\left(\mathrm{UnifSt}\left(f\right)\right)$$
15	9 14	wa	$$wff\left(\mathrm{UnifSt}\left(f\right)\in \mathrm{UnifOn}\left({\mathrm{Base}}_f\right)\wedge \mathrm{TopOpen}\left(f\right)=\mathrm{unifTop}\left(\mathrm{UnifSt}\left(f\right)\right)\right)$$
16	15 1	cab	$$class\left\{f|\left(\mathrm{UnifSt}\left(f\right)\in \mathrm{UnifOn}\left({\mathrm{Base}}_f\right)\wedge \mathrm{TopOpen}\left(f\right)=\mathrm{unifTop}\left(\mathrm{UnifSt}\left(f\right)\right)\right)\right\}$$
17	0 16	wceq	$$wff\mathrm{UnifSp}=\left\{f|\left(\mathrm{UnifSt}\left(f\right)\in \mathrm{UnifOn}\left({\mathrm{Base}}_f\right)\wedge \mathrm{TopOpen}\left(f\right)=\mathrm{unifTop}\left(\mathrm{UnifSt}\left(f\right)\right)\right)\right\}$$