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 (df-poset 16946) or a group (df-grp 17425)).
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 15882). 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 6201). 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.) |