Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  df-ress Unicode version

Definition df-ress 11977
 Description: Define a multifunction restriction operator for extensible structures, which can be used to turn statements about rings into statements about subrings, modules into submodules, etc. This definition knows nothing about individual structures and merely truncates the set while leaving operators alone; individual kinds of structures will need to handle this behavior, by ignoring operators' values outside the range, defining a function using the base set and applying that, or explicitly truncating the slot before use. (Credit for this operator goes to Mario Carneiro.) (Contributed by Stefan O'Rear, 29-Nov-2014.)
Assertion
Ref Expression
df-ress s sSet
Distinct variable group:   ,

Detailed syntax breakdown of Definition df-ress
StepHypRef Expression
1 cress 11970 . 2 s
2 vw . . 3
3 vx . . 3
4 cvv 2686 . . 3
52cv 1330 . . . . . 6
6 cbs 11969 . . . . . 6
75, 6cfv 5123 . . . . 5
83cv 1330 . . . . 5
97, 8wss 3071 . . . 4
10 cnx 11966 . . . . . . 7
1110, 6cfv 5123 . . . . . 6
128, 7cin 3070 . . . . . 6
1311, 12cop 3530 . . . . 5
14 csts 11967 . . . . 5 sSet
155, 13, 14co 5774 . . . 4 sSet
169, 5, 15cif 3474 . . 3 sSet
172, 3, 4, 4, 16cmpo 5776 . 2 sSet
181, 17wceq 1331 1 s sSet
 Colors of variables: wff set class This definition is referenced by:  reldmress  12027  ressid2  12028  ressval2  12029
 Copyright terms: Public domain W3C validator