Theorem sringcatALTV

Description: The restriction of the category of (unital) rings to the set of special ring homomorphisms is a category. (Contributed by AV, 19-Feb-2020) (New usage is discouraged.)

	Ref	Expression
Hypotheses	srhmsubcALTV.s	|- A. r e. S r e. Ring
	srhmsubcALTV.c	|- C = ( U i^i S )
	srhmsubcALTV.j	|- J = ( r e. C , s e. C |-> ( r RingHom s ) )
Assertion	sringcatALTV	|- ( U e. V -> ( ( RingCatALTV ` U ) |`cat J ) e. Cat )

Proof

Step	Hyp	Ref	Expression
1		srhmsubcALTV.s	|- A. r e. S r e. Ring
2		srhmsubcALTV.c	|- C = ( U i^i S )
3		srhmsubcALTV.j	|- J = ( r e. C , s e. C |-> ( r RingHom s ) )
4		eqid	|- ( ( RingCatALTV ` U ) |`cat J ) = ( ( RingCatALTV ` U ) |`cat J )
5	1 2 3	srhmsubcALTV	|- ( U e. V -> J e. ( Subcat ` ( RingCatALTV ` U ) ) )
6	4 5	subccat	|- ( U e. V -> ( ( RingCatALTV ` U ) |`cat J ) e. Cat )