Definition df-uss 22060

Description: Define the uniform structure extractor function. Similarly with df-topn 16084 this differs from df-unif 15965 when a structure has been restricted using df-ress 15865; 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.)

Assertion

Ref	Expression
df-uss	|- UnifSt = ( f e. _V |-> ( ( UnifSet ` f ) ↾t ( ( Base ` f ) X. ( Base ` f ) ) ) )

Detailed syntax breakdown of Definition df-uss

Step	Hyp	Ref	Expression
1		cuss 22057	. 2 class UnifSt
2		vf	. . 3 setvar f
3		cvv 3200	. . 3 class _V
4	2	cv 1482	. . . . 5 class f
5		cunif 15951	. . . . 5 class UnifSet
6	4, 5	cfv 5888	. . . 4 class ( UnifSet ` f )
7		cbs 15857	. . . . . 6 class Base
8	4, 7	cfv 5888	. . . . 5 class ( Base ` f )
9	8, 8	cxp 5112	. . . 4 class ( ( Base ` f ) X. ( Base ` f ) )
10		crest 16081	. . . 4 class ↾t
11	6, 9, 10	co 6650	. . 3 class ( ( UnifSet ` f ) ↾t ( ( Base ` f ) X. ( Base ` f ) ) )
12	2, 3, 11	cmpt 4729	. 2 class ( f e. _V |-> ( ( UnifSet ` f ) ↾t ( ( Base ` f ) X. ( Base ` f ) ) ) )
13	1, 12	wceq 1483	1 wff UnifSt = ( f e. _V |-> ( ( UnifSet ` f ) ↾t ( ( Base ` f ) X. ( Base ` f ) ) ) )

This definition is referenced by:  ussval  22063