Theorem rhmsubcALTVcat

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

	Ref	Expression
Hypotheses	rngcrescrhmALTV.u	$$⊢\phi \to U\in V$$
	rngcrescrhmALTV.c	$$⊢C=\mathrm{RngCatALTV}\left(U\right)$$
	rngcrescrhmALTV.r	$$⊢\phi \to R=\mathrm{Ring}\cap U$$
	rngcrescrhmALTV.h	$$⊢H={\mathrm{RingHom}\upharpoonright }_{\left(R\times R\right)}$$
Assertion	rhmsubcALTVcat	$$⊢\phi \to \mathrm{RngCatALTV}\left(U\right){\upharpoonright }_{\mathrm{cat}}H\in \mathrm{Cat}$$

Proof

Step	Hyp	Ref	Expression
1		rngcrescrhmALTV.u	$$⊢\phi \to U\in V$$
2		rngcrescrhmALTV.c	$$⊢C=\mathrm{RngCatALTV}\left(U\right)$$
3		rngcrescrhmALTV.r	$$⊢\phi \to R=\mathrm{Ring}\cap U$$
4		rngcrescrhmALTV.h	$$⊢H={\mathrm{RingHom}\upharpoonright }_{\left(R\times R\right)}$$
5		eqid	$$⊢\mathrm{RngCatALTV}\left(U\right){\upharpoonright }_{\mathrm{cat}}H=\mathrm{RngCatALTV}\left(U\right){\upharpoonright }_{\mathrm{cat}}H$$
6	1 2 3 4	rhmsubcALTV	$$⊢\phi \to H\in \mathrm{Subcat}\left(\mathrm{RngCatALTV}\left(U\right)\right)$$
7	5 6	subccat	$$⊢\phi \to \mathrm{RngCatALTV}\left(U\right){\upharpoonright }_{\mathrm{cat}}H\in \mathrm{Cat}$$