Definition df-uss 21870

Description: Define the uniform structure extractor function. Similarly with df-topn 15907 this differs from df-unif 15792 when a structure has been restricted using df-ress 15702; 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 = (𝑓 ∈ V ↦ ((UnifSet‘𝑓) ↾t ((Base‘𝑓) × (Base‘𝑓))))

Detailed syntax breakdown of Definition df-uss

Step	Hyp	Ref	Expression
1		cuss 21867	. 2 class UnifSt
2		vf	. . 3 setvar 𝑓
3		cvv 3173	. . 3 class V
4	2	cv 1474	. . . . 5 class 𝑓
5		cunif 15778	. . . . 5 class UnifSet
6	4, 5	cfv 5804	. . . 4 class (UnifSet‘𝑓)
7		cbs 15695	. . . . . 6 class Base
8	4, 7	cfv 5804	. . . . 5 class (Base‘𝑓)
9	8, 8	cxp 5036	. . . 4 class ((Base‘𝑓) × (Base‘𝑓))
10		crest 15904	. . . 4 class ↾t
11	6, 9, 10	co 6549	. . 3 class ((UnifSet‘𝑓) ↾t ((Base‘𝑓) × (Base‘𝑓)))
12	2, 3, 11	cmpt 4643	. 2 class (𝑓 ∈ V ↦ ((UnifSet‘𝑓) ↾t ((Base‘𝑓) × (Base‘𝑓))))
13	1, 12	wceq 1475	1 wff UnifSt = (𝑓 ∈ V ↦ ((UnifSet‘𝑓) ↾t ((Base‘𝑓) × (Base‘𝑓))))

This definition is referenced by:  ussval  21873