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

Definition df-slot 12407
Description: Define the slot extractor for extensible structures. The class Slot  A 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  A is implemented as "evaluation at  A". That is,  (Slot  A `  S ) is defined to be  ( S `  A ), where  A will typically be a small nonzero natural number. Each extensible structure  S is a function defined on specific natural number "slots", and this function extracts the value at a particular slot.

The special "structure"  ndx, defined as the identity function restricted to  NN, can be used to extract the number  A from a slot, since  (Slot  A `  ndx )  =  A (see ndxarg 12426). 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  ( Base `  ndx ) in theorems and proofs instead of its value 1).

The class Slot cannot be defined as  ( x  e.  _V  |->  ( f  e. 
_V  |->  ( f `  x ) ) ) because each Slot  A is a function on the proper class  _V so is itself a proper class, and the values of functions are sets (fvex 5514). It is necessary to allow proper classes as values of Slot  A 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  A  =  ( x  e.  _V  |->  ( x `  A
) )
Distinct variable group:    x, A

Detailed syntax breakdown of Definition df-slot
StepHypRef Expression
1 cA . . 3  class  A
21cslot 12402 . 2  class Slot  A
3 vx . . 3  setvar  x
4 cvv 2730 . . 3  class  _V
53cv 1347 . . . 4  class  x
61, 5cfv 5196 . . 3  class  ( x `
 A )
73, 4, 6cmpt 4048 . 2  class  ( x  e.  _V  |->  ( x `
 A ) )
82, 7wceq 1348 1  wff Slot  A  =  ( x  e.  _V  |->  ( x `  A
) )
Colors of variables: wff set class
This definition is referenced by:  sloteq  12408  strnfvnd  12423  slotslfn  12429
  Copyright terms: Public domain W3C validator