Metamath Proof Explorer

Theorem setccat

Description: The category of sets is a category. (Contributed by Mario Carneiro, 3-Jan-2017)

Ref Expression
Hypothesis setccat.c 
|- C = ( SetCat ` U )
Assertion setccat 
|- ( U e. V -> C e. Cat )

Proof

Step Hyp Ref Expression
1 setccat.c 
 |-  C = ( SetCat ` U )
2 1 setccatid 
 |-  ( U e. V -> ( C e. Cat /\ ( Id ` C ) = ( x e. U |-> ( _I |` x ) ) ) )
3 2 simpld 
 |-  ( U e. V -> C e. Cat )