Definition df-slot 16892

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 18040) or a group (df-grp 18589)).

Note that Slot 𝐴 is implemented as "evaluation at 𝐴". That is, (Slot 𝐴‘𝑆) is defined to be (𝑆‘𝐴), where 𝐴 will typically be an index (which is implemented as a small natural number) of a component of an extensible structure 𝑆. Each extensible structure is a function defined on specific (natural number) "slots", and the function Slot 𝐴 extracts the structure's component as a function value at a particular slot (with index 𝐴).

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 16906). 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 hard-coded, numeric value 1), and discourage using the specific definition of slot extractors like Base = Slot 1 (see df-base 16922). Actually, these definitions are used in two basic theorems named *id (theorems of the form 𝐶 = Slot (𝐶‘ndx)) and *ndx (theorems of the form (𝐶‘ndx) = 𝑁) only (see, for example, baseid 16924 and basendx 16930), except additionally in the discouraged theorem baseval 16923 to demonstrate the representations of the value of the base set extractor. The *id theorems are implementation independent equivalents of the definitions by the means of ndxid 16907, but the *ndx theorems still depend on the hard-coded values of the indices. Therefore, the usage of these *ndx theorems is also discouraged (for more details see the section header comment mmtheorems.html#cnx 16907).

Example: The group operation is the second component, i.e., the component in the second slot, of a group-like structure 𝐺 = {⟨(Base‘ndx), 𝐵⟩, ⟨(+_g‘ndx), + ⟩} (see grpstr 17003). The slot extractor +_g = Slot 2 (see df-plusg 16984) applied on the structure 𝐺 provides the group operation + = (+_g‘𝐺). Expanding the defintions, we get + = (Slot 2‘𝐺) = (𝐺‘2) = (𝐺‘(+_g‘ndx)) (for the last equation, see plusgndx 16997).

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 6796). 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 𝐴 = (𝑥 ∈ V ↦ (𝑥‘𝐴))

Distinct variable group:   𝑥,𝐴

Detailed syntax breakdown of Definition df-slot

Step	Hyp	Ref	Expression
1		cA	. . 3 class 𝐴
2	1	cslot 16891	. 2 class Slot 𝐴
3		vx	. . 3 setvar 𝑥
4		cvv 3433	. . 3 class V
5	3	cv 1538	. . . 4 class 𝑥
6	1, 5	cfv 6437	. . 3 class (𝑥‘𝐴)
7	3, 4, 6	cmpt 5158	. 2 class (𝑥 ∈ V ↦ (𝑥‘𝐴))
8	2, 7	wceq 1539	1 wff Slot 𝐴 = (𝑥 ∈ V ↦ (𝑥‘𝐴))

This definition is referenced by:  sloteq  16893  slotfn  16894  strfvnd  16895  bj-evaleq  35252  bj-evalfun  35253  bj-evalfn  35254  bj-evalval  35255