Definition df-slot 16811

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

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 16825). 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 6769). 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 16810	. 2 class Slot 𝐴
3		vx	. . 3 setvar 𝑥
4		cvv 3422	. . 3 class V
5	3	cv 1538	. . . 4 class 𝑥
6	1, 5	cfv 6418	. . 3 class (𝑥‘𝐴)
7	3, 4, 6	cmpt 5153	. 2 class (𝑥 ∈ V ↦ (𝑥‘𝐴))
8	2, 7	wceq 1539	1 wff Slot 𝐴 = (𝑥 ∈ V ↦ (𝑥‘𝐴))

This definition is referenced by:  sloteq  16812  slotfn  16813  strfvnd  16814  bj-evaleq  35170  bj-evalfun  35171  bj-evalfn  35172  bj-evalval  35173