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 𝐴 = ( 𝑥 ∈ V ↦ ( 𝑥 ‘ 𝐴 ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 0 | cA | ⊢ 𝐴 | |
| 1 | 0 | cslot | ⊢ Slot 𝐴 |
| 2 | vx | ⊢ 𝑥 | |
| 3 | cvv | ⊢ V | |
| 4 | 2 | cv | ⊢ 𝑥 |
| 5 | 0 4 | cfv | ⊢ ( 𝑥 ‘ 𝐴 ) |
| 6 | 2 3 5 | cmpt | ⊢ ( 𝑥 ∈ V ↦ ( 𝑥 ‘ 𝐴 ) ) |
| 7 | 1 6 | wceq | ⊢ Slot 𝐴 = ( 𝑥 ∈ V ↦ ( 𝑥 ‘ 𝐴 ) ) |