Metamath Proof Explorer

Theorem ringccatALTV

Description: The category of rings is a category. (Contributed by AV, 14-Feb-2020) (New usage is discouraged.)

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

Proof

Step Hyp Ref Expression
1 ringccatALTV.c 
 |-  C = ( RingCatALTV ` U )
2 eqid 
 |-  ( Base ` C ) = ( Base ` C )
3 1 2 ringccatidALTV 
 |-  ( U e. V -> ( C e. Cat /\ ( Id ` C ) = ( x e. ( Base ` C ) |-> ( _I |` ( Base ` x ) ) ) ) )
4 3 simpld 
 |-  ( U e. V -> C e. Cat )