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 e. V -> C e. Cat )

Proof

Step	Hyp	Ref	Expression
1		catccat.c	|- C = ( CatCat ` U )
2		eqid	|- ( Base ` C ) = ( Base ` C )
3	1 2	catccatid	|- ( U e. V -> ( C e. Cat /\ ( Id ` C ) = ( x e. ( Base ` C ) |-> ( idFunc ` x ) ) ) )
4	3	simpld	|- ( U e. V -> C e. Cat )