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 e. _V |-> ( ( UnifSet ` f ) |`t ( ( Base ` f ) X. ( Base ` f ) ) ) )

Detailed syntax breakdown

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