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 )