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	⊢ ( 𝜑 → 𝑈 ∈ 𝑉 )
	rngcrescrhmALTV.c	⊢ 𝐶 = ( RngCatALTV ‘ 𝑈 )
	rngcrescrhmALTV.r	⊢ ( 𝜑 → 𝑅 = ( Ring ∩ 𝑈 ) )
	rngcrescrhmALTV.h	⊢ 𝐻 = ( RingHom ↾ ( 𝑅 × 𝑅 ) )
Assertion	rhmsubcALTVcat	⊢ ( 𝜑 → ( ( RngCatALTV ‘ 𝑈 ) ↾cat 𝐻 ) ∈ Cat )

Proof

Step	Hyp	Ref	Expression
1		rngcrescrhmALTV.u	⊢ ( 𝜑 → 𝑈 ∈ 𝑉 )
2		rngcrescrhmALTV.c	⊢ 𝐶 = ( RngCatALTV ‘ 𝑈 )
3		rngcrescrhmALTV.r	⊢ ( 𝜑 → 𝑅 = ( Ring ∩ 𝑈 ) )
4		rngcrescrhmALTV.h	⊢ 𝐻 = ( RingHom ↾ ( 𝑅 × 𝑅 ) )
5		eqid	⊢ ( ( RngCatALTV ‘ 𝑈 ) ↾cat 𝐻 ) = ( ( RngCatALTV ‘ 𝑈 ) ↾cat 𝐻 )
6	1 2 3 4	rhmsubcALTV	⊢ ( 𝜑 → 𝐻 ∈ ( Subcat ‘ ( RngCatALTV ‘ 𝑈 ) ) )
7	5 6	subccat	⊢ ( 𝜑 → ( ( RngCatALTV ‘ 𝑈 ) ↾cat 𝐻 ) ∈ Cat )