Metamath Proof Explorer


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 UnifSt = f V UnifSet f 𝑡 Base f × Base f

Detailed syntax breakdown

Step Hyp Ref Expression
0 cuss class UnifSt
1 vf setvar f
2 cvv class V
3 cunif class UnifSet
4 1 cv setvar f
5 4 3 cfv class UnifSet f
6 crest class 𝑡
7 cbs class Base
8 4 7 cfv class Base f
9 8 8 cxp class Base f × Base f
10 5 9 6 co class UnifSet f 𝑡 Base f × Base f
11 1 2 10 cmpt class f V UnifSet f 𝑡 Base f × Base f
12 0 11 wceq wff UnifSt = f V UnifSet f 𝑡 Base f × Base f