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	⊢ ∀ 𝑟 ∈ 𝑆 𝑟 ∈ Ring
	srhmsubcALTV.c	⊢ 𝐶 = ( 𝑈 ∩ 𝑆 )
	srhmsubcALTV.j	⊢ 𝐽 = ( 𝑟 ∈ 𝐶 , 𝑠 ∈ 𝐶 ↦ ( 𝑟 RingHom 𝑠 ) )
Assertion	sringcatALTV	⊢ ( 𝑈 ∈ 𝑉 → ( ( RingCatALTV ‘ 𝑈 ) ↾cat 𝐽 ) ∈ Cat )

Proof

Step	Hyp	Ref	Expression
1		srhmsubcALTV.s	⊢ ∀ 𝑟 ∈ 𝑆 𝑟 ∈ Ring
2		srhmsubcALTV.c	⊢ 𝐶 = ( 𝑈 ∩ 𝑆 )
3		srhmsubcALTV.j	⊢ 𝐽 = ( 𝑟 ∈ 𝐶 , 𝑠 ∈ 𝐶 ↦ ( 𝑟 RingHom 𝑠 ) )
4		eqid	⊢ ( ( RingCatALTV ‘ 𝑈 ) ↾cat 𝐽 ) = ( ( RingCatALTV ‘ 𝑈 ) ↾cat 𝐽 )
5	1 2 3	srhmsubcALTV	⊢ ( 𝑈 ∈ 𝑉 → 𝐽 ∈ ( Subcat ‘ ( RingCatALTV ‘ 𝑈 ) ) )
6	4 5	subccat	⊢ ( 𝑈 ∈ 𝑉 → ( ( RingCatALTV ‘ 𝑈 ) ↾cat 𝐽 ) ∈ Cat )