Theorem cringcat

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

	Ref	Expression
Hypotheses	crhmsubc.c	|- C = ( U i^i CRing )
	crhmsubc.j	|- J = ( r e. C , s e. C |-> ( r RingHom s ) )
Assertion	cringcat	|- ( U e. V -> ( ( RingCat ` U ) |`cat J ) e. Cat )

Proof

Step	Hyp	Ref	Expression
1		crhmsubc.c	|- C = ( U i^i CRing )
2		crhmsubc.j	|- J = ( r e. C , s e. C |-> ( r RingHom s ) )
3		eqid	|- ( ( RingCat ` U ) |`cat J ) = ( ( RingCat ` U ) |`cat J )
4	1 2	crhmsubc	|- ( U e. V -> J e. ( Subcat ` ( RingCat ` U ) ) )
5	3 4	subccat	|- ( U e. V -> ( ( RingCat ` U ) |`cat J ) e. Cat )