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

Definition df-slot 11973
 Description: Define the slot extractor for extensible structures. The class Slot is a function whose argument can be any set, although it is meaningful only if that set is a member of an extensible structure (such as a partially ordered set or a group). Note that Slot is implemented as "evaluation at ". That is, Slot is defined to be , where will typically be a small nonzero natural number. Each extensible structure is a function defined on specific natural number "slots", and this function extracts the value at a particular slot. The special "structure" , defined as the identity function restricted to , can be used to extract the number from a slot, since Slot (see ndxarg 11992). This is typically used to refer to the number of a slot when defining structures without having to expose the detail of what that number is (for instance, we use the expression in theorems and proofs instead of its value 1). The class Slot cannot be defined as because each Slot is a function on the proper class so is itself a proper class, and the values of functions are sets (fvex 5441). It is necessary to allow proper classes as values of Slot since for instance the class of all (base sets of) groups is proper. (Contributed by Mario Carneiro, 22-Sep-2015.)
Assertion
Ref Expression
df-slot Slot
Distinct variable group:   ,

Detailed syntax breakdown of Definition df-slot
StepHypRef Expression
1 cA . . 3
21cslot 11968 . 2 Slot
3 vx . . 3
4 cvv 2686 . . 3
53cv 1330 . . . 4
61, 5cfv 5123 . . 3
73, 4, 6cmpt 3989 . 2
82, 7wceq 1331 1 Slot
 Colors of variables: wff set class This definition is referenced by:  sloteq  11974  strnfvnd  11989  slotslfn  11995
 Copyright terms: Public domain W3C validator