Definition df-slot

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

Note that Slot A is implemented as "evaluation at A ". That is, ( Slot AS ) is defined to be ( SA ) , 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 Andx ) = A (see ndxarg ). 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 ( Basendx ) in theorems and proofs instead of its value 1).

The class Slot cannot be defined as ( x e.V |-> ( f e. V |-> ( fx ) ) ) 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 ). 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)

	Ref	Expression
Assertion	df-slot	|- Slot A = ( x e. _V |-> ( x ` A ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cA	|- A
1	0	cslot	|- Slot A
2		vx	|- x
3		cvv	|- _V
4	2	cv	|- x
5	0 4	cfv	|- ( x ` A )
6	2 3 5	cmpt	|- ( x e. _V |-> ( x ` A ) )
7	1 6	wceq	|- Slot A = ( x e. _V |-> ( x ` A ) )