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	⊢ 𝐶 = ( CatCat ‘ 𝑈 )
Assertion	catccat	⊢ ( 𝑈 ∈ 𝑉 → 𝐶 ∈ Cat )

Proof

Step	Hyp	Ref	Expression
1		catccat.c	⊢ 𝐶 = ( CatCat ‘ 𝑈 )
2		eqid	⊢ ( Base ‘ 𝐶 ) = ( Base ‘ 𝐶 )
3	1 2	catccatid	⊢ ( 𝑈 ∈ 𝑉 → ( 𝐶 ∈ Cat ∧ ( Id ‘ 𝐶 ) = ( 𝑥 ∈ ( Base ‘ 𝐶 ) ↦ ( idfunc ‘ 𝑥 ) ) ) )
4	3	simpld	⊢ ( 𝑈 ∈ 𝑉 → 𝐶 ∈ Cat )