Metamath Proof Explorer

Theorem rngccatALTV

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

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

Proof

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