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\cap \mathrm{CRing}$$
	crhmsubc.j	$$⊢J=\left(r\in C,s\in C⟼r\mathrm{RingHom}s\right)$$
Assertion	cringcat	$$⊢U\in V\to \mathrm{RingCat}\left(U\right){\upharpoonright }_{\mathrm{cat}}J\in \mathrm{Cat}$$

Proof

Step	Hyp	Ref	Expression
1		crhmsubc.c	$$⊢C=U\cap \mathrm{CRing}$$
2		crhmsubc.j	$$⊢J=\left(r\in C,s\in C⟼r\mathrm{RingHom}s\right)$$
3		eqid	$$⊢\mathrm{RingCat}\left(U\right){\upharpoonright }_{\mathrm{cat}}J=\mathrm{RingCat}\left(U\right){\upharpoonright }_{\mathrm{cat}}J$$
4	1 2	crhmsubc	$$⊢U\in V\to J\in \mathrm{Subcat}\left(\mathrm{RingCat}\left(U\right)\right)$$
5	3 4	subccat	$$⊢U\in V\to \mathrm{RingCat}\left(U\right){\upharpoonright }_{\mathrm{cat}}J\in \mathrm{Cat}$$