This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ∈ V → C ∈ Cat

Proof

Step Hyp Ref Expression
1 estrccat.c ⊢ C = ExtStrCat ⁡ U
2 1 estrccatid ⊢ U ∈ V → C ∈ Cat ∧ Id ⁡ C = x ∈ U ⟼ I ↾ Base x
3 2 simpld ⊢ U ∈ V → C ∈ Cat