Definition df-uss

Description: Define the uniform structure extractor function. Similarly with df-topn this differs from df-unif when a structure has been restricted using df-ress ; in this case the UnifSet component will still have a uniform set over the larger set, and this function fixes this by restricting the uniform set as well. (Contributed by Thierry Arnoux, 1-Dec-2017)

	Ref	Expression
Assertion	df-uss	$$⊢\mathrm{UnifSt}=\left(f\in \mathrm{V}⟼\mathrm{UnifSet}\left(f\right){\upharpoonright }_{𝑡}\left({\mathrm{Base}}_f\times {\mathrm{Base}}_f\right)\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cuss	$$class\mathrm{UnifSt}$$
1		vf	$$setvarf$$
2		cvv	$$class\mathrm{V}$$
3		cunif	$$class\mathrm{UnifSet}$$
4	1	cv	$$setvarf$$
5	4 3	cfv	$$class\mathrm{UnifSet}\left(f\right)$$
6		crest	$$class{\upharpoonright }_{𝑡}$$
7		cbs	$$class\mathrm{Base}$$
8	4 7	cfv	$$class{\mathrm{Base}}_f$$
9	8 8	cxp	$$class\left({\mathrm{Base}}_f\times {\mathrm{Base}}_f\right)$$
10	5 9 6	co	$$class\left(\mathrm{UnifSet}\left(f\right){\upharpoonright }_{𝑡}\left({\mathrm{Base}}_f\times {\mathrm{Base}}_f\right)\right)$$
11	1 2 10	cmpt	$$class\left(f\in \mathrm{V}⟼\mathrm{UnifSet}\left(f\right){\upharpoonright }_{𝑡}\left({\mathrm{Base}}_f\times {\mathrm{Base}}_f\right)\right)$$
12	0 11	wceq	$$wff\mathrm{UnifSt}=\left(f\in \mathrm{V}⟼\mathrm{UnifSet}\left(f\right){\upharpoonright }_{𝑡}\left({\mathrm{Base}}_f\times {\mathrm{Base}}_f\right)\right)$$