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 𝐶 = ( ExtStrCat ‘ 𝑈 )
Assertion estrccat ( 𝑈𝑉𝐶 ∈ Cat )

Proof

Step Hyp Ref Expression
1 estrccat.c 𝐶 = ( ExtStrCat ‘ 𝑈 )
2 1 estrccatid ( 𝑈𝑉 → ( 𝐶 ∈ Cat ∧ ( Id ‘ 𝐶 ) = ( 𝑥𝑈 ↦ ( I ↾ ( Base ‘ 𝑥 ) ) ) ) )
3 2 simpld ( 𝑈𝑉𝐶 ∈ Cat )