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	$$⊢\forall r\in Sr\in \mathrm{Ring}$$
	srhmsubcALTV.c	$$⊢C=U\cap S$$
	srhmsubcALTV.j	$$⊢J=\left(r\in C,s\in C⟼r\mathrm{RingHom}s\right)$$
Assertion	sringcatALTV	$$⊢U\in V\to \mathrm{RingCatALTV}\left(U\right){\upharpoonright }_{\mathrm{cat}}J\in \mathrm{Cat}$$

Proof

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