Metamath Proof Explorer


Theorem estrccat

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 )

Proof

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 )