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

Metamath Proof Explorer

Theorem catccat

Description: The category of categories is a category, see remark 3.48 in Adamek p. 40. (Clearly it cannot be an element of itself, hence it is " U -large".) (Contributed by Mario Carneiro, 3-Jan-2017)

Ref Expression
Hypothesis catccat.c ⊢ C = CatCat ⁡ U
Assertion catccat ⊢ U ∈ V → C ∈ Cat

Proof

Step Hyp Ref Expression
1 catccat.c ⊢ C = CatCat ⁡ U
2 eqid ⊢ Base C = Base C
3 1 2 catccatid ⊢ U ∈ V → C ∈ Cat ∧ Id ⁡ C = x ∈ Base C ⟼ id func ⁡ x
4 3 simpld ⊢ U ∈ V → C ∈ Cat