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 e. _V |-> ( ( UnifSet ` f ) |`t ( ( Base ` f ) X. ( Base ` f ) ) ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
0 | cuss | |- UnifSt |
|
1 | vf | |- f |
|
2 | cvv | |- _V |
|
3 | cunif | |- UnifSet |
|
4 | 1 | cv | |- f |
5 | 4 3 | cfv | |- ( UnifSet ` f ) |
6 | crest | |- |`t |
|
7 | cbs | |- Base |
|
8 | 4 7 | cfv | |- ( Base ` f ) |
9 | 8 8 | cxp | |- ( ( Base ` f ) X. ( Base ` f ) ) |
10 | 5 9 6 | co | |- ( ( UnifSet ` f ) |`t ( ( Base ` f ) X. ( Base ` f ) ) ) |
11 | 1 2 10 | cmpt | |- ( f e. _V |-> ( ( UnifSet ` f ) |`t ( ( Base ` f ) X. ( Base ` f ) ) ) ) |
12 | 0 11 | wceq | |- UnifSt = ( f e. _V |-> ( ( UnifSet ` f ) |`t ( ( Base ` f ) X. ( Base ` f ) ) ) ) |