Theorem rhmsubccat

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)

	Ref	Expression
Hypotheses	rngcrescrhm.u	|- ( ph -> U e. V )
	rngcrescrhm.c	|- C = ( RngCat ` U )
	rngcrescrhm.r	|- ( ph -> R = ( Ring i^i U ) )
	rngcrescrhm.h	|- H = ( RingHom |` ( R X. R ) )
Assertion	rhmsubccat	|- ( ph -> ( ( RngCat ` U ) |`cat H ) e. Cat )

Proof

Step	Hyp	Ref	Expression
1		rngcrescrhm.u	|- ( ph -> U e. V )
2		rngcrescrhm.c	|- C = ( RngCat ` U )
3		rngcrescrhm.r	|- ( ph -> R = ( Ring i^i U ) )
4		rngcrescrhm.h	|- H = ( RingHom |` ( R X. R ) )
5		eqid	|- ( ( RngCat ` U ) |`cat H ) = ( ( RngCat ` U ) |`cat H )
6	1 2 3 4	rhmsubc	|- ( ph -> H e. ( Subcat ` ( RngCat ` U ) ) )
7	5 6	subccat	|- ( ph -> ( ( RngCat ` U ) |`cat H ) e. Cat )