| 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" ndx, defined
as the identity function
restricted to ℕ, can be used to extract
the number 𝐴 from a
slot, since (Slot 𝐴‘ndx) = 𝐴 (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 (Base‘ndx)
in theorems and
proofs instead of its value 1).
The class Slot cannot be defined as
(𝑥
∈ 𝑉 ↦ (𝑓 ∈ 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 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.) |
