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" ndx, defined
as the identity function
restricted to ℕ, can be used to extract
the number 𝐴 from a
slot, since (Slot 𝐴‘ndx) = 𝐴 (see ndxarg 12432). 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
(𝑥
∈ V ↦ (𝑓 ∈
V ↦ (𝑓‘𝑥))) because each Slot 𝐴
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 𝐴 since for instance the
class of all (base sets of) groups is proper. (Contributed by Mario
Carneiro, 22-Sep-2015.) |