Description: A slot entry of an element of the base set of the category of categories for a weak universe belongs to the weak universe. Formerly part of the proof for catcoppccl . (Contributed by AV, 14-Oct-2024)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | catcbascl.c | |- C = ( CatCat ` U ) |
|
| catcbascl.b | |- B = ( Base ` C ) |
||
| catcbascl.u | |- ( ph -> U e. WUni ) |
||
| catcbascl.x | |- ( ph -> X e. B ) |
||
| catcslotelcl.e | |- E = Slot ( E ` ndx ) |
||
| Assertion | catcslotelcl | |- ( ph -> ( E ` X ) e. U ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | catcbascl.c | |- C = ( CatCat ` U ) |
|
| 2 | catcbascl.b | |- B = ( Base ` C ) |
|
| 3 | catcbascl.u | |- ( ph -> U e. WUni ) |
|
| 4 | catcbascl.x | |- ( ph -> X e. B ) |
|
| 5 | catcslotelcl.e | |- E = Slot ( E ` ndx ) |
|
| 6 | 1 2 3 4 | catcbascl | |- ( ph -> X e. U ) |
| 7 | 5 3 6 | wunstr | |- ( ph -> ( E ` X ) e. U ) |