Description: The category of extensible structures is a category. (Contributed by AV, 8-Mar-2020)
Ref | Expression | ||
---|---|---|---|
Hypothesis | estrccat.c | |- C = ( ExtStrCat ` U ) |
|
Assertion | estrccat | |- ( U e. V -> C e. Cat ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | estrccat.c | |- C = ( ExtStrCat ` U ) |
|
2 | 1 | estrccatid | |- ( U e. V -> ( C e. Cat /\ ( Id ` C ) = ( x e. U |-> ( _I |` ( Base ` x ) ) ) ) ) |
3 | 2 | simpld | |- ( U e. V -> C e. Cat ) |