Description: The Hom-set 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 ) |
||
| Assertion | catchomcl | |- ( ph -> ( Hom ` 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 | homid | |- Hom = Slot ( Hom ` ndx ) |
|
| 6 | 1 2 3 4 5 | catcslotelcl | |- ( ph -> ( Hom ` X ) e. U ) |