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 ) ) ) ) |