MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-uss Structured version   Unicode version

Definition df-uss 20737
Description: Define the uniform structure extractor function. Similarly with df-topn 14803 this differs from df-unif 14702 when a structure has been restricted using df-ress 14621; 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  =  ( f  e.  _V  |->  ( ( UnifSet `  f )t  (
( Base `  f )  X.  ( Base `  f
) ) ) )

Detailed syntax breakdown of Definition df-uss
StepHypRef Expression
1 cuss 20734 . 2  class UnifSt
2 vf . . 3  setvar  f
3 cvv 3095 . . 3  class  _V
42cv 1382 . . . . 5  class  f
5 cunif 14689 . . . . 5  class  UnifSet
64, 5cfv 5578 . . . 4  class  ( UnifSet `  f )
7 cbs 14614 . . . . . 6  class  Base
84, 7cfv 5578 . . . . 5  class  ( Base `  f )
98, 8cxp 4987 . . . 4  class  ( (
Base `  f )  X.  ( Base `  f
) )
10 crest 14800 . . . 4  classt
116, 9, 10co 6281 . . 3  class  ( (
UnifSet `  f )t  ( (
Base `  f )  X.  ( Base `  f
) ) )
122, 3, 11cmpt 4495 . 2  class  ( f  e.  _V  |->  ( (
UnifSet `  f )t  ( (
Base `  f )  X.  ( Base `  f
) ) ) )
131, 12wceq 1383 1  wff UnifSt  =  ( f  e.  _V  |->  ( ( UnifSet `  f )t  (
( Base `  f )  X.  ( Base `  f
) ) ) )
Colors of variables: wff setvar class
This definition is referenced by:  ussval  20740
  Copyright terms: Public domain W3C validator