Definition df-slot 12420

Description: Define the slot extractor for extensible structures. The class Slot A 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 A is implemented as "evaluation at A". That is, (Slot A ` S ) is defined to be ( S ` A ), where A will typically be a small nonzero natural number. Each extensible structure S 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 NN, can be used to extract the number A from a slot, since (Slot A ` ndx ) = A (see ndxarg 12439). 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 ( x e. _V |-> ( f e. _V |-> ( f ` x ) ) ) because each Slot A is a function on the proper class _V so is itself a proper class, and the values of functions are sets (fvex 5516). It is necessary to allow proper classes as values of Slot A 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 A = ( x e. _V |-> ( x ` A ) )

Distinct variable group:   x, A

Detailed syntax breakdown of Definition df-slot

Step	Hyp	Ref	Expression
1		cA	. . 3 class A
2	1	cslot 12415	. 2 class Slot A
3		vx	. . 3 setvar x
4		cvv 2730	. . 3 class _V
5	3	cv 1347	. . . 4 class x
6	1, 5	cfv 5198	. . 3 class ( x ` A )
7	3, 4, 6	cmpt 4050	. 2 class ( x e. _V |-> ( x ` A ) )
8	2, 7	wceq 1348	1 wff Slot A = ( x e. _V |-> ( x ` A ) )

This definition is referenced by:  sloteq  12421  strnfvnd  12436  slotslfn  12442